scholarly journals Well-founded Functions and Extreme Predicates in Dafny: A Tutorial

10.29007/v2m3 ◽  
2018 ◽  
Author(s):  
Rustan Leino
Keyword(s):  
Boolean Function ◽  
Programming Language ◽  
Inference Rules ◽  
Recursive Call ◽  
Constructive Logic ◽  
Smt Solver ◽  
First Order ◽  
The Core ◽  
General Terms ◽  
The Difference

A recursive function is well defined if its every recursive callcorresponds a decrease in some well-founded order. Such a function issaid to be _terminating_ and is in many applications the standard wayto define a function. A boolean function can also be defined asan extreme solution to a recurrence relation, that is, as a least orgreatest fixpoint of some functor. Such _extreme predicates_ areuseful to encode a set of inductive or coinductive inference rulesand are at the core of many a constructive logic. Theverification-aware programming language Dafny supports bothterminating functions and extreme predicates. This tutorialdescribes the difference in general terms, and then describes novelsyntactic support in Dafny for defining and proving lemmas withextreme predicates. Various examples and considerations are given.Although Dafny's verifier has at its core a first-order SMT solver,Dafny's logical encoding makes it possible to reason about fixpointsin an automated way.

Constructive mathematics and computer programming

1984 ◽  
Vol 312 (1522) ◽  
pp. 501-518 ◽  
Keyword(s):  
Computer Science ◽  
Programming Languages ◽  
Programming Language ◽  
Program Synthesis ◽  
Constructive Mathematics ◽  
Inference Rules ◽  
Computing Science ◽  
Intuitionistic Theory ◽  
The Difference ◽  
Correct Program

If programming is understood not as the writing of instructions for this or that computing machine but as the design of methods of computation that it is the computer’s duty to execute (a difference that Dijkstra has referred to as the difference between computer science and computing science), then it no longer seems possible to distinguish the discipline of programming from constructive mathematics. This explains why the intuitionistic theory of types (Martin-Lof 1975 In Logic Colloquium 1973 (ed. H. E. Rose & J. C. Shepherdson), pp. 73- 118. Amsterdam: North-Holland), which was originally developed as a symbolism for the precise codification of constructive mathematics, may equally well be viewed as a programming language. As such it provides a precise notation not only, like other programming languages, for the programs themselves but also for the tasks that the programs are supposed to perform. Moreover, the inference rules of the theory of types, which are again completely formal, appear as rules of correct program synthesis. Thus the correctness of a program written in the theory of types is proved formally at the same time as it is being synthesized.

Extended natural semantics

1993 ◽  
Vol 3 (2) ◽  
pp. 123-152 ◽  
Author(s):  
John Hannan
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Functional Programming ◽  
Higher Order ◽  
Order Logic ◽  
Inference Rules ◽  
Abstract Syntax ◽  
Higher Order Logic ◽  
First Order ◽  
Definition Of

AbstractWe extend the definition of natural semantics to include simply typed λ-terms, instead of first-order terms, for representing programs, and to include inference rules for the introduction and discharge of hypotheses and eigenvariables. This extension, which we call extended natural semantics, affords a higher-level notion of abstract syntax for representing programs and suitable mechanisms for manipulating this syntax. We present several examples of semantic specifications for a simple functional programming language and demonstrate how we achieve simple and elegant manipulations of bound variables in functional programs. All the examples have been implemented and tested in λProlog, a higher-order logic programming language that supports all of the features of extended natural semantics.

Computing Cores for Existential Rules with the Standard Chase and ASP

2020 ◽  
Author(s):  
Markus Krötzsch
Keyword(s):  
Large Class ◽  
Data Exchange ◽  
Answer Set Programming ◽  
Query Answering ◽  
Universal Model ◽  
The Core ◽  
Universal Models ◽  
General Terms ◽  
Special Cases ◽  
The Many

To reason with existential rules (a.k.a. tuple-generating dependencies), one often computes universal models. Among the many such models of different structure and cardinality, the core is arguably the “best”. Especially for finitely satisfiable theories, where the core is the unique smallest universal model, it has advantages in query answering, non-monotonic reasoning, and data exchange. Unfortunately, computing cores is difficult and not supported by most reasoners. We therefore propose ways of computing cores using practically implemented methods from rule reasoning and answer set programming. Our focus is on cases where the standard chase algorithm produces a core. We characterise this desirable situation in general terms that apply to a large class of cores, derive concrete approaches for decidable special cases, and generalise these approaches to non-monotonic extensions of existential rules.

Boolean-valued structures

2018 ◽  
Author(s):  
Tim Button ◽  
Sean Walsh
Keyword(s):  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Inference Rules ◽  
Mathematical Concepts ◽  
Semantic Framework ◽  
First Order ◽  
Standard Models ◽  
Boolean Valued Model ◽  
Semantic Values

