# Prawf: An Interactive Proof System for Program Extraction

- 3 Mentions
- 67 Downloads

## Abstract

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.

## 1 Introduction

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 \(\mathrm {IFP}\) (Intuitionistic Fixed Point Logic) was introduced whose primary goal is program extraction. \(\mathrm {IFP}\) is first-order logic extended with least and greatest fixed points of strictly positive predicate transformers. Program extraction in \(\mathrm {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 \(\mathrm {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 \(\mathrm {IFP}\) and program extraction in \(\mathrm {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.

## 2 Program Extraction in \(\mathrm {IFP}\)

*Syntax and Proofs.*The syntax of \(\mathrm {IFP}\) has

*terms*,

*formulas*,

*predicates*and

*operators*, the latter describing strictly positive (s.p.) and hence monotone predicate transformers. For every s.p. operator \(\varPhi \) there are predicates \(\mu \,\varPhi \) and \(\nu \,\varPhi \) denoting the predicates defined inductively resp. coinductively from \(\varPhi \):where \({\varvec{P}}\)

*is s.p.*

*in*Open image in new window if every free occurrence of \({\varvec{X}}\) in \({\varvec{P}}\) is at a

*s.p. position*, i.e. not in the premise of an implication.

The proof rules of \(\mathrm {IFP}\) are the usual rules of intuitionistic first-order logic with equality (regarding equality as binary predicate constant) augmented by rules stating that \(\mu \,\varPhi \) and \(\nu \,\varPhi \) are the least and greatest fixed points of \(\varPhi \) (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 \(\lambda \)-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,\ldots ,a_k) \rightarrow q\) in which

*C*is a

*constructor*, i.e. one of \(\mathbf {Nil}, \mathbf {Lt}, \mathbf {Rt}, \mathbf {Pair}\), and the \(a_i\) are pairwise different program variables binding the free occurrences of the \(a_i\) in

*q*. \(\mathbf {rec}\,p\) computes the (least) fixed point of

*p*, hence \(p\,\mathbf {rec}(p)=\mathbf {rec}(p)\). It is well-known that an essentially equivalent calculus can be defined within the pure untyped \(\lambda \)-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 \(\rightarrow ^{+}\), ‘\(a:A\vdash \)’indicates that the assumption *A* in the proof has been assigned the program variable *a*. In the rule \(\wedge _L^{-}\), \(\mathbf {proj}_{L}(p)\) stands for the program \(\mathbf {case}\,p\,\mathbf {of}\,\{\mathbf {Pair}(a,b)\rightarrow a\}\). Similarly for \(\wedge _R^{-}\). The rules \(\forall ^+\) and \(\exists ^{-}\) are subject to the usual provisos. In the rules ind and coind the program \(m_\varPhi \) realizes (in a sense explained below) the monotonicity of \(\varPhi \), that is the formula \(X\subseteq Y \rightarrow \varPhi (X)\subseteq \varPhi (Y)\) (with fresh predicate variables *X*, *Y*).

The correctness of programs is expressed through a realizability relation \(p\,\mathbf {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 \(\mathbf {R}(A)\) on a Scott domain *D* of ‘potential realizers’. \(p\,\mathbf {r}\,A\) means that the denotation of *p* in *D* satisfies the predicate \(\mathbf {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 \(\mathrm {RIFP}\) that extends \(\mathrm {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-\(\bot \) 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 \(\mathbf {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 \(\mathrm {IFP}'\) whose induction and coinduction rules require as additional premise a proof of the monotonicity of \(\varPhi \), e.g., Soundness is then proven for \(\mathrm {IFP}'\) and transferred to \(\mathrm {IFP}\) via an embedding of \(\mathrm {IFP}\) into \(\mathrm {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. \(\forall x\,(x+0=x)\) and \(\forall x\,(x \ne 0 \rightarrow \exists y\,(x*y=1))\)).

*Computation vs. Equational Reasoning.* 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 \(\mathrm {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].

## 3 Prawf

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 \(\mathrm {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\):

*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: The program transforms realizers of \(\mathbf {N}(x)\) and \(\mathbf {N}(y)\) into a realizer of \(\mathbf {N}(x+y)\). By the inductive definition of the predicate \(\mathbf {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): 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 \(\mathbf {N}\) is logically equivalent to the conjunction of the

*induction base*, \(\mathcal {P}(0)\), and the

*induction step*, \(\forall x\,(\mathcal {P}(x-1)\rightarrow \mathcal {P}(x))\). The induction step slightly differs from the usual induction step since it lacks the additional assumption \(\mathbf {N}(x)\). This discrepancy disappears in the following rule of

*half-strong induction*and its associated extracted program where \(\langle f,g\rangle \,{\mathop {=}\limits ^{\mathrm {Def}}}\, \lambda a\,\mathbf {Pair}(f\,a,g\,a)\) and \(\mathbf {id}\,{\mathop {=}\limits ^{\mathrm {Def}}}\,\lambda a\,a\). In the following example, half-strong 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

*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 \(\mu (\varPhi )\) is taken ‘inside’ \(\varPhi \): For the case of the natural numbers its effect is that the step becomes logically equivalent to \(\forall x\,(\mathbf {N}(x) \wedge \mathcal {P}(x)\rightarrow \mathcal {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.

## 4 Case Study: Exact Real Number Representations

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 \(\mathrm {IFP}\) through suitable predicates and their realizability interpretation, in a similar style as we represented unary natural numbers through the predicate \(\mathbf {N}\). In general, a representation is provided by defining a predicate \(\mathcal {P}\) such that a realizer of \(\mathcal {P}(x)\) is a representation of *x*.

*Archimedean induction*. It is logically equivalent to the rule Archimedean induction is used to prove Open image in new window which is the essential step in the proof of Claim1.

*half-strong coinduction*which is the rule where \([f+g] \,{\mathop {=}\limits ^{\mathrm {Def}}}\,\lambda a\,\mathbf {case}\,a\,\mathbf {of}\,\{\mathbf {Lt}(b) \rightarrow f\,b;\,\mathbf {Rt}(c)\rightarrow g\,c\}\). Similarly,

*strong coinduction*is the rule This rule can be used to give a short proof of Open image in new window 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).

## 5 Conclusion

We presented Prawf, a first prototype implementation of the logical system \(\mathrm {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 (\(\varPi ^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.

## Footnotes

- 1.
‘Prawf’ (pronounced /prau̯v/) is Welsh for ‘Proof’.

## Notes

### Acknowledgements

## References

- 1.Isabelle. https://isabelle.in.tum.de/
- 2.Agda official website. http://wiki.portal.chalmers.se/agda/
- 3.Berger, U.: Realisability for induction and coinduction with applications to constructive analysis. J. Univ. Comput. Sci.
**16**(18), 2535–2555 (2010)MathSciNetzbMATHGoogle Scholar - 4.Berger, U., Miyamoto, K., Schwichtenberg, H., Seisenberger, M.: Minlog - a tool for program extraction supporting algebras and coalgebras. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 393–399. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22944-2_29CrossRefzbMATHGoogle Scholar
- 5.Berger, U., Petrovska, O.: Optimized program extraction for induction and coinduction. In: Manea, F., Miller, R.G., Nowotka, D. (eds.) CiE 2018. LNCS, vol. 10936, pp. 70–80. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94418-0_7CrossRefGoogle Scholar
- 6.Berger, U., Tsuiki, H.: Intuitionistic fixed point logic (2019). Unpublished manuscript available on ArXivGoogle Scholar
- 7.Bertot, Y., Castéran, P.: Interactive theorem proving and program development (2004)Google Scholar
- 8.Constable, R.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Upper Saddle River (1986)Google Scholar
- 9.The Coq Proof Assistant. https://coq.inria.fr
- 10.Lockwood, J.: Nuprl: an open logical programming environment: a practical framework for sharing formal models and tools. Program extraction (1998). http://www.nuprl.org
- 11.Prawf official website. https://prawftree.wordpress.com/
- 12.Tsuiki, H.: Real number computation through gray code embedding. Theor. Comput. Sci.
**284**(2), 467–485 (2002)MathSciNetCrossRefGoogle Scholar