Partial hyperdoctrines: categorical models for partial function logic and Hoare logic

1994 ◽  
Vol 4 (2) ◽  
pp. 117-146
Author(s):  
Peter Knijnenburg ◽  
Frank Nordemann
Keyword(s):  
Programming Language ◽  
Partial Function ◽  
Hoare Logic ◽  
Weakest Precondition ◽  
First Order ◽  
Categorical Models ◽  
Intended Use

In this paper we provide a categorical interpretation of the first-order Hoare logic of a small programming language by giving a weakest precondition semantics for the language. To this end, we extend the well-known notion of a (first-order) hyperdoctrine to include partial maps. The most important new aspect of the resulting partial (first-order) hyperdoctrine is a different notion of morphism between the fibres. We also use this partial hyperdoctrine to give a model for Beeson's Partial Function Logic such that (a version of) his axiomatization is complete with respect to this model. This shows the usefulness of the notion, independent of its intended use as a model for Hoare logic.

A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language

2011 ◽  
Vol 76 (2) ◽  
pp. 673-699 ◽  
Author(s):  
Michael Gabbay
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Functional Programming ◽  
Order Logic ◽  
First Order Logic ◽  
Cut Elimination ◽  
Logic Programming Language ◽  
First Order ◽  
Functional Programming Language ◽  
Sequent System

AbstractWe build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic.We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).

scholarly journals VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC

2002 ◽  
Vol 13 (03) ◽  
pp. 315-340 ◽  
Author(s):  
J. I. DEN HARTOG ◽  
E. P. DE VINK
Keyword(s):  
Programming Language ◽  
Denotational Semantics ◽  
Order Logic ◽  
First Order Logic ◽  
Proof System ◽  
Probabilistic Choice ◽  
First Order ◽  
Probabilistic Programs

Probability, be it inherent or explicitly introduced, has become an important issue in the verification of programs. In this paper we study a formalism which allows reasoning about programs which can act probabilistically. To describe probabilistic programs, a basic programming language with an operator for probabilistic choice is introduced and a denotational semantics is given for this language. To specify propertics of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates is introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to be sound and complete; the properties that can be derived are exactly the valid properties. Finally some typical examples illustrate the use of the probabilistic predicates and the proof system.

scholarly journals Here and There with Arithmetic

2021 ◽  
pp. 1-15
Author(s):  
VLADIMIR LIFSCHITZ
Keyword(s):  
Programming Language ◽  
Propositional Logic ◽  
Answer Set Programming ◽  
The Other ◽  
Arithmetic Operations ◽  
First Order ◽  
The Relationship ◽  
Answer Set

Abstarct In the theory of answer set programming, two groups of rules are called strongly equivalent if, informally speaking, they have the same meaning in any context. The relationship between strong equivalence and the propositional logic of here-and-there allows us to establish strong equivalence by deriving rules of each group from rules of the other. In the process, rules are rewritten as propositional formulas. We extend this method of proving strong equivalence to an answer set programming language that includes operations on integers. The formula representing a rule in this language is a first-order formula that may contain comparison symbols among its predicate constants, and symbols for arithmetic operations among its function constants. The paper is under consideration for acceptance in TPLP.

scholarly journals Generalizations of Rice's Theorem, Applicable to Executable and Non-Executable Formalisms

10.29007/jnl6 ◽  
2018 ◽  
Author(s):  
Cornelis Huizing ◽  
Ruurd Kuiper ◽  
Tom Verhoeff
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Specification Language ◽  
Partial Function ◽  
Program Text ◽  
Turing Machines ◽  
Partial Functions ◽  
Executable Specification ◽  
Special Cases ◽  
Diagonal Argument

We formulate and prove two Rice-like theoremsthat characterize limitations on nameability of propertieswithin a given naming scheme for partial functions.Such a naming scheme can, but need not be, an executable formalism.A programming language is an example of an executable naming scheme,where the program text names the partial function it implements.Halting is an example of a propertythat is not nameable in that naming scheme.The proofs reveal requirements on the naming schemeto make the characterization work.Universal programming languages satisfy these requirements,but also other formalisms can satisfy them.We present some non-universal programming languagesand a non-executable specification languagesatisfying these requirements.Our theorems haveTuring's well-known Halting Theorem and Rice's Theorem as special cases,by applying them to a universal programming language or Turing Machines as naming scheme.Thus, our proofs separate the nature of the naming scheme(which can, but need not, coincide with computability) from the diagonal argument.This sheds further light on how far reaching and simple the `diagonal' argument is in itself.

Implementing the cylindrical algebraic decomposition within the Coq system

2007 ◽  
Vol 17 (1) ◽  
pp. 99-127 ◽  
Author(s):  
ASSIA MAHBOUBI
Keyword(s):  
Programming Language ◽  
Decision Procedure ◽  
Order Theory ◽  
Decomposition Algorithm ◽  
Proof Assistant ◽  
Real Numbers ◽  
First Order ◽  
Cylindrical Algebraic Decomposition ◽  
First Order Theory ◽  
Automation Tools

The Coq system is a Curry–Howard based proof assistant. Therefore, it contains a full functional, strongly typed programming language, which can be used to enhance the system with powerful automation tools through the implementation of reflexive tactics. We present the implementation of a cylindrical algebraic decomposition algorithm within the Coq system, whose certification leads to a proof producing decision procedure for the first-order theory of real numbers.

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.

scholarly journals A Programming Language for the Inductive Sets, and Applications

1982 ◽  
Vol 11 (143) ◽  
Author(s):  
David Harel ◽  
Dexter Kozen
Keyword(s):  
Programming Language ◽  
Relational Database ◽  
Query Language ◽  
Dynamic Logic ◽  
Computational Approach ◽  
Turing Machines ◽  
First Order ◽  
Separation Result ◽  
Alternating Turing Machines ◽  
Order Structures

We introduce a programming language IND that generalizes alternating Turing machines to arbitrary first-order structures. We show that IND programs (respectively, everywhere-halting IND programs, loop-free IND programs) accept precisely the inductively definable (respectively, hyperelementary, elementary) relations. We give several examples showing how the language provides a robust and computational approach to the theory of first-order inductive definability. We then show: (1) on all acceptable structures (in the sense of Moschovakis), r.e. Dynamic Logic is more expressive than finite-test Dynamic Logic. This refines a separation result of Meyer and Parikh; (2) IND provides a natural query language for the set of fixpoint queries over a relational database, answering a question of Chandra and Harel.

Sign in / Sign up

Export Citation Format

Share Document