Proofs-as-programs synthesis

The proofs-as-programs approach to program synthesis—also classified as constructive synthesis—is based on the Curry-Howard isomorphism [Howard 80], which states that there is a one-to-one relationship between a (constructive) proof of an existence theorem and a program that actually computes witnesses of the existentially quantified variables of the theorem. Given a specification in the functional form  

Inputs 3 Outputs Pre Inputs) = Fost Inputs, Outputs) the idea is to proceed in two steps  

The two approaches have complementary advantages and drawbacks interpretation is not as efficient as the execution of a compiled version, but the choice of a target language might obscure computational properties of proofs. 

In any case, the crux is of course the state-of-the-art in theorem proving the key issues are soundness of the synthesis (entailing correctness, completeness, and possibly termination of the resulting programs), deductive power (provability for an entire class of statements, extractability of whole families of programs for the same specification), and efficiency (need for proof planning in order to control the huge search space). Traditional theorem pro vers, such as the one of [Boyer and Moore 79], are inadequate due to their inability to reason constructively about existential quanti- 

There is an obvious interest in proofs-by-induction, because these allow the synthesis of recursive programs. Note that there often is a similar proof content in transformational synthesis and proofs-as-programs synthesis, and it seems that the same proof construction techniques should be applicable to both. This may suggest that these approaches are probably two facets of the same process. For instance, the work of [Neugebauer 93] shows how the specification forms of these approaches may be reconciled. 

---

Since deductive inference is generally a familiar notion, we do not survey it here. We rather directly propose a taxonomy of the different ways of applying deductive inference to program synthesis from axiomatic specifications. Thus, Sections 2.2.1 to 2.2.3 respectively contain general introductions to transformational synthesis, proofs-as-programs synthesis, and schema-guided synthesis. 

Compared to transformational synthesis, there is no problem here about when to stop synthesis halts when the proof is completed. Transformational synthesis seems more appropriate for synthesis from specifications that are almost programs (in which case synthesis is more like an optimizing transformation), whereas proofs-as-programs synthesis seems more appropriate for synthesis from highly descriptive specifications. Note that program transformation may actually be performed by the transformation of synthesis proofs. 

As mentioned above, the probably first proofs-as-programs synthesis systems are QA3 Question-Answering system) of [Green 69], and the PRO gram Writer (PROW) of [Waldinger and Lee 69]. In the latter, a post-proof processor extracts LISP programs from constructive existence proofs. 

In Chapter 2, we survey the use of deductive inference in automatic programming. Axiomatic specifications are expected to be complete and non-ambiguous, but are usually also quite lengthy and artificial. Deductive synthesis from axiomatic specifications can be classified into transformational synthesis, proofs-as-programs synthesis (or constructive synthesis), and schema-guided synthesis. We survey the achievements of deductive synthesis of LISP functions and Prolog predicates. 

First of all, let s remark that our Proofs-as-Programs Method is totally unlike classical proofs-as-programs approaches to algorithm synthesis (see Chapter 2). Indeed, we here adopt the liberal viewpoint that any technique that extracts some computational contents from a proof may be seen as a proofs-as-programs technique. 

Schema-guided synthesis was argued for in Section 8.1 because schemas are an interesting way of incorporating algorithm design knowledge into a synthesis process. Schema-guided synthesis is naturally a stepwise synthesis, as the predicate-variables are not all instantiated at the same time. A most interesting approach was then advocated in Section 8.3, namely to deploy an entire tool-box of predicate-variable instantiating methods, rather than a unique method. In Chapter 9 (Proofs-as-Programs Method) and Chapter 10 (MSG Method), we described two of the more sophisticated methods we have developed so far. Note that these methods are entirely dissociated from specific schemas or predicate-variables.

In Section 11.1, we have constrained the bodies of logic algorithms and properties to be free of negation, namely because the Proofs-as-Programs Method (which is used by Step 7 of the synthesis mechanism) cannot handle negation. As outlined in Section 9.5, this method could be extended to handle negated atoms that have primitive predicates, which would thus overcome the overall restriction. 

While the pre-synthesis work has to be performed once, the post- synthesis work is to be done for each concrete synthesis result. We therefore have to care for efficiency and automation of the verification procedure. For this task we do not use automatic decision procedure provided as contributions to the HOL system. Instead we first implement our own proving procedures as tactics and conversions in HOL. These tactics and conversions are then incrementally lifted to meta levels, i.e. they are first implemented in SML and then translated to C programs. That means, that proofs of subtheorems initially performed within the HOL logic may be also performed by decision procedures at meta levels, which then introduce the subtheorem as an axiom to the HOL proof. Deciding a property at the meta level is much faster than performing the... 

---