key: cord-0046157-t5duxtjv
authors: Berger, Ulrich; Petrovska, Olga; Tsuiki, Hideki
title: Prawf: An Interactive Proof System for Program Extraction
date: 2020-06-24
journal: Beyond the Horizon of Computability
DOI: 10.1007/978-3-030-51466-2_12
sha: 6bf077ad26ac17aa24941e97201f7d3627bdb900
doc_id: 46157
cord_uid: t5duxtjv

We present an interactive proof system dedicated to program extraction from proofs. In a previous paper [5] the underlying theory IFP (Intuitionistic Fixed Point Logic) was presented and its soundness proven. The present contribution describes a prototype implementation and explains its use through several case studies. The system benefits from an improvement of the theory which makes it possible to extract programs from proofs using unrestricted strictly positive inductive and coinductive definitions, thus removing the previous admissibility restrictions.

One of the salient features of constructive proofs is the fact that they carry computational content which can be extracted by a simple automatic procedure. Examples of formal systems providing constructive proofs are intuitionistic (Heyting) arithmetic or (varieties of) constructive type theory. There exist several computer implementations of these systems, which support program extraction based on Curry-Howard correspondence (e.g. Minlog [4] , Nuprl [8, 10] , Coq [7, 9] , Isabelle [1], Agda [2]). However, none of them has program extraction as their main raison d'être.

In [5] the system IFP (Intuitionistic Fixed Point Logic) was introduced whose primary goal is program extraction. IFP is first-order logic extended with least and greatest fixed points of strictly positive predicate transformers. Program extraction in IFP is based on a refined realizability interpretation that permits arbitrary classically true disjunction-free formulas as axioms and ignores the (trivial) computational content of proofs of Harrop formulas thus leading to programs without formal garbage. The main purpose of [5] was to show soundness of this realizability interpretation, that is, the correctness of extracted programs.

In the present paper we present Prawf 1 , the first prototype of an implementation of IFP as an interactive proof system with program extraction feature. Prawf is based on a (compared with [5] ) simplified notion of program and an improved Soundness Theorem that admits least and greatest fixed points of arbitrary strictly positive predicate transformers, removing the admissibility restriction in [5] .

The paper is structured as follows: In Sect. 2 we briefly recap IFP and program extraction in IFP, explaining in some detail the above mentioned changes and improvements. In Sect. 3 we describe Prawf and its basic use through some simple examples involving real and natural numbers. Section 4 contains an advanced case study about exact real number representations: The well-known signed digit representation and infinite Gray-code [12] are represented by coinductive predicates and inclusion between the predicates is proven in Prawf thus enabling the extraction of a program transforming the signed digit representation into infinite Gray-code. In the conclusion we reflect on what we achieved and compare our work with related approaches.

We briefly summarize the system IFP and its associated program extraction procedure. For full details we refer to [5] . IFP Syntax and Proofs. The syntax of IFP has terms, formulas, predicates and operators, the latter describing strictly positive (s.p.) and hence monotone predicate transformers. For every s.p. operator Φ there are predicates μΦ and ν Φ denoting the predicates defined inductively resp. coinductively from Φ:

Terms r, s, t ::= x (variables) | f (t 1 , . . . , t n ) ( f function constant) Formulas A, B ::= P( ì t) (P not an abstraction, ì t arity(P)-many terms)

Operators Φ,Ψ ::= λX P (P s.p. in X, arity(λX P) = arity(X) = arity(P))

where P is s.p. in X if every free occurrence of X in P is at a s.p. position, i.e. not in the premise of an implication. The proof rules of IFP are the usual rules of intuitionistic first-order logic with equality (regarding equality as binary predicate constant) augmented by rules stating that μΦ and ν Φ are the least and greatest fixed points of Φ (see Fig. 1 , ignoring for the moment the expressions to the left of the colon).

Programs. The programs extracted from proofs are terms in an untyped λcalculus enriched by constructors for pattern matching and recursion.

