Draft Extended Abstract

1 Abstract

In this paper we extend the Whelk proof development system of Wiggins92 with destructor functions. This Paper presented an implemented logic. It could be used for program transformation and the synthesize of relational, non-deterministic logic programs from a first-order logic specification.

Destructor functions allow proofs and programs to be broken down into their sub-parts, for instance one such function could map a program for A ∧ B to a program for just A or just B.

The addition of these functions has made the logic much more powerful and introduced the possibility of using it with theorem provers such as Clam [Ref to Clam] but it has also introduced new problems.

2 Introduction.

This paper is concerned with the synthesize of logic programs from first order logic specifications. That is taking a specification, regarding it as a proposition, and attempting to prove it with proof rules that build up a program, hence making a program and a proof of it’s correctness in a single go. Martin Löf introduced the idea of proofs as programs in his original work on type theory [Ref to Martin]. He show how to synthesize function programs from there proofs. Wiggins in [Ref to Whelk] carried out an adaptation of Martin Löf’s ideas to logic programs, in the form of horn clauses. Wiggins develops a logic based on Gentzen’s sequent calculus, which for reason that will remain obscure, is called Whelk. This logic lacks a complete set of elimination rules and therefore it is limited in power and scope. In this paper we add these rules but this presents new and interesting problems which we will address below.

The proof rules associate program terms with each sequent. So when applying a elimination rule to a proposition it is necessary to break down this proof term. To do this we use functions known as destructor functions, which will be applied to the proof terms, however it is the proposition that we look at when deciding where to apply these destructor functions. Therefore we need a to know the link between the proposition and its proof term but as there is more than one proof for any proposition this will never be a bijection.

Martin Löf gave us the correspondents between proofs and programs, and also propositions and specifications. We now find it necessary to find the lose correspondence between proposition and proof or programs and specifications.

In this paper we use the notion of proof and program interchangeably, indeed this is the very essence of program syntheses. In the next section we give an outline of the logic of [Ref]. In section 3 we describe the changes we have made to this logic that are not directly related to adding destructor function, these functions are given in section 4. Section 5 contains a worked example and finally we state our conclusion in section 6.

3 Outline of Whelk 92.

Based on logic of Gen69.

I though we could use sections 2.1, 2.2 and 2.3 from your Meta

92 paper. 1 +1/2 pages

4 Non destructor function changes from Whelk 92

Many revisions have been made to Whelk92 apart from adding destructor functions, these are outlined in this section.

A new rule has been added to introduce equality. Having to decide equality in the specification logic matches the notion of unification in logical languages: if it is possible to equate two variables, unification will do so and register as true otherwise it will be false. This leads to the rules:

\overline{Γ ⊢_{x=y} ∂(x = y)} ∂ = intro \frac{Γ, ∂(x = y)_{x=y} ⊢_{ϕ} A}{Γ ⊢_{ϕ} A} ∂ = elim

So now, as we deal with equality under ∂ with a rule it would seem odd to deal with equality outside a ∂ with axioms. So we use rules to decide equality of our basic types (bool’s, integers and lists). They are all of the form:

\overline{Γ ⊢ [ ] = [ ]} list = base \frac{Γ ⊢_{P(ε_{1})⌊ϕ} h1 = h2  Γ ⊢_{P(ε_{2})⌊ψ} t1 = t2}{Γ ⊢_{(P(ε_{1}joinε_{2})⌊ϕ∧ψ} [h1|t1] = [h2|t2]}

list = step

Another change concerns the introduction of implication: ). This can not be introduced under a ∂ as this would be incomplete (in the most general case a function with a infinite domain would require an infinite program hence producing code that will never terminate).

This leaves us with ) introduction out sided a ∂ and the question of what it actually means for one specification to imply another. We have taken the view that A ) B is a function that given a proof of A will produce a proof of B, hence we add lambda notation to our logic:

\frac{Γ, A_{α} ⊢_{ϕ} B}{Γ ⊢_{λα.ϕ} A ) B} ) intro \frac{Γ, B_{α(ψ)} ⊢_{ϕ} C Γ ⊢_{ψ} A}{Γ, (A ) B)_{α} ⊢_{ϕ} C} ) elim