Chapters 6-12 are driven by questions about the ability to pin down mathematical entities and to articulate mathematical concepts. This chapter is driven by similar questions about the ability to pin down the semantic frameworks of language. It transpires that there are not just non-standard models, but non-standard ways of doing model theory itself. In more detail: whilst we normally outline a two-valued semantics which makes sentences True or False in a model, the inference rules for first-order logic are compatible with a four-valued semantics; or a semantics with countably many values; or what-have-you. The appropriate level of generality here is that of a Boolean-valued model, which we introduce. And the plurality of possible semantic values gives rise to perhaps the ‘deepest’ level of indeterminacy questions: How can humans pin down the semantic framework for their languages? We consider three different ways for inferentialists to respond to this question.

Spatial Convergence in Height in Central Europe, 1890-1910

2009 ◽  
pp. 90
Author(s):  
Marek Brabec ◽  
John Komlos
Keyword(s):  
Global Economy ◽  
Well Being ◽  
Habsburg Monarchy ◽  
The Core ◽  
Military Recruits ◽  
Convergence Clubs ◽  
Spatial Convergence ◽  
Physical Stature ◽  
The Difference ◽  
Peripheral Areas

We examine spatial convergence in biological well-being in the Habsburg Monarchy, circa 1890-1910, on the basis of evidence of the physical stature of 21-year-old military recruits, disaggregated into 15 Districts. We find that the shorter the population in 1890, the faster its height grew thereafter. Hence, there was convergence in physical stature between the peripheral areas of the monarchy (located in today’s Poland/Ukraine, Romania, and Slovakia) and its core (located in today’s Austria, Czech Republic, and Hungary). The difference in trends between the trend in height in the Polish District of Przemysl and in Vienna was about 0.9 cm per decade, in favor of the former. Convergence among the core Districts themselves was minimal or non-existent, whereas the convergence among the peripheral Districts was more pronounced. Spatial convergence also took place between the peripheral regions and the more developed ones. The pattern is somewhat reminiscent of modern findings on convergence clubs in the global economy.

Gebruiksaspecten van het uitroeppartikel wat in het Nederlands en Fries

2020 ◽  
Vol 136 (4) ◽  
pp. 189-209
Author(s):  
Henk Wolf
Keyword(s):  
The Core ◽  
The Difference ◽  
Lexical Phrase ◽  
High Degree ◽  
Lexical Phrases

Abstract Both Dutch and (West) Frisian make use of the exclamative particle wat (‘how’), that adds an element of surprise about a high degree of something to the semantics of the sentence. In this paper I will first show the similarities between the use of the particle in the two languages. I will demonstrate that, in Dutch, its use is largely confined to constructions that are semantically scalable, whereas in Frisian this restriction is far less strict. I will explain the difference by showing that Dutch wat is a syntactic amplifier of lexical phrases, whereas Frisian wat has developed into a pragmatic amplifier of the core predicate. I will try to account for that difference by showing how homophonous words absent in Dutch are likely to have influenced the use of Frisian wat, and how Dutch prosody strengthens the connection between wat and the amplified lexical phrase, whereas Frisian prosody weakens it. Finally, I will show that the system described as ‘Frisian’ is occasionally found in varieties of Dutch too

scholarly journals A comparative analysis of differentially expressed mRNAs, miRNAs and circRNAs provides insights into the key genes involved in the high-altitude adaptation of yaks

BMC Genomics ◽  
2021 ◽  
Vol 22 (1) ◽  
Author(s):  
Qianyun Ge ◽  
Yongbo Guo ◽  
Wangshan Zheng ◽  
Yuan Cai ◽  
Xuebin Qi ◽  
...  
Keyword(s):  
High Altitude ◽  
Molecular Mechanisms ◽  
Regulation Of Gene Expression ◽  
Differentially Expressed ◽  
The Tibetan Plateau ◽  
The Core ◽  
Processing Pathways ◽  
Genetic Information Processing ◽  
Altitude Adaptation ◽  
The Difference