where in the case-construct each Cl i is a clause of the form C(a 1 , . . . , a k ) → q in which C is a constructor, i.e. one of Nil, Lt, Rt, Pair, and the a i are pairwise different program variables binding the free occurrences of the a i in q. rec p computes the (least) fixed point of p, hence p rec(p) = rec(p). It is well-known that an essentially equivalent calculus can be defined within the pure untyped λ-calculus, however, the enriched version is more convenient to work with. For the sake of readability we slightly simplify our notion of program compared to the one in [5] by no longer distinguishing between programs and functions.

Program Extraction. In its raw form the extracted program of a proof is simply obtained by replacing the proof rules by corresponding program constructs following the Curry-Howard correspondence. This is summarized in Fig. 1 where p : A means that p is the program extracted from a proof of A. In the assumption rule and the rule → + , 'a : A 'indicates that the assumption A in the proof has been assigned the program variable a. In the rule ∧ − L , proj L (p) stands for the program case p of {Pair(a, b) → a}. Similarly for ∧ − R . The rules ∀ + and ∃ − are subject to the usual provisos. In the rules ind and coind the program m Φ realizes (in a sense explained below) the monotonicity of Φ, that is the formula

The correctness of programs is expressed through a realizability relation p r A between programs p and formulas A which is defined by recursion on formulas (see [5] ). Formally, realizability is defined as a family of unary predicates R(A) on a Scott domain D of 'potential realizers'. p r A means that the denotation of p in D satisfies the predicate R(A). The Soundness Theorem [5] shows that if p is extracted from a proof of A, then p realizes A. The Soundness Theorem is formalised in a theory RIFP that extends IFP by a sort of realizers and axioms that describe the behaviour of programs. The denotational semantics of programs is linked to the operational one through the Adequacy Theorem, stating that programs with non-⊥ value terminate and reduce to that value [6] .

Refinements. Program extraction in its raw form (as sketched above) produces correct programs which, however, contain a lot of garbage and are therefore practically useless. This is due to programs extracted from sub proofs of Harrop formulas, that is, formulas which do not contain a disjunction at a strictly positive position. These programs contain no useful information and should therefore be contracted to a trivial program, say Nil. In a refined realizability interpretation, which was presented in [5] and which is implemented in Prawf, this contraction is carried out. It is based on a refined notion of realizability and a refined program extraction procedure. The proof of the soundness theorem becomes considerably more complicated and could only be accomplished in [5] by subjecting induction and coinduction to a certain admissibility condition. In [6] a soundness proof without this restriction is given. It uses an intermediate system IFP whose induction and coinduction rules require as additional premise a proof of the monotonicity of Φ, e.g.,

Soundness is then proven for IFP and transferred to IFP via an embedding of IFP into IFP . Minlog [4] has a similar refined realizability interpretation but treats disjunction-free formulas and Harrop formulas in the same way. This simplifies program extraction but seems to restrict the validity of the Soundness Theorem to a constructive framework (see also the remarks in Sect. 5).

Axioms. For a proof with assumptions the soundness theorem states that the extracted program computes a realizer of the proven formula from realizers of the assumptions. If the assumptions contain no disjunctions at all -we call such assumptions non-computational (nc) -then they are Harrop formulas and hence their realizers are trivial but, even more, they are equivalent to their realizability interpretations. This fact is extremely useful since it implies that a program extracted from a proof that uses nc-assumptions (regarded as axioms specifying a class of structures) will not depend on realizers of these axioms and will be correct in any model of the axioms. For example, in a proof about real numbers (see Sect. 3) the arithmetic operations may be given abstractly and specified by nc-axioms (e.g. ∀x (x + 0 = x) and ∀x (x 0 → ∃y (x * y = 1))).