5 Destructor functions.

Destructor functions map proofs to proofs, breaking them up into their composite parts. For instance given a proof of A ∧ B , ϕ say, it would be useful to be able to obtain a proof of A. However, A ∧ B might be proved by induction or by a call to another predicate so we can not simply pattern match the proof with α ∧ β, where α is a proof of A. So we use a destructor function l_{∧} which will correctly extract the appropriate proof. So given:

[[A ∧ B]]_{P(ε)⌊ϕ}

we many conclude:

[[A]]_{P(ε)⌊l_{∧} (ϕ)}

It is now our job to define these functions. For them to work nicely we want the proof, the program and the specification to have the same structure. But because we have a variety of different proofs (or programs) for a given proposition (or specification), if in fact have the structure of the proof reflecting the structure of the program which is only limited by the structure of the specification and this is where all the problems lie.

It is necessary to keep all information about how the proof is preformed. For instance, when a specification is always true or always false the final program will be simply true or false, respectively, however the proof of these programs might contain computational information we want to keep. Given programs to decide odd and even numbers and the specification:

P(n : nat) ⌊ even(n) ∨ odd(n)

Assigning the program true is correct but in doing this we would then lose the programs to test for odd and even numbers. So we introduce two new destructor functions: ∂_{true} and ∂_{false} which says that the program needed here is true or false but also preserve its internal structure.

\frac{Γ ⊢_{P(ε)⌊ϕ} A}{Γ ⊢_{P(nil)⌊∂_{true} (ϕ)} ∂A} ∂true \frac{Γ ⊢_{P(ε)⌊ϕ} ¬A}{Γ ⊢_{P(nil)⌊∂_{false} (ϕ)} ∂A} ∂false

Another possible disruption of the proof is introduced by induction. Induction introduces a case split into the proof term to distinguish between the base case and the step case, for instance, induction on natural numbers has to decide if it’s argument is 0 or a successor number leading to the proof term:

(n = 0 ∧ ϕ) ∨ (∃k.n = succ(k) ∧ ψ)

where ϕ is the proof of the base case and ψ is the proof of the induction case. This has put an ∨ into our proof term that did not come from an ∨-introduction rule. So when a destructor function encounters an ∨ in a proof term it will not be clear if it represent a case spilt or the proof of a conjunction. Our solution to introduced a new symbol into our logic: ∨_{ind} that behaves as ∨ but carries a mark to show it was introduced by induction. We now have the induction rule:

\begin{matrix}Γ ⊢_{P′(ε_{1})⌊ϕ} A[0/b] \\ Γ, k : nat, A[k/n]_{P′(ε′ join (ε_{1} merge ε_{2}))[k/n]} ⊢_{P′(ε_{2})⌊ψ} A[succ(k)/n] \\ Γ, n : nat ⊢_{P(ε_{1} merge ε_{2})⌊P′(ε‘ join (ε_{1} merge ε_{2}))} \\ _{where P′(ε′ join (ε_{1} merge ε_{2}))⌊(n=0∧ϕ)∨(∃k:nat.n=succ(k)∧ψ} ) A \end{matrix} Nat induction

In most cases there is only, really, one way to perform a proof. For instance to prove A ∧ B we must, at some point, prove A and prove B and join them with a ∧, likewise to be able to decide if A ∧ B is true or false we must be able to decide A and also decide B. Hence we have the introduction rules:

\frac{Γ ⊢_{P(ε_{1})⌊ϕ} A Γ ⊢_{P(ε_{2})⌊ψ} B}{Γ ⊢_{P(ε_{1} join ε_{2})⌊ϕ∧ψ} A ∧ B} ∧ intro

\frac{Γ ⊢_{P(ε_{1})⌊ϕ} ∂A Γ ⊢_{P(ε_{2})⌊ψ} ∂B}{Γ ⊢_{P(ε_{1} join ε_{2})⌊ϕ∧ψ} ∂(A ∧ B)} ∂ ∧ intro

and the elimination rules:

