Proofs-as-Programs Method

In this chapter, we develop the Proofs-as-Programs Method, which adds atoms to a logic algorithm so that some correctness criteria wrt a set of properties become satisfied. This method is part of our tool-box of methods for instantiating the predicate-variables of a schema. First, in Section 9.1, we state the problem. Then, in Section 9.2, we explain a method to solve this problem, and discuss its correctness in Section 9.3. In Section 9.4, we illustrate this method on a few sample problems. Future work and related work are discussed in Section 9.5 and Section 9.6, respectively, before drawing some conclusions in Section 9.7. 

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. 

SLD resolution is parameterized on a computation rule and a search rule [Lloyd 87]. For extended execution, these rules are, for the purpose of the Proofs-as-Programs Method, instantiated as follows ... 

The problem statement of the Proofs-as-Programs Method requires that LA r) be complete wrt P(r), and this, in retrospective, according to the new criterion (1). Indeed, there wouldn t exist any complete syntactic specialization otherwise. But in practice, it is often impossible to know beforehand whether this constraint is satisfied... 

Definition 9-5 The Proofs-as-Programs Method succeeds iff LA r) is proven (by extended execution) to be complete wrt P(r). It fails otherwise. 

So far for the proof aspects of the Proofs-as-Programs Method. Let s now turn to the condition extraction aspects. 

The Proofs-as-Programs Method is deterministic because the results of all successful derivations are collected before computing 21 therefrom. The method is thus independent of any ordering of disjuncts within LA r), or of properties within P(r). The method may fail, as conveyed by Definition 9-5. However, nothing can be said about the synthesized logic algorithms in terms of determinism or finiteness, because nothing is known about the properties. 

The research related to our Proofs-as-Programs Method can be separated into two parts the motivation for the terminology used in naming this method, as well as the discussion of other methods that solve the same (or a similar) problem as the one defined here. 

Our Proofs-as-Programs Method is not like the other methods of program extraction from proofs (see Chapter 2), since the program is here extracted from the unique final... 

In terms of methods that solve the same (or a similar) problem as the one tackled by our Proofs-as-Programs Method, there first is the method described by [Smith 82] given two formulas F and G, the objective is to find the weakest pre-condition P such that G follows from F a P. Taking F as the initial logic algorithm, G as the property set, and F a P as the final logic algorithm, this problem is a sub-case of ours, because F, G, P are here sets of formulas. Smith s proofs are performed by natural deduction. 

In this chapter, we have presented the Proofs-as-Programs Method, which adds atoms to (and hence specializes) a logic algorithm so that it is complete wrt a set of given properties. The added atoms are extracted from the proof that the initial logic algorithm is already complete wrt these properties. 

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.

An instantiation of the Discriminate/, predicate-variable tests the values of HX, TX, Y in order to see whether ProcComp/ is applicable. Step 7 yields LA-/ r) by invoking the Proofs-as-Programs Method (see Chapter 9) and generalizing its results via some heuristics. 

For instance, in our case the Proofs-as-Programs Method performs as shown in Example 9-4, where the following instances of Discriminate/ are synthesized ( = 2,...,3) ... 

Note that the Proofs-as-Programs Method wouldn t need to prove that the examples are logical consequences of the input logic algorithm, as we know that LA (r) is already complete wrt Cfr). Moreover, such proofs would result in very specialized discriminants, and hence in the need for considerable generalization afterwards. But the presence of some examples is often necessary within the theories, so that DC/ may reduce atoms of predicate rin in case no property is applicable. The following definition and heuristic capture this ... 

Heuristic 13-6 At Step 7, only provide the properties and property-examples of EP r) as input property set to the Proofs-as-Programs Method. 

Example 13-11 For the compress problem. Step 7 proceeds as in Example 9-4. There is one property-example, namely Ej, so Heuristic 13-6 provides E and the properties of EP(compress) as a property-set to the Proofs-as-Programs Method. The applied generalization heuristics are Heuristic 13-3, Heuristic 13-4, and Heuristic 13-5, respectively. The resulting logic algorithm and its expansion are shown in Example 11-1. 

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. 

---