In the systems Nuprl, Coq, Agda, and Minlog computation is built into the notion of proof by considering terms, formulas or types up to normal form with respect to certain rewrite rules. As a consequence, each of these systems has various (decidable or undecidable) notions of equality, which may make proof checking (deciding the correctness of a proof) algorithmically hard if not undecidable. The motivations for interweaving logic and computation are partly philosophical and partly practical since in this way a fair amount of (otherwise laborious) equational reasoning can be automatized. In contrast, the system IFP strictly separates computation from reasoning. Its proof calculus is free of computation and there is only one notion of equality obeying the usual rules of equational logic. This makes proof checking a nearly trivial task. Equational reasoning can be to a large extent (or even completely) externalised by stating the required equations (which are nc-formulas) as axioms which can be proven elsewhere (or believed). Computation is confined to programs and is given through rewrite rules which enjoy an Adequacy Theorem stating that the operational and the denotational semantics of programs match [3, 6] .

Prawf [11] is a prototype implementation in Haskell, which allows users to write IFP proofs and extract executable programs from them. It follows pretty closely the theory of IFP sketched in the previous section but extends it in several respects:

-the logical language of Prawf is many-sorted; -names for predicates and operators can be introduced through declarations; -induction and coinduction come in three variations, the original ones presented in Sect. 2, and two strengthenings (half-strong and strong (co)induction) which are explained and motivated below.

The software has two modes: a prover mode and an execution mode. The prover mode enables users to create a proof environment, consisting of a language, a context, declarations and axioms. The proof rules in Prawf correspond to those of IFP and include the usual natural deduction rules for predicate logic, rules for (co)induction, half-strong (co)induction and strong (co)induction, as well as the equality rules such as symmetry, reflexivity and congruence.

A theorem can be proven by applying these rules step by step or by using a tactic. A tactic consists of a sequence of proof commands that allows users to re-run a proof either partially or fully. Once proven, a theorem can be saved in a theory and used as a part of another proof.

The execution mode allows running extracted programs. In this mode a user can take advantage of the standard Prelude commands as well as special functions for running and showing programs.

An Introductory Example: Natural Numbers and Addition. We explain the working of Prawf by means of a simple example based on the language of real numbers with the constants 0 and 1 and the operations + and − for addition and subtraction. We first give the idea in ordinary mathematical language and then show how to do it in Prawf. We define the natural numbers as the least subset (predicate) of the reals that contains 0 and that contains x whenever it contains x − 1:

We prove that N is closed under addition:

Hence assume N(x). We have to show ∀y(N(y) → N(x + y)), that is N ⊆ P where P Def = λy N(x + y). By the induction rule it suffices to show Φ(P) ⊆ P, that is,

If y = 0 then N(x + y) holds since x + 0 = x (using an axiom) and N(x) holds by assumption. If N(x + (y − 1)), then N((x + y) − 1) since x + (y − 1) = x + (y − 1) (using an axiom) and hence N(x + y) by the closure rule.

In order to carry out this example in Prawf one first needs to define the language. This can be done by creating in the directory batches a subdirectory real (the name can be freely chosen), and in that directory the text file lang.txt (the name is prescribed) with the contents Note that we do not need to give definitions of + and -. For the proofs it is sufficient to know their properties that are expressed through axioms.

In the same subdirectory one creates the file decls.txt (name prescribed) containing the definition of N:

Phi:(R) = lambda Y:(R) lambda (z:R) (z=0 v Y(z-1)) N:(R) = Mu(Phi) Finally, one creates (again in the directory real) the file axi.txt (name prescribed) containing the axioms one wishes to use. The axioms must be ncformulas that is, not contain any disjunctions (for example the predicate N must not occur since its definition contains ∨ as part of the definition of Φ).

ax1 . all x:R x+0 = x ax2 . all x:R all y:R (x+y)-1 = x+(y-1)

Now we are set to start our proof. We load the Haskell file Mode.hs, execute main, load our batch by typing real (after which the contents of the files we created will be displayed) and type at the prompt our goal formula Enter goal formula> all x:R (N(x) -> all y:R (N(y) -> N(x+y))) Proving in Prawf proceeds in the usual goal-directed backwards reasoning style. In our example the first two steps are easy: alli (for ∀-introduction backwards), then impi v1 (for →-introduction backwards creating the assumption v1 : N(x)). After these two steps one arrives at which easily follows from our axioms and some equality reasoning. The necessary steps in Prawf (and much more) can be found in a tutorial on the Prawf website.