\frac{Γ, ∂(A_{r_{∧} (α)} ), ∂(B_{l_{∧} (α)} ) ⊢_{ϕ} C}{Γ, ∂(A ∧ B)_{α} ⊢_{ϕ} C} ∂ ∧ elim \frac{Γ, A_{r_{∧} (α)} , B_{l_{∧} (α)} ⊢_{ϕ} C}{Γ, A ∧ B_{α} ⊢_{ϕ} C} ∧ elim

Note the use of the new destructor functions r_{∧} and l_{∧} . r_{∧} will find the proof of the right conjunct, usually the right branch of the first ∧ expression:

r_{∧} (ϕ ∧ ψ)= ψ

But if the proposition was proved by an application of the ∂_{true} or ∂_{false} rule then we first must strip away the constructor and reapply the destructor function to the term under it:

\begin{matrix}r_{∧} (∂_{true} (ϕ)= & r_{∧} (ϕ)) \\ r_{∧} (∂_{false} (ϕ)= & r_{∧} (ϕ)) \end{matrix}

Another case is if the proposition as been proven by making a sub-call, in which case we simply apply the destructor function to the proof of the sub-call:

r_{∧} (defn[X])= r_{∧} (ϕ)

where defn[X] ⌊ ϕ

Finally the proposition may have been proven using induction, so we have a case split. Therefore we apply the destructor function to each of the cases:

r_{∧} ((G_{1} ∧ ϕ) ∨_{ind} (G_{2} ∧ ψ)) = (G_{1} ∧ r_{∧} (ϕ)) ∨_{ind} (G_{2} ∧ r_{∧} (ψ))

l_{∧} follows symmetrically. Destructor function for other elimination rules are also defined in a similar way.

5.0.1 The ∨ Rule

Our first interesting problem arises when trying to break down a proof of ∂(A ∨ B) this is because there are three distinct ways to prove a proposition of this form: i) from ∂A and ∂B, ii) from A, and iii) from B. So a program for ∂(A ∨ B) may not have the information for programs for both ∂A and ∂B. For instance:

∂(true ∨ otherprog)

can be proved by ∂_{true} introduction then left ∨ introduction, giving no information about otherprog. Therefore no destructor function, however complicated, can extract a program for it. We solve this, in our current implementation, by introducing the constructs isl and isr when performing ∨ introduction:

\frac{Γ ⊢_{P(ε_{1})⌊ϕ} ∂A Γ ⊢_{P(ε_{2})⌊ψ} ∂B}{Γ ⊢_{P(ε_{1} join ε_{2})⌊ϕ∨ψ} ∂(A ∨ B)} ∂ ∨ intro

\frac{Γ ⊢_{ϕ} A}{Γ ⊢_{isl(ϕ)} A ∨ B} ∨ intro(left)  \frac{Γ ⊢_{ϕ} B}{Γ ⊢_{isr(ϕ)} A ∨ B} ∨ intro(right)

and the elimination rule:

\frac{Γ, ∂(A_{r_{∨} (α)} ), ∂(B_{l_{∨} (α)} ) ⊢_{ϕ} C}{Γ, ∂((A ∨ B)_{α}) ⊢_{ϕ} C} ∂ ∨ elim

The destructor functions can now do a test to see if they are applicable.

\begin{matrix}r_{∨} (ϕ ∨ ψ)  = & ψ \\ r_{∨} (isr(ϕ))  = & ϕ \\ r_{∨} (isl(ϕ))  = & or error \\ r_{∨} (∂_{true} (ϕ))  = & r_{∨} (ϕ) \\ r_{∨} (∂_{false} (ϕ))  = & r_{∨} (ϕ) \\ r_{∨} ((G_{1} ∧ ϕ) ∨_{ind} (G_{2} ∧ ψ)) = & (G_{1} ∧ r_{∧} (ϕ)) ∨_{ind} (G_{2} ∧ r_{∨} (ψ)) \\ r_{∨} (defn[X])  = & r_{∨} (ϕ) \end{matrix}

where defn[X] ⌊ ϕ

and (G_{1} ∧ ϕ) ∨_{ind} (G_{2} ∧ ψ) is a proof of A ∧ B for some A and B.