Abstract Background Yaks that inhabit the Tibetan Plateau exhibit striking phenotypic and physiological differences from cattle and have adapted well to the extreme conditions on the plateau. However, the mechanisms used by these animals for the regulation of gene expression at high altitude are not fully understood. Results Here, we sequenced nine lung transcriptomes of yaks at altitudes of 3400, 4200 and 5000 m, and low-altitude Zaosheng cattle, which is a closely related species, served as controls. The analysis identified 21,764 mRNAs, 1377 circRNAs and 1209 miRNAs. By comparing yaks and cattle, 4975 mRNAs, 252 circRNAs and 75 miRNAs were identified differentially expressed. By comparing yaks at different altitudes, we identified 756 mRNAs, 64 circRNAs and 83 miRNAs that were differentially expressed (fold change ≥2 and P-value < 0.05). The pathways enriched in the mRNAs, circRNAs and miRNAs identified from the comparison of yaks and cattle were mainly associated with metabolism, including ‘glycosaminoglycan degradation’, ‘pentose and glucuronate interconversions’ and ‘flavone and flavonol biosynthesis’, and the mRNAs, circRNAs and miRNAs identified from the comparison of yaks at different altitude gradients were significantly enriched in metabolic pathways and immune and genetic information processing pathways. The core RNAs were identified from the mRNA-miRNA-circRNA networks constructed using the predominant differentially expressed RNAs. The core genes specific to the difference between yaks and cattle were associated with the endoplasmic reticulum and fat deposition, but those identified from the comparison among yaks at different altitude gradients were associated with maintenance of the normal biological functions of cells. Conclusions This study enhances our understanding of the molecular mechanisms involved in hypoxic adaptation in yaks and might contribute to improvements in the understanding and prevention of hypoxia-related diseases.

scholarly journals Territorial organization of the restaurant facilities of Kyiv agglomeration

2015 ◽  
pp. 79-82
Author(s):  
K. Dmytriieva
Keyword(s):  
Restaurant Industry ◽  
The Core ◽  
Industry Standards ◽  
The Status ◽  
Territorial Organization ◽  
The Difference ◽  
Surrounding Areas ◽  
Concentration Ratios

The article outlines the factors of development of the restaurant facilities in Kyiv and surrounding areas. The status of the territorial organization of the restaurant facilities of Kyiv and Kyiv region through the review of the main indicators of the industry by districts in 2013 has been analyzed. Comparison of the industry standards due to availability of these services to population needs has been performed. The result of the difference of efficiency of the restaurant industry through calculation of concentration ratios turnover has been received. Area that can be considered as the core of the restaurant industry of Kyiv agglomeration and area with the potential of growth has been identified. The article visualized by maps.

scholarly journals Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny

10.29007/5zjp ◽  
2018 ◽  
Author(s):  
Sylvia Grewe ◽  
Sebastian Erdweg ◽  
Mira Mezini
Keyword(s):  
Formal Methods ◽  
Programming Language ◽  
Type System ◽  
Type Systems ◽  
Domain Specific Languages ◽  
Smt Solver ◽  
Domain Specific ◽  
Efficient Type

\noindent Developing provably sound type systems is a non-trivial task which, as of today, typically requires expert skills in formal methods and a considerable amount of time. Our Veritas~\cite{GreweErdwegWittmannMezini15} project aims at providing support for the development of soundness proofs of type systems and efficient type checker implementations from specifications of type systems. To this end, we investigate how to best automate typical steps within type soundness proofs.\noindent In this paper, we focus on progress proofs for type systems of domain-specific languages. As a running example for such a type system, we model a subset SQL and augment it with a type system. We compare two different approaches for automating proof steps of the progress proofs for this type system against each other: firstly, our own tool Veritas, which translates proof goals and specifications automatically to TPTP~\cite{Sutcliffe98} and calls Vampire~\cite{KovacsV13} on them, and secondly, the programming language Dafny~\cite{Leino2010}, which translates proof goals and specifications to the intermediate verification language Boogie 2~\cite{Leino2008} and calls the SMT solver Z3~\cite{DeMoura2008} on them. We find that Vampire and Dafny are equally well-suited for automatically proving simple steps within progress proofs.

scholarly journals Weak solvability of the unconditionally stable difference scheme for the coupled sine-Gordon system

2020 ◽  
Vol 25 (6) ◽  
pp. 997-1014
Author(s):  
Ozgur Yildirim ◽  
Meltem Uzun
Keyword(s):  
Difference Scheme ◽  
Numerical Method ◽  
Existence And Uniqueness ◽  
Numerical Experiments ◽  
Finite Difference Schemes ◽  
Order Of Accuracy ◽  
Unconditionally Stable ◽  
First Order ◽  
The Difference ◽  
Weak Solvability

In this paper, we study the existence and uniqueness of weak solution for the system of finite difference schemes for coupled sine-Gordon equations. A novel first order of accuracy unconditionally stable difference scheme is considered. The variational method also known as the energy method is applied to prove unique weak solvability.We also present a new unified numerical method for the approximate solution of this problem by combining the difference scheme and the fixed point iteration. A test problem is considered, and results of numerical experiments are presented with error analysis to verify the accuracy of the proposed numerical method.

Sign in / Sign up

Export Citation Format

Share Document