Program Extraction. After completing the proof above one can extract a program by typing extract addition (addition is a name we chose). This will write the extracted program into the file progs.txt: addition . ProgAbst "v1" (ProgRec (ProgAbst "f_mu" (ProgAbst "a_comp" (ProgCase (ProgVar "a_comp") [(Lt,["a_ore"],ProgVar "v1"),(Rt,["b_ore"],ProgCon Rt [ProgApp (ProgVar "f_mu") (ProgVar "b_ore")])]))))

The program transforms realizers of N(x) and N(y) into a realizer of N(x + y).

By the inductive definition of the predicate N its elements are realized in unary notation where Lt( ) plays the role of 0 and Rt plays the role of the successor function. The extracted program can be rewritten in more readable form as follows (using Haskell notation):

addition v1 a_comp = case a_comp of { Lt _ -> v1 ; Rt b_ore -> Rt (addition v1 b_ore) } which clearly is the usual algorithm for addition of unary natural numbers. How to run this program is described in detail in the tutorial.

Half-Strong and Strong Induction. The premise of the induction rule for the predicate N is logically equivalent to the conjunction of the induction base, P(0), and the induction step, ∀x (P(x − 1) → P(x)). The induction step slightly differs from the usual induction step since it lacks the additional assumption N(x). This discrepancy disappears in the following rule of half-strong induction and its associated extracted program ( f a, g a) and id Def = λa a. In the following example, halfstrong induction appears to be needed to extract a good program. We aim to prove that the distance of two natural numbers is a natural number

It is possible to prove this by (ordinary) induction on N(x), however, the proof is complicated and the extracted program contrived and inefficient. On the other hand, with half-strong induction (command hsind) the goal reduces to proving ∀y(N(y) → N(x − y)∨N(y − x)) from the assumptions N(x) and x = 0∨∀y(N(y) → N((x − 1) − y) ∨ N(y − (x − 1))) which, because of the extra assumption N(x), is relatively straightforward. Moreover, the extracted program is the expected one which removes successors from (realizers of) x and y until one of the two becomes 0 after which what remains of the other one is returned as result. The interested reader is invited to try this example on their own. Strong induction is similar to half-strong induction, however, the intersection with μ(Φ) is taken 'inside' Φ:

For the case of the natural numbers its effect is that the step becomes logically equivalent to ∀x (N(x) ∧ P(x) → P(x + 1)), that is, precisely the step in Peano induction. The extracted program corresponds exactly to primitive recursion.

Half-strong and strong coinduction will be discussed in Sect. 4.

As a rather large example, we formalize the existence of various exact representations of real numbers and prove the existence of conversions between them in Prawf.

We continue to work in the theory of real numbers implemented in Prawf through the batch real introduced in the previous section, but extend language, declarations and axioms as needed.

The structure of real numbers represented by the sort R and various constants and functions does not support any kind of computation on real numbers. For computation, we need representations. These can be provided in IFP through suitable predicates and their realizability interpretation, in a similar style as we represented unary natural numbers through the predicate N. In general, a representation is provided by defining a predicate P such that a realizer of P(x) is a representation of x.

Exact representations of real numbers are typically infinite sequences or streams which are naturally expressed through coinductively defined predicates. For example, the predicate S(x) meaning the existence of the signed digit representation of x, which is one of the standard representations of real numbers for computation, is expressed as follows. To give an impression how this looks in Prawf we use in the following machine notation where v stands for ∨, ex for ∃, m is a constant for −1, * is multiplication, and <= means 'less or equal'. This defines S as the largest predicate on the reals satisfying S = PhiS(S). A realizer of S(x) is an infinite stream of signed digits where a digit is a realizer of a formula of the form SD(y) that is either Lt(Lt(Nil)) or Lt(Rt(Nil)) or R(Nil) (representing −1, 0, 1). Streams are given as infinitely nested pairs, e.g. Another representation, called infinite Gray-code [12] , is defined through a coinductive predicate G(x) defined in Prawf by B:(R) = lambda (x:R) (x <= 0 v 0 <= x) D:(R) = lambda (x:R) (not (x = 0)) -> B(x) PhiG:(R) = lambda X:(R) lambda (x:R) (m <= x and x <= 1) and (D(x) and X(t(x))) G:(R) = Nu(PhiG)

Here, t:(R)->R is the tent function defined as t(x)=1-2*abs(x). An interesting and challenging aspects of the infinite Gray-code is the fact that it is partial, more precisely, a realizer of G(x) is a stream that may have one undefined element. This is due to the premise not (x = 0) in the definition of D which, if false (that is, x=0), will admit as realizer a program whose value is undefined (e.g. a program that loops infinitely).

Following [6] , we proved in Prawf

The proof is rather involved in that it consists of two coinductions, half-strong coinduction, and Archimedean induction, which is a special form of induction suitable for proving predicates with a premise where x << y is defined as 2*abs(x) <= 1 and y = 2*x. Accp is the accessible or wellfounded part of the relation <<. Using Brouwer's Thesis, which states that induction on a well-founded relation is valid, and the Archimedean property of the reals (see [6] ) one can show that Accp(x) holds for all nonzero x. Therefore, induction on Accp(x) turns into an induction principle for nonzero real numbers which in [6] is dubbed Archimedean induction. It is logically equivalent to the rule ∀x 0 ((|x| ≤ 1/2 → P(2x)) → P(x)) AI ∀x 0 P(x) Archimedean induction is used to prove all x:R (S(x) -> B(x)) which is the essential step in the proof of Claim1.

The proof of Claim2 uses half-strong coinduction which is the rule

Similarly, strong coinduction is the rule

This rule can be used to give a short proof of G(-x) -> G(x) and extract a simple program which negates the head of the input stream and leaves its tail untouched (instead of recursively reproducing the tail, which would happen with ordinary coinduction).

We presented Prawf, a first prototype implementation of the logical system IFP and its associated program extraction procedure. The successful formalization in Prawf of exact real number representations and formal proofs of their relationships guarantee the correctness of the proofs in [6] . This advanced case study also gives us evidence that our approach scales to substantial nontrivial problems.

The examples also demonstrate the enormous advantage gained from the possibility of describing different data representation in an abstract setting using only first-order logic, and postulating arbitrary true nc-axioms. In the formalization of infinite Gray-code it was also essential that our method is able to produce partial extracted programs.

We would like to point out that the Soundness Theorem, that is, the correctness proof for extracted programs, though constructive, is valid with respect to a classical semantics. This is in line with the attitude in constructive mathematics to produce only results that are constructively and classically valid, which is not necessary the case in other approaches to program extraction.

Despite its successful maiden voyage Prawf has some loose ends that need to be tied up. The most urgent one is an implementation of the soundness proof, that is, the enhancement of program extraction so that not only extracted programs but also their correctness proofs are created automatically. Currently, correctness relies on soundness as a meta theorem that has not been formalized yet. Other necessary improvements concern support for schematic theorems (Π 1 1 -theorems, essentially), advanced proof tactics and interpretations between different languages.

We also plan to extend Prawf by sequent calculus rules and rules that permit the extraction of concurrent programs. The latter will be needed to prove, conversely, that G (infinite Gray-code) is included in S (signed digit representation). We know from [12] that the extracted translation program has to be concurrent and nondeterministic.

Realisability for induction and coinduction with applications to constructive analysis

Minlog -a tool for program extraction supporting algebras and coalgebras

Optimized program extraction for induction and coinduction

Intuitionistic fixed point logic

Interactive theorem proving and program development

Implementing Mathematics with the Nuprl Proof Development System

Nuprl: an open logical programming environment: a practical framework for sharing formal models and tools

Real number computation through gray code embedding. Theor. Comput

Acknowledgements. This