These rules have been used to synthesize non-trivial programs, see the example section for one. But care is required in there use, it is necessary to remember each ∨ under ∂ was proved. Worst of all it can lead to run time error in meta level of synthesized programs. A better solution would be to alter our notion of ∨ introduction to include proof or disproof of each branch of the lor. i.e. replace the left ∨ intro and right ∨ intro rules with 3 new rules of the form:

\frac{Γ ⊢ A  Γ ⊢ B}{Γ ⊢ A ∨ B} \frac{Γ ⊢ A  Γ ⊢ ¬B}{Γ ⊢ A ∨ B} \frac{Γ ⊢ ¬A  Γ ⊢ B}{Γ ⊢ A ∨ B}

Hence giving us all the information we need to carry out true ∨ elimination. We could also use the more complicated rule:

\frac{Γ ⊢ ∂(A ∨ B) Γ ⊢ (∂(A) ) C) Γ ⊢ ∂(B) ) C}{Γ ⊢ C}

Where orapp will look at the proof of A ∨ B to decide which transformation to apply. This rule is closer the Gentzen’s sequent calculus than the one given above but forcing the user to prove both implications means it is less powerful.

5.1 Substitution Rules

An underlying theme of these rules is that the structure of the proof should in some way reflect the structure of the proposition. However substitution can interfere with this. Simply substitution B ∧ A for A ∧ B with out any other changes would muddle up the proofs of A and B. But implication gives us a way of transforming proofs. So we require a rule along the lines of:

\frac{Γ ⊢_{P(ε_{1})⌊ϕ} B ) A  Γ ⊢_{P(ε_{2})⌊ψ} A ) B  Γ ⊢_{P(ε_{3})⌊θ} B}{Γ ⊢_{P(ε_{1} join ε_{3})⌊ϕ(θ)} A} ⌊ sub

But there is another problem here. We have no rules for the elimination or introduction of a ∀ under a ∂, us such a rule would be incomplete. Our normal way to deal with this is to use substitution to find an equivalent proposition that is easier to break down.

However, we could not make these substitutions, using the rules above, until we proved them valid, which would involve performing another proof under a ∂ and a ∀ which would be impossible with out a substitution, hence this rule would never be usable. Providing axioms to cover every conceivable situation would not be practical so we need a rule of the form:

\frac{Γ ⊢_{P(ε_{1})⌊ϕ} B ) A  Γ ⊢_{P(ε_{2})⌊ψ} A ) B  Γ ⊢_{P(ε_{3})⌊θ} C}{Γ ⊢_{P(ε_{1} join ε_{3})⌊progsub(θ,B,ϕ)} C[A/B]} ⌊ sub

where progsub will replace any proof of B, (β say) with θ(β). This involves the nontrivial problem of recognizing proofs of B. One possible way of doing this might be to annoyed each part of the proof as it is done to say what it proves. Unfortunately we have not had enough time to implement this. So for the time being we will use the rule:

\frac{Γ ⊢_{P(ε_{1})⌊ϕ} B ) A  Γ ⊢_{P(ε_{2})⌊ψ} A ) B  Γ ⊢_{P(ε_{3})⌊θ} C}{Γ ⊢_{P(ε_{1} join ε_{3})⌊θ} C[A/B]} ⌊ sub

and ask the user to ensure that they do not destroy any structure that is relied upon by any destructor function they use. Although by no means perfect this will let me demonstrate the system without have to implement the progsub function above.

6 Working Example.

2 pages As an example I will synthesize the subset predicate from the specification:

∀(k : nat list.∀(l : nat list.∂(∀(x : nat, x ∈ k ) x ∈ l))

A full proof is not possible here, but I will give it’s structure and the important proof steps and terms.

7 Conclusion and further work.

We have added destructor functions to a synthesis logic and this has given us a clear idea of the problems involved. We have also given the first formal definition of the ∂ = rule.

This has produced a logic much more sophisticated than that of the original Whelk logic [Ref to Wiggins92]. But we leave much work to be done, notably formulating new rules for ∨ and substitution along the lines we have described.

Further work might involve using this logic with the Clam proof planner to automatically synthesize programs. Our work his been an important first step to this as proof planers such as Clam require destructor function.

Another step might be to an automate the translation of our runable logic code into a real logic language such as Prolog of Godel.