A Constructive Logic for Synthesising Logic Programs

Tom Chothia

March 10, 1999

Contents

1 Introduction 4

2 Background 4 2.1 Logics and Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Constructive Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Literature Review 6 3.1 The Constructive Type Theory of Martin-Löf or Proofs as Programs …. 6 3.2 The synthesis of Logic programs . . . . . . . . . . . . . . . . . . . . . . . . 9 3.3 K.K. Lau and S.D. Prestwich: Top down Synthesis of Recursive Logic Pro-

cedures from First order Logic Specification. . . . . . . . . . . . . . . . . . 9 3.4 L. Fribourg Extracting logic programs from proofs that use extended Prolog

execution and induction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.5 G. Wiggins: Synthesis and Transformation of Logic Programs in the Whelk

Proof Development System. . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.5.1 Evaluation of [Wig92] . . . . . . . . . . . . . . . . . . . . . . . . . . 19

4 Changes to be Made 20

5 Notation 20 5.1 Hypotheses Constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

6 The Rules 22 6.1 ∧ and ∨ Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 6.2 ∂_{true} and ∂_{false} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 6.3 ¬ Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6.4 Axiom, Lemma and Cut . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6.5 ∀ and ∃ Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 6.6 ) Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 6.7 = Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 6.8 Substitution Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 6.9 Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

7 The Destructor Functions and Other Syntax 29 7.1 A Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 7.2 The Destructor Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

7.2.1 r_{∧} and l_{∧} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 7.2.2 r_{∨} , l_{∨} , isr and isl . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 7.2.3 Lambda: λ and Apply: ( ) . . . . . . . . . . . . . . . . . . . . . . 31 7.2.4 subs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 7.2.5 Lex: l_{∃}, Rex: r_{∃}, and exists proof: ( , ) . . . . . . . . . . . . . . . 32 7.2.6 Decides true and false: ∂_{true} , ∂_{false} . . . . . . . . . . . . . . . . . . 32

7.3 Other Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 7.3.1 induction or: ∨_{ind} . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 7.3.2 Join and Merge . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

8 Implementation 33 8.1 The Implementation Method . . . . . . . . . . . . . . . . . . . . . . . . . . 33 8.2 Work Carried Out . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

9 Examples 35 9.1 The Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 9.2 The Program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

10 Conclusion and Further Work 49 10.1 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 10.2 Further Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

A Martin-Löf Type Theory Rules and Language 51 A.1 General Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 A.2 Cartesian Product of a Family of Types . . . . . . . . . . . . . . . . . . . . 52 A.3 Disjoint Union of a Family of Types . . . . . . . . . . . . . . . . . . . . . . 52 A.4 The Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

B The Rules of [Wig92] 54 B.1 Axiom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 B.2 ∃ Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 B.3 ∀ Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 B.4 ∧ Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 B.5 ∨ Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 B.6 ) Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 B.7 ∂ Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 B.8 ∀ Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 B.9 ¬ Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 B.10 ∨ Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 B.11 Induction on Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 B.12 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 B.13 New Hypotheses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

C Two Coded Rules 56 C.1 ∂_{true} introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 C.2 ∀ elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

Abstract

The aim of this project is to develop a proof system for synthesising logic programs. This is a method of extracting programs from proofs of their specification. It is also generally know as Proofs-as-Programs [ML84] and [Con82]. I present a new calculus that is an extension of the work in [Wig92]; it makes full use of destructor functions and synthesises non-deterministic relational logic programs. I also discus its implementation in the Mollusc system [RKSW94] and give some running examples.

1 Introduction

In this paper I present a calculus which can synthesise non-deterministic, relational logic programs. One way of doing program synthesis is to extracting programs from proofs. This involves a user performing a constructive proof of the specification, of the program they wish to have and in return they will get a program that fulfils that specification. It is based on the proofs as programs work of [ML84] and is an extension of the work done in [Wig92]. When developing the logic of [Wig92] compromises were made in its design. For example given a proof, or a program, there is no way to break it down into its subparts which would often be useful in further proofs or other programs. The work give here aims to lift this and other restrictions to allow completely general styles of proof.

Section 3 provides background on classic, functional program synthesise and on logics in general. Section 4 looks at other attempts to synthesise logic programs. Section 5 outlines what I have had to do. In section 6, I define my notation and I give the rules for my calculus in section 7. Section 8 describes how the non-standard functions I have used compute. Any implementation of the calculus is described in section 9 and examples presented in section 10. Section 11 contains my conclusion and further work.

2 Background

I will assume knowledge of first order Predicate calculus and lambda calculus such as that found in [Ham78] and [Bar84].

2.1 Logics and Calculi

A calculus and logic is a formal system of rules for manipulating mathematical symbols. A logic is calculus with a truth functional semantics. A sequence of these rules is said to be a proof of the final mathematical object produced. The first such system was developed by Euclid around 300 BC [EucBC]. It dealt with simple geometric construction and had rules that where deemed to be obvious such, as “any two points can be joined by a line”. Euclid provided many proofs in this system, such as “if you are given a square you can produce a square of twice the area”.

Later calculi where introduced to deal with provability in general. These calculi also have simple rules that are deemed to be obviously true, such as Modus ponens (or MP) which states that if we know A is true and we know A implies B, we may conclude B. A conventional way of writing this is to put what you know above a line and what you can conclude below it, or equivalently what you wish to be true below the line and the necessary pre-conditions above it. So MP can be written:

\frac{A ) B A}{B} MP

In a sequent calculus each assertion may include a possibly empty list of hypotheses. An assertion can then be written as a sequent:

ListofHypotheses ⊢ Conclusion

Where the ⊢ means that given the hypotheses there exists a proof of the Conclusion. Of course a statement proved in this way is not proven true in the world in general but

just in the enclosed logic system.

A set of rules is said to be sound if and only if any formula derivable from a noncontradictory theory is true with respect to that theory. This is a vital property which I will expect from all logics used and put forward in this paper. However proofs of soundness are beyond the scope of this paper

2.2 Constructive Logics

A calculus is known as constructive if propositions are proved by producing an example of what is required to be true. For instance a constructive proof that there exists a prime above 100 would be to observe that 113 is prime. A non-constructive proof might observe that there is an infinite number of natural primes and finite number of naturals below 100. The constructive condition means that many proposition that rely on negation can not be proved, such as: It is always true that:

A ∨ ¬A

or that

¬(¬A) ) A

Constructive logics are particularly useful in synthesising programs as we always wish to be given an example of the program specified rather than be assured that one exists.

3 Literature Review

3.1 The Constructive Type Theory of Martin-Löf or Proofs as Programs

The work of Martin-Löf was based on the observation that a proposition in intuitionistic Predicate calculus, a data type and a specification of a computing problem or task can in fact be regarded as the same thing. The equivalents of the first two was show by [Cur58], [How58]. The equivalence of tasks and propositions was known as early as the 1930’s, [Kol32], but as this was before the advent of modern computers its significance was neglected. Function can be specified in the ∀∃ form e.g.:

∀x : nat.∃y : nat.x^{2} = y

• As a proposition this means that for every number there exists another number which is the square of the first.

• As a programming task this specifies the program that takes a number as input and returns its square.

• As a data type it is the data type of all functions that map a number to its square.

This leads to the much more important observation that the following are equivalent

a is an object of type A a is a constructive proof of a proposition A and a is a program to solve a task A.

This trinity is fundamental to all of the work that follows. All of the proof rules and theorems can be thought of as applying in each or all of these ways. I shall use them interchangeably. Hence given a specification of a program the appropriate set of rules can be applied to produce a proof, which in turn will automatically produce a program. This is known as program synthesis. The term “Programs as Proofs” was coined by Bob Constable in [Con82] and subsequently corrupted to its more common form: “Proofs as Programs”.

Any programs developed from a system with a proof of soundness have the benefit of being automatically correct (with regard to their specification). Given a good understanding of logic and proof methods it is often easier to synthesise programs using proof rules than it is to write them directly in the computer language. Proofs are usually quite simple and they can be automated or guided. It is sometimes the case that the proofs can be done completely by a proof planner such as CLAM [BvHHS90]. So we are presented with a situation where we simply give a computer a specification of the program we want and it will return the finished code. Martin-Löf outlines these ideas in [ML84].

The paper starts with a brief discussion of what constitutes a high and a low level language. This leads into a comparison of constructive mathematics and high level languages. Martian-Löf points out that these are essentially the same. Differences that do exists are due to the computer scientists’ insistence that computer languages should consist of very formal notation that can be easily executed by machine and the mathematicians habit of leaving trivial computational details implicit in proof. A table that accompanies his paper nicely illustrates this similarity:

Programming  Mathematics
Program  Function
Output  Value
X := e  x = e
S_{1}; S_{2}  Composition of functions
If B then S_{1} else S_{2}  Definition by cases
while B do S  Definition by recursion
Data structure  Element, Object
Data type  set, type
Value of a data type {  Element of a set

Object of a type {

a : A  a ∈ A
Integer  Z
Real  R
Boolean  0,1
(c_{1}, c_{2}, ...c_{n})  {c_{1}, c_{2}, ...c_{n}}
Array [I] of T  T^{I},I ) T
record s_{1} : T_{1}; s_{2} : T_{2}{  T_{1}xT_{2}
record case s : (c_{1}, c_{2}) of c_{1} : (s_{1} : T_{1}); {
c_{2} : (s_{2} : T_{2}) end  T_{1} + T_{2}
set of T  {0, 1}^{T}, T ) 0, 1

To make use of this observation Martin-Löf gives a typed λ-calculus [Bar84] and a set of proof rules that will generate programs in this language. Applying the rules to prove the proposition produces a program. The program always reflects the proof therefore different proof styles will produce different programs: quick-sort and exponential time sort can both be synthesised from the same specification. The language is given in full in appendix A. Martin-Löf points out that the normal way of evaluating mathematics (from the inside outwards) is not possible for expressions in this system. For instance in (λx.b).a it is impossible to evaluate b before replacing the x with the a. Hence λx.b can not be reduced at all. This will also present a problem when trying to synthesise logic programs.

The proof rules are given in the natural deduction style and I give then in full in appendix A. Martin-Löf approaches these from a type theorist‘s point of view, so Cartesian product of types (Π) is used instead of universal quantification (∀) and implication ()), disjoint union of a family of types (Σ) instead of existential quantification (∃), disjoint union of two types (+) instead of disjunction and conjunction is a special case of disjoint union of a family of types. I give the disjunction rules here as they to illustrate the way in which the all the rules work.

\frac{a ∈ A}{i(a) ∈ A + B} + introduction  \frac{b ∈ B}{j(b) ∈ A + B} + introduction

These rules describe how it is possible to:

construct a object of type A + B make a proof of A ∨ B or build a program, which does A ∨ B.

A disjunction is proved by proving one of its two sub-branch. The i and j work as markers to show which part of the proposition has been proved. + can be eliminated from a proof using the following rule:

\frac{c ∈ A + B d ∈ C(i(x)/z) e ∈ C(j(y)/z)}{(Dx, y)(i(a), d, e) ∈ C(c/z)} + −elimination

D is, in fact, an operator in the language where as A, B, C are data types, propositions or specifications, depending on how you like to think of these things. So looking at this from the computational point of view it says to produce a program that will do C with x replaced by c you must:

• show that c will do A or B.

• find a program d that does C with i(x) in place of z

• find a program e with does C with j(y) in place of z.

Then the piece of code you want is (Dx, y)(c, d, e). (see appendix A for the evaluation rules for D, they are, as you would expect).

3.2 The synthesis of Logic programs

The work of Martin-Löf covered the synthesis of functional programs, indeed he is still a leading authority on the field today. Functional languages are the most obvious to synthesis because of the clear correspondence between β-reduction and ( elimination. This is known as the Curry-Howard isomorphism [Cur58], [How58]. But logic languages do not use β reduction so this is no longer any use to us.

If logic programs were to be regarded as deterministic functions then they too could be in the same way but then we would lose the non-deterministic and backtracking abilities that make logic languages so useful. Therefore a different method is needed.

3.3 K.K. Lau and S.D. Prestwich: Top down Synthesis of Recursive Logic Procedures from First order Logic Specification.

Lau and Prestwich [LP90] approach the synthesis of programs from a much more mechanical and much simpler point of view. They have none of the underlying theory which makes Martin-Löf‘s work so powerful. They require the specification to be given in the form: head ⌊ q where head is of the form ⟨name⟩(arguments). q can be any first order predicate logic formula. From this they synthesise a recursive step case predicate in a Horn clause logic. No attempt is made to synthesise the base case. To do the synthesis the system also requires an example of how the predicate will split up its arguments and the form of any recursive calls to be made in the predicate. So to synthesise the basic subset predicate you could give the specification:

subset(xs, ys) ⌊ ∀x.(member(x, xs) ( member(x, ys)).

The required head: subset([a|as], b).

And the required recursive calls subset(as, bs).

Lau and Prestwich describe this as the folding problem and write it as FOLD(Head, Body, Calls) where Body is the program we wish to synthesise, the specification remains in the background. The synthesis takes place in a top down manner using a number of folding strategies. These strategies are either axiomatic or they synthesise FOLD(Head, Body, Calls) by breaking the Body down in to simpler bits, say Body_{1}, ...Body_{n} using a unfold formula and then solving FOLD(Head, Body_{1}, Calls),..., FOLD(Head, Body_{n}, Calls). The solutions of these sub-problems are then recombined using a fold formula. The exact fold and unfold formulae are dependent on what strategies are used as well as the Head and Calls.

There are four rules in all:

• The Definition Strategy. This is the main decomposition strategy. Given the folding problem:

FOLD(pθ_{0}, z, {pθ_{1}, ...pθ_{n}})

where θ_{0} to θ_{n} are variable bindings and suppose p has the definition:

p ⌊ q

then we use:

pθ_{0} ( qθ_{0}

as the unfold formula. We can define a number of sub problems:

FOLD(q_{0}θ_{0}, z, {q_{0}θ_{1}, ...q_{0}θ_{n}}) FOLD(q_{1}θ_{0}, z, {q_{1}θ_{1}, ...q_{1}θ_{n}})
FOLD(q_{o}θ_{0}, z, {q_{o}θ_{1}, ...q_{o}θ_{n}})

where the q_{n}s are the sub parts of q, and use:

qθ_{1} ( pθ_{1}. qθ_{2} ( pθ_{2}.
qθ_{n} ( pθ_{n}.

There are four sub-versions of this strategy: the conjunctive form, the disjunctive form, the existential form and the universal form, which differ in the way they break down q.

• The Implication strategy. This strategy can be used when there is already a known recursive solution to a head. Say we have the problem:

FOLD(pθ_{0}, z, {pθ_{1}, ...pθ_{n}})

and we know that:

pθ_{0}ψ ( q(pϕ_{1}, ...pϕ_{p})

Where ψ are any more bindings that are needed. pϕ_{1}...pϕ_{p} are then solved with calls pθ_{1}, ...pθ_{n}.

• The Match strategy. This is the main axiomatic strategy. It works by matching unifying the Head with each of the Calls. i.e. it solves problems of the form:

FOLD(t, t, {t})

• The Modus Ponens strategy. This strategy simply defines a new predicate that fits the specification. i.e. it solves the problem:

FOLD(pθ_{0}, z, {pθ_{1}, ...pθ_{n}})

by saying that:

z = pθ_{0} ( aux(y_{1}...y_{m}) ∧ pθ_{1} ∧ ... ∧ pθ_{n}.

where y_{1}, ..., y_{m} are the free variables of {pθ_{1}, ...p, θ_{n}}. However this does still leave the problem of synthesising a predicate for:

aux(y_{1}, ..., y_{n}) ⌊ (pθ_{0} ( pθ_{1} ∧ ... ∧ pθ_{n})

In the paper, [LP90] the subset predicate is synthesised. The subset predicate is specified like so:

subset(a, b) ⌊ ∀x.aux(x, b, a)

aux(x, b, a) ⌊ men(x, b) ∨ ¬mem(x, a)

mem(x, a ++b) ⌊ mem(x, a) ∨ mem(x, b)

So this particular folding problem can be written:

G_{1} : FOLD(subset(a ++b, s), z_{1}, {subset(a, s_{1}), subset(b, s_{2})}).

Indicating that the list should be spill down into two smaller lists and than there should then be recursively calls to each of these parts. The first rule to be applied is the definition rule. This uses the unfold formula:

subset(a ++b, s) ( ∀x.aux(x, s, a ++b)

and the fold formulae:

aux(x_{1}, s_{1}, a) ( subset(a, s_{1})
aux(x_{2}, s_{2}, b) ( subset(b, s_{2})

These lead to the new folding problem:

G_{1.1} : FOLD(aux(x, a ++b, s), z_{1.1}, {aux(x_{1}, s_{1}, a), aux(x_{2}, s_{2}, b)}).

We now apply the disjunction form of the Definition rule with the specification of aux. This uses the unfold formula:

aux(x, s, a ++b) ( mem(x, s) ∨ ¬mem(x, a ++b)

and the fold formulae:

mem(x_{1}, s_{1}) ∨ ¬mem(x_{1}, a) ( aux(x_{1}, s_{1}, a)
mem(x_{2}, s_{2}) ∨ ¬mem(x_{2}, b) ( aux(x_{2}, s_{2}, b)

This disjunction then leads to two new fold problems:

G_{1.1.1} : FOLD(mem(x, s), z_{1.1.1}, {mem(x_{1}, s_{1}), mem(x_{2}, s_{2})})
G_{1.1.2} : FOLD(¬mem(x, a ++b), z_{1.1.2}, {¬mem(x_{1}, s_{1})¬mem(x_{2}, s_{2})})

G_{1.1.1} can now be solved by matching it with the Calls. To do this we use the axiomatic MATCH rule. This requires the bindings: [x_{1} := x, x_{2} := x, s_{1} := s, s_{2} := s]. This means that:

z_{1.1.1} = mem(x, s)

We then apply the bindings to G_{1.1.2} to get:

G_{1.1.2} : FOLD(¬mem(x, a ++b), z_{1.1.2}, {¬mem(x, a)¬mem(x, b)})

This can then be solved using the Implication rule and the mem definitions. So we now place z_{1.1.1} and z_{1.1.2} into the unfold formula for G_{1.1} to get:

aux(x, s, a ++b) ( mem(x, s) ∨ ¬mem(x, a) ∧ mem(x, b)

Which when written in CNF form is:

aux(x, s, a ++b) ( (mem(x, s) ∨ ¬mem(x, a)) ∧ (mem(x, s) ∨ ¬mem(x, b)).

How we use the fold formulae for G_{1.1} and the bindings to get z_{1.1}:

aux(x, s, a ++b) ( aux(x, s, a) ∧ aux(x, s, b)

Then we use the unfold formula of G_{1} to give:

subset(a ++b, s) ( ∀x(aux(x, s, a) ∧ aux(x, s, b))

We can rewrite this as:

subset(a ++b, s) ( ∀x.aux(x, s, a) ∧ ∀x.aux(x, s, b))

and use the unfold formula again to give:

subset(a ++b, s) ( ∀x.subset(a, s) ∧ ∀x.subset(b, s)

And final rewrite to get z_{1}, the finished predicate:

subset(a ++b, s) ( subset(a, s) ∧ subset(b, s)

This fold/unfold method does work but it lacks the power and the elegance of Martin-Löf’s Type Theory. It’s more of a clever transformation than ground breaking theory. It is also unclear if this method is complete, (a point which the author’s concede). Having to give the initial decomposition of the predicate’s arguments and the recursive calls the predicate is to make leaves very little for the synthesis to do. I find it hard to imagine that you could come up with these with out knowing exactly how the predicate is to be written in the target language. So this process will be most use full to ensure correctness.

3.4 L. Fribourg Extracting logic programs from proofs that use extended Prolog execution and induction.

Fribourg [Fri90] breaks away from the fold unfold transformation method by regarding Prolog goals in the form:

∀x∃y.q(x, y) ( r(x)

where q and r are conjunctions of Prolog atoms. q is the goal’s conclusion and r is the hypotheses. So Fribourg is considering x as input and y as the output. He then uses proof rules to extract a program. This is done with an extended version of the Prolog interpreter and produces programs, directly, in Prolog.

The goals are processed in a quantifier free form. i.e. given

∀X∃YG− ( G+

every variable y, in Y is replaced by ?y, this is written: G + (?Y) ( G−. Fribourg calls a goal in this form an implicative goal. He also considers the conclusion part G+ to be in first order logic so uses & as the conjunction symbol where as the hypotheses part is considered to already be Prolog code so “,” is used as the conjunction symbol.

Associated with each implicative goal, G there is an io-atom written io_{G}(X, Y). Here io stands for input-output. The io-atom associated with the initial goal will be the finished predicate. Deductions describe how to break a goal G down into simpler parts: H_{i}_{I=1..n} . io-procedures then define IO_{G} in terms of IO_{H1}, ..IO_{Hn}.

Fribourg gives 3 rules in his paper. The first is called Definite Clause Inference (DCI); it is an extension of the normal Prolog SLD resolution. The axiomatic rule is called Simplification and it matches the conclusion to one of the hypotheses. The final rule covers induction. For lists it takes the goal:

G : G^{+}(?Y)[x] ( G^{−}

to

H0 : G^{+}(?Y)[nil] ( G^{−}
H1 : G^{+}(?Y)[t.w] ( G^{+}(?Y)[w]G^{−}

The associated io-procedure is:

IO_{G}(Y)[nil] ( IO_{H0} IO_{G}(Y)[t.w] ( IO_{G}(Y)[w], IO_{H1}

The paper also explains how to truncate the io atoms to get rid of unwanted variables. A statement of correctness is included with no proof. In his paper Fribourg synthesises an extract for the goal G_{∗} : reverse(x, ?w)&append(?w, ?y, z) predicate.

He uses the predicate definitions:

reverse(nil, nil). reverse(t.x, y) ( reverse(x, z), append(z, t.nil, y)

We first apply the induction rule to get the sub-problems:

H0 : reverse(nil, ?w)&append(?w, ?y, z)
H1 : reverse(t.x, ?w)&append(x, w‘) ( reverse(x, w‘), append(w‘, y‘, z)

with the associated io-procedure:

io_{G}(w, nil, y, z) ( io_{H0}(w, y, z).
io_{G}(w, t.x, y, z) ( io_{G∗}(w′, x, y′, z), io_{H1}(t, w, w′, x, y, y′, z).

We can then apply DCI to H0 with the bindings [w ( nil, y ( z] which produces the io-procedure:

io_{H0}(nil, z, z).

We now turn to H1. We first replace reverse(t.x, ?w) with its definition. To get:

I1 : reverse(x, ?w′′)&append(?w′′, t.nil, ?w)&append(?w, ?y, z) (
reverse(x, w‘), append(w‘, y‘, z)

We can simplify this with the binding: {w′′ ( w′} to give:

J1 : append(w′, t.nil, ?w)&append(?w, ?y, z) ( append(w‘, y‘, z)

with the io-procedure:

io_{H1}(t, w, w′, x, y, y′, z) ( io_{J1}(t, w, w′, y, y′, z)

We now rewrite J1 to give:

J1∗ : append(w′, t.nil, ?w)&append(?w, ?y, ?z)&append(w‘, ?y‘, ?z)

and applying induction on w′ we get:

K0 : append(nil, t.nl, ?w)&append(?w, ?y.?z)&append(nil, ?y′, ?Z)
K1 : append(s.w′, t.nl, ?w)&append(?w, ?y.?z)&append(s.w′′, ?y′, ?Z)
( append(w′, t.nl, ?w)&append(?w, ?y.?z)&append(w′, ?y′, ?Z)

with the io-procedures:

io_{J1∗}(t, w, nil, y, y′, z) ( io_{K0}(t, w, y, y′, z)

io_{J1∗}(t, w, s.w′, y, y′, z) ( io_{J1∗}(t, w, w′, y, y′, z), io_{K1}(s, t, w, w′, w′′, y, y′, y′′, z, z′′)

Applying DCI to K0 with [w ( t.nil, z ( t.y, y′ ( t.y] gives the io - procedure for K0 : io_{K0}(t, t.nil, y, t.y, t.y). Where as applying DCI to K1 with [w ( s.v, z ( s.u] yields:

L1 : append(w′, t.nil, ?v)&append(?v, ?y, ?u)&append(w′, ?y′, ?u) (
append(w′, t.nil, w′′), append(w′′, y′′, z′′), append(w′, y′′′, z′′)

This can then be simplified using [v ( w′′, y ( y′′, u ( z′′, y′ ( y′′′] to give the trivial goal:

io_{L1}(t, z′′, w′′, w′, w′′, y′′, y′′′, y′′, y′′′, z′′)

So then the finished program is:

io_{G∗}(w, nil, y, z)  ( io_{H0}(w, y, z).
io_{G∗}(w, t.x, y, z)  ( io_{G∗}(w′, x, y, z),
io_{H1}(t, w, w′, x, y, y′, z).

io_{H0}(nil, z, z).

io_{H1}(t, w, w′, x, y, y′, z)  ( io_{J1}(t, w, w′, y, y′, z).
io_{J1}(t, w, w′, y, y′, z)  ( io_{J1∗}(t, w, w′, y, y′, z).
io_{J1∗}(t, w, w′, y, y′, z)  ( io_{K0}(t, w, y, y′, z).
io_{J1∗}(t, w, s.w′, y, y′, z)  ( io_{J1∗}(t, w′′, w′, y′′, y′′′, z′′),
io_{K1}(s, t, w, w′, w′′, y, y′, y′′, y′′′, z, z′′).

io_{K0}(t, t.nil, y, t.y, , t.y).

io_{K1}(s, t, s.v, w′, w′′, y, y′, y′′, y′′′, s.u, x, z′) ( io_{L1}(t, u, v, w′, w′′, y, y′, y′′, y′′′, z′′).

io_{L1}(t, z′′, w′′, w′, w′′, y′′, y′′′, z′′).

By unfolding this can be simplified to:

io_{G∗}(nil, nil, y, y).

io_{G∗}(w, t.x, y, z)  ( io_{G∗}(w′, x, y′, z), io_{J1}(t, w, w′, y, y′, z).

io_{J1}(t, t.nil, nil, y, t.y, t.y).

io_{J1}(t, s.w, s.w′, y, y′, s.z)  ( io_{J1}(t, w, w′, y, y′, z).

This method of synthesis is much closer to Martin-Löf’s Type Theory: starting off with a logical specification and applying proof rules to prove it and so generating a program.

It requires much less extra knowledge than Lau and Prestwich’s method. But the form the specification takes seriously limits the whole process. Firstly the strict separation of “input” and “output” will produce logic code that can only be, reliably, run in one direction. It will also only synthesise deterministic predicates. But more importantly insisting the conclusion and the hypotheses must be conjunctions of atoms means that only very simple concepts can be specified. Conjunctions of atoms can be run in Prolog directly, so this syntheses is really only useful for code transformation. Indeed the example given in the paper (and above) synthesises an efficient version of reverse from an inefficient version.

3.5 G. Wiggins: Synthesis and Transformation of Logic Programs in the Whelk Proof Development System.

This paper [Wig92] is the basis of my work so I treat it in greater depth than the others reviewed here.

The paper presents a proof development system called Whelk. Whelk logic is base on the logic of [Gen69]. Proof rules are applied to give a constructive proof of a specification from which a program can be extracted.

The paper starts with an introduction of proofs as programs in the functional paradigm, and outlines its limitations when it is applied to logic programming i.e. producing purely functional programs, so no there handling of multiple outputs, failure etc., as explained in section above, Wiggins then introduces the form of specification he will use. It breaks away from the limitations of functional synthesis by regarding logic programs in all-ground mode (or relations) as functions to true or false. i.e.:

⊢ ∀vars.∃B.Spec(vars) ⌊ B

where Spec is any first order formula and B is a boolean. Or more conveniently:

⊢ ∀vars.∃P.Spec(vars) ⌊ P(vars)

where P is decidable.

A constructive proof of this will have to produce a P and show it is decidable hence giving us a program. As it is not desirable to use a fully blown higher order language the quantification over programs can be “hidden” with a special symbol, in this case “∂”. So the specification of a program takes the form:

⊢ ∀vars.∂(Spec(vars))

For example, the logic program expressing the square / square-root relation between two numbers could be specified thus:

⊢ ∀x : nat, ∀y : nat.∂(x^{2} = y)

and the subset relation on numbers could be specified thus:

⊢ ∀x : list(nat), ∀y : list(nat).∂(∀z : nat, z ∈ x ) z ∈ y)

The language is strictly first order. Therefore we can not quantify over types so it is impossible to specify the subset relation for list or any type, although it could quite easily be synthesised, in principle.

This form of specification is very powerful. We can express the program to be synthesised in first order logic (and place a ∂ around it). Wiggins also points out that no procedural content is needed as is the case in the fold / unfold method. As the synthesis process is equivalent to doing a proof it could be automated by a proof planner, such as CLAM. Once we have a proof of correctness of the system we know that any program synthesised by this method is correct with regard to its specification. Wiggins also points out that this can be used the other way around: Given a program technique, say a new sorting algorithm, we can attempt to synthesis it in Whelk; if we can, we then know it is correct and it needs no further justification.

Wiggins then introduces his notation and the concept of a pure logic program. Whelk takes a specification in what is termed the specification logic: L_{s} and extracts a program in a program logic: L_{p}. The specification logic is first order logic with the addition of the ∂ symbol and the condition that there can only be one ∂ in any given formula.

It would be awkward to translate straight into Prolog because of its limited expressive power and non-logical features. So an intermediate, pure, logic language is used. The point of this language is to be computable so that the job of translating it to Prolog or Gödel is trivial, but not so computable that we get bogged down in technical detail.

A program in the pure logic language consists of a head and a body connected with a bi-condition symbol. The head is a predicate with a number of arguments and the body is an arbitrary formula, which may contain existential quantification and any free variables that appear in the head, the symbols true and false may also be used. This means that any well-founded recursion must take place by having a disjunction that splits the base and step cases. For example the Prolog program member:

member(X, [X| ]). member(X, [ |Y]) : −member(X, Y).

Would be:

member(x : nat, y : nat list) ⌊

y = [ ] ∧ false

∨ ∃v_{0} : nat∃v_{1} : nat list.y = [v_{0}|v_{1}]
∧ (x = v_{0} ∨ member(x : nat, v_{0} : list(nat))

Wiggins makes a distinction between two different parts of a proof. He calls any part of the proof that contributes directly to the program the synthesis proof and parts of the proof that simply show correctness are called the verification proof. An advantage of the Whelk system is that the two type of proofs are easily distinguishable: whatever is performed inside a ∂ is synthesis proof and proofs done without a ∂ are verification proofs. This means that, unlike Martin-Löf’s Type Theory, we can leave out the parts of the program that would reprove the program correct every time it is run, and not contribute to the result.

Proof rules are then given for the introduction and elimination of each connective, with or with out a ∂. One of the simplest is:

∧ intro \frac{[[Γ ⊢ ∂ A]]_{P(E)⌊ϕ} [[Γ ⊢ ∂ B]]_{P(E)⌊ψ}}{[[Γ ⊢ ∂ (A ∧ B)]]_{P(E)⌊ϕ∧ψ}}

It simply says that if P(ε) ⌊ ϕ is a program that performs task A and P(ε) ⌊ ψ is a program that performs task B then P(ε) ⌊ ϕ ∧ ψ performs task A ∧ B.

Two of the defining rules of the system are ∂_{true} and ∂_{false} . These rules can be used to finish a program and state that if something is always provable true then P(nil) ⌊ true is a program that decides it. Likewise for false:

∂_{true} intro \frac{[[Γ ⊢ A]]_{P(E)⌊ϕ}}{[[Γ ⊢ ∂ A]]_{P(nil)⌊true}}  ∂_{false} intro \frac{[[Γ ⊢ ¬A]]_{P(E)⌊ϕ}}{[[Γ ⊢ ∂ A]]_{P(nil)⌊false}}

The proof of A (or ¬A) and the program extract ϕ do not become part of the in finished program because they simply verify the resulting program is correct and so do not given any computation information. This switch from synthesis proof to verification proof is marked by the removal of the ∂.

A recursive program is produced by an inductive proof. The paper only gives the induction rule for lists:

induction \begin{matrix}[[Γ, x:list(τ), ∂ ⊢ A⟨[ ]/x⟩]]_{P′(E)⌊ϕ} \\ [[Γ, x:list(τ), ∂, v_{0}:τ, v_{1}:list(τ), [[A⟨v_{1}/x⟩]]_{P′(E′)} ⊢ A⟨[v_{0}|v_{1}]/x⟩]]_{P′(E)⌊ψ} \\ [[Γ, x:list(τ), ∂ ⊢ A]]_{P(E)⌊P′(E)} \end{matrix}

where E′ is the environment at the time of application of the rule, and P′ is defined by

P‘(ε′) ⌊ x =_{list(τ)} [ ] ∧ ϕ ∨ ∃v_{0}:τ.∃v_{1}:τ.x =_{list(τ)} [v_{0}|v_{1}] ∧ ψ

The other rules given in the paper are in appendix B, although the paper does not contain all the rules developed. A proof of correctness is then sketched, but is not with in the scope of this paper. For an example syntheses see [Wig92].

3.5.1 Evaluation of [Wig92]

This is the first system I have looked at that allows the synthesis of non-deterministic logic programs from only their specification. The exact correspondence between the proof and the program it produces also means that the user can decide what sort of program they wish to produce for any given specification.

Wiggins also notes that care must be taken in translating the pure logic language to any real logic language.

Whelk works as it is but the system lacks destructor functions. These are functions that map proofs to proofs, breaking them up into their composite parts. For instance given a proof of A ∧ B , ϕ say, it will sometimes be necessary to obtain a proof of just A. The proof of A ∧ B might be done by induction or by a call to another predicate so we can not match ϕ 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_{∧} (ϕ)}

These functions play a similar role to the D,R,i and j functions in Martin-Löf’s type theory (Outlined in the appendix A).

There are also problems with some of the rules. As the author later pointed out, the ∀ intro rule, under delta is unsound:

∀ intro \frac{[[Γ, x:τ ⊢ ∂ A]]_{P(E)⌊ϕ}}{[[Γ ⊢ ∂ (∀x:τ.A)]]_{P(E)⌊ϕ}}

Consider the program that computes a number bigger than any other:

⊢ ∀n : nat.∂(∀m : nat.m ≤ n))

This rule will allow us to replace this goal with:

n : nat, m : nat ⊢ ∂(m ≤ n))

which will lead to the program biggest(n : nat) ⌊ le(m, n).

Another problem is the way parameters are handled. Consider trying to prove:

⊢ forall(z : nat, true) ∧ forall(y : nat, true).

The first rule to apply is the ∧ introduction rule, given above. This leaves:

⊢ forall(z : nat, true) (1).

and

⊢ forall(y : nat, true) (2).

The intro and axiom rules can then be used to prove (1).

axiom \overline{[[Γ, [[A]]_{ϕ} , ∂ ⊢ A]]_{P(nil)⌊ϕ}}  axiom \overline{Γ, \{\}, ∂ ⊢ A}

This implies that the list of arguments of the predicate being synthesised is [z : nat]. However applying the same rules to prove (2) will imply that the predicate’s arguments are [y : nat] and hence we have a contradiction. I give a way to solve this problem in section 6.

4 Changes to be Made

After reviewing these papers it seems clear that the way forward is to extend the work of Wiggins. This will involve:

• Correcting the problems in the current Whelk system, outlined in section 3.5.1.

• Extending the logic to include destructor functions, as outlined in section 3.5.1.

• Define how each destructor function is to operate.

• Implement the system.

• Use the implementation to produce working examples.

.

5 Notation

Before giving my rules I will outline my notation. The rules will be presented as a sequent calculus. I will keep the ∂ symbol from [Wig92]. i.e.

⊢ ∀vars.∂(Spec(vars))

means that:

⊢ ∀vars.∃P.Spec(vars) ⌊ P(vars)

where P is decidable.

I will produce programs in the pure logic languages outlined in section 3.5. So these programs will take the form

P(ε) ⌊ ϕ

where P is the predicate head and ε is its arguments. ϕ is the programs itself which may take form: θ where P′(ε′) ⌊ ψ. I will use P′, P′′... and ε′ε′′... as alternate head names and arguments, and ψ, θ as alternate programs.

Program extracts are produce by doing a proof so I will write the program produced by a sequent as a subscript of the sequent symbol, ⊢. When it is clear what the head should be it will be dropped for the sake of readability. So

\frac{Γ, A_{α} ⊢_{P(ε)⌊ϕ} B ⊢_{P′(ε′)⌊α} A}{Γ ⊢_{P(ε)⌊ϕ} B} Cut

becomes:

\frac{Γ, A_{α} ⊢_{ϕ} B ⊢_{α} A}{Γ ⊢_{ϕ} B} Cut

5.1 Hypotheses Constructions

When a Greek, lower case letter is associated with a Hypotheses, like the α below.

Γ, A_{α} ⊢_{ϕ} B

it indicates that α is the construction of that proof showing that ⊢_{α} A is true. I will normally use Greek lower case letters from the start of the alphabet for this. So the expression above means that given Γ and A, which can be constructed by α then B is provable with construction ϕ.

6 The Rules

These rules are base on the logic of [Gen69] however this logic does not have any proof terms. The structure of the program produced by any rule must reflect the structure of the proof that was used to create it. This ensures we can manipulate the programs as logical objects. For instance if A ∧ B is proved by giving a proof of A and a proof of B then a program for A ∧ B must contain a subprogram of both A and B. These subprograms are accessed by the destructor functions.

To solve the problems with the parameters outlined in section 3.5.1, I will introduce two new pieces of syntax to the pure logic languages: join and merge. join operates on two lists of parameters produced by proving two disjoint propositions. Therefore the two lists will also be disjoint and can simply be appended. For instance, with the ∧ rules.

6.1 ∧ and ∨ 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

When proving A ∨ B from just A or just B it is necessary to mark the proof as having been derived from A or B so when a destructor function is applied, it is clear which proof is present. In his Type Theory Martin-Löf uses i and j. Here I use isl and isr

\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)

Bound variables will be renamed to avoid unwanted variable capture. join can not be implemented while doing the proof because the parameter lists must remain uninstantiated so it must be view as a constructor.

The elimination rules use the destructor functions: r_{∧} , l_{∧} , r_{∨} , l_{∨} . The exact computation rules for all the destructor functions are given in section 7.2.

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

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

When two separate proofs of the same object are needed, as with the ∨ elim rule, two different proofs may introduce a different number of variables and so produce two different parameter lists. Given a renaming of the variables to avoid any variables capture, identical names that appear in both lists will refer to the same variable. So merge will append its two lists deleting as elements of the second list that appear in the first.

\frac{Γ, A_{r_{∨} (α)} ⊢_{P(ε_{1})⌊ϕ} C Γ, B_{l_{∨} (α)} ⊢_{P(ε_{2})⌊ψ} C}{Γ, (A ∨ B)_{α} ⊢_{P(ε_{1} merge ε_{2})⌊ϕ∧ψ} C} ∨ elim

6.2 ∂_{true} and ∂_{false}

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. For instance, given the specification:

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

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

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

6.3 ¬ Rules

The ¬ rules are unchanged from the standard logic calculus systems. However logic languages such as Prolog or Gödel have assumed “closed world”, that is, they assume that everything that is not specified as true is false. Therefore they have no way of handling negation, constructively, so I do not want it in the pure logic language. For this reason there are no ∂¬ intro and ∂¬elim rules. It is unclear what program extract should be with proof by contradiction. Here I propose that the extract should be left unchanged. So any proof associated with {} will come for what ever axiom is used to proof it.

\frac{Γ ⊢_{ϕ} A}{Γ, ¬A ⊢_{ϕ} \{\}} ¬ elim \frac{Γ, A ⊢_{ϕ} \{\}}{Γ, ⊢_{ϕ} (¬A)} ¬ intro

\frac{Γ ⊢_{ϕ} \{\}}{Γ ⊢_{ϕ} A} thin

6.4 Axiom, Lemma and Cut

The axiom rule is simply the usual:

\overline{Γ, A_{α} ⊢_{α} A} axiom

A hypothesis can be added to the sequent at any time:

\frac{Γ, B_{α} ⊢_{ϕ} A}{Γ ⊢_{ϕ} A} lemma

This does not give us any free information as the added hypothesis must have a program extract associated with it, the α. So this requires that ⊢_{α} B. When this hypothesis is used in the proof the program extract will be used in the program. Similarly if there is no ready proof of the hypothesis we wish to add we can do the proof, there and then, with the cut rule:

\frac{Γ, A_{α} ⊢_{ϕ} B ⊢_{α} A}{Γ ⊢_{ϕ} B} Cut

6.5 ∀ and ∃ Rules

The problem of introducing a ∀ under a ∂ is a problem in the logic itself: there is simply no way you can remove ∀s from under a ∂ and still ensure soundness. This is because it would allow you to synthesise programs that would run a computation on all numbers or all lists i.e. programs that would never terminate. We can not get around it but we can substitute ∀ expressions under a ∂ and hence avoid the need of an introduction, as is done in the examples in section 9.1. So I will not allow introduction or elimination of ∀ or ∃ under ∂. This leaves the normal introduction and elimination rules:

\frac{Γ, x : τ ⊢_{P(ε)⌊ϕ} A}{Γ, ⊢_{P((x:τ) join ε)⌊ϕ} ∀x : τ.A} ∀ intro \frac{Γ, A[t/x]_{subs(α,t,x)} ⊢_{ϕ} B}{Γ, (∀x.A)_{α} ⊢_{ϕ} B} ∀ elim

\frac{Γ, t, x : τ, ⊢_{ϕ} A[t/x]}{Γ ⊢_{(t,ϕ)} (∃x : τ.A)} ∃ intro \frac{Γ, (A[l_{∃}(α)/x])_{r_{∃}(α)} ⊢_{ϕ} B}{Γ, ∃x : τ.A_{α} ⊢_{ϕ} B} ∃ elim

6.6 ) Rules

Implication under a ∂ has a similar problem as ∀. Indeed:

∂(nat(n) => P(n))

is in some sense the same as:

∂(∀n : nat.P(n))

Therefore my system contains no intro rules for implication under ∂ as this too would be unsound. Without a ∂, implication specifies a process that given a program transforms it into another program. So I will introduce lambda notation into my logic.

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

6.7 = Rules

The decision of equality in the specification logic matches 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. So we have the following rules:

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

As we deal with equality under ∂ with a rule it would seem odd to deal with equality with out a ∂ with axioms so I will also use rules to decide these:

\overline{Γ ⊢ 0 = 0} nat = base \frac{Γ ⊢_{ϕ} n = m}{Γ ⊢_{ϕ} succ(n) = succ(m)} nat = step

\overline{Γ ⊢ true = true} = true \overline{Γ ⊢ false = false} bool = false

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

list = step

6.8 Substitution Rules

An underlying theme of these rules is that the structure of the proof should in some way reflex the structure of the proposition. I.e. a proof of A ∧ B should have in its extract, at some point: (a proof of A) ∧ (a proof of B). 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 we have a way of transforming proof using the proof of implication. So we need something like:

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

But there is another problem here. I have no rules for the elimination or introduction of a ∀ under a ∂. So to do proof involving these operators I will have to make substitutions under them.

But I could not make these substitution, using the rules above, until I proved them valid, which would involve performing a proof under a ∂ and a ∀ which would be impossible with out a substitution. So I would not even be able to prove sequent such as:

p ) q, q ) p, ∂(∀x.(p)) ⊢ ∂(∀x.(q))

Therefore unless I want to provide axioms to cover very conceivable situation I need a rules 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 recognising 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 I have not had enough time to implement this. So for the time being I 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 in by any destructor function they use. Although by no means prefect this will let me demonstrate the system without have to implement the progsub function above.

6.9 Induction

There is an induction rule for each of the three types I wish to use:

\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

\begin{matrix}Γ ⊢_{P(ε_{1})⌊ϕ} A[true/b] \\ Γ ⊢_{P(ε_{2})⌊ψ} A[false/b] \\ Γ, b : bool ⊢_{P(ε_{1} merge ε)⌊(b=true∧ϕ)∨(b=false∧ψ)} A) \end{matrix} Bool induction

\begin{matrix}Γ ⊢_{P′(ε_{1})⌊ϕ} A[[ ]/l] \\ Γ, t : list(τ), h : τ, A[t/l]_{P′(ε′ join (ε_{1} merge ε_{2}))[t/l]} ⊢_{P′(ε_{2})⌊ψ} A[[h|t]/l] \\ Γ, l : list(τ) ⊢_{P(ε_{1} merge ε_{2})⌊P′(ε′ join (ε_{1} merge ε_{2}))} \\ _{where P′(ε′ join (ε_{1} merge ε_{2}))⌊(l=[ ]∧ϕ)∨(∃h:τ.∃t:list(τ).l=[h|t]∧ψ)} A \end{matrix} List induction

As the type of Booleans only has two elements, instead of a countable number as with numbers or lists, its induction consists of two bases cases and no induction step.

The conclusion of each sequent is the normal primitive induction base and step cases. Notice also that the induction variable is removed from the environment and replaced by its constituent parts.

These rules handle recursion by adding a new predicate, which also acts as the proof of the induction hypothesis. This new predicate is defined as a disjunction of the base and step cases with the appropriate guard. This introduces a disjunction in the program that is not reflected by the structure of the proof (i.e. a proof of ∂(A ∨ B) will generally have the form (proof of A) ∨ (proof of B) but not if we have proved it by induction. However the structure will be preserved in the programs produced by the proofs of the base and step case. So the destructor functions will have to be applied to the programs for the base and step cases. To make it clear when this is necessary the disjunction has been changed to ∨_{ind} .

The base case and the step case will prove essentially the same object in, possibly, different ways and so they may produce different parameter lists that refer to a different number of the same variables therefore these two lists must be merged to produce the main parameter list. However variables in the environment must also be available to the new predicate so these are joined into the new predicate argument list.

7 The Destructor Functions and Other Syntax

7.1 A Summary

In this section I define now my destructor functions and other non-standard features work. Over the page is a table summarising all the destructor functions and other pieces of Syntax that are specific to my calculus. Pf represents the type of proofs, P is the type of lists of parameters and var it the type of variables.

7.2 The Destructor Functions

These are the function that map proofs to proofs. These are the top 11 functions on the table below. They all operate on the principle that the structure of the proof reflects the structure of the program.

7.2.1 r_{∧} and l_{∧}

These are the simplest Destructor Functions. A proof of A ∧ B will be made up of a proof of A and a proof of B put together with a ∧. So these two functions simply go through the program until they find this and return the correct branch:

\begin{matrix}r_{∧} (ϕ ∧ ψ)  = & ψ \\ 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 likewise for l_{∧}

7.2.2 r_{∨} , l_{∨} , isr and isl

∨ elimination is slightly more tricky because a proof of ∂(A ∨ B) may contain a proof of ∂(A) and a proof of ∂(A) or it may contain a proof of A or it may contain a proof of B. It is for precisely this reason that I have introduced the markers isr and isl to tell me which proofs are present.

Symbol  Name  Type  Associated with Purpose
r_{∧}  rand  Pf ) Pf  ∧ elim  Finding the proof of the

right ranch of a conjunction

l_{∧} land Pf ) Pf ∧ elim Finding the proof of the

left branch of a conjunction

r_{∨} roar Pf ) Pf ∨ elim Finding the proof of the

right ranch of a disjunction

l_{∨} law Pf ) Pf ∨ elim Finding the proof of the

left ranch of a disjunction

λ lambda Pfvar ) Pf ) Pf ) intro Takes a proof and a name

to an implication proof.

, ( ) apply Pf ) Pf ) Pf ) elim Takes proofs of A&A ) B

and returns a proof of B

subs subs Pf ) var ) ∀ elim substitutes two vars or
var ) Pf  adds a var to a name.
( , )  exists  var ) Pr  ∃ intro  Given a v and proof of
proof  ) (var, Pf)  P(v) it gives a proof of ∃x.P(x)
l_{∃}  lex  (var, Pf) ) var  ∃ elim  maps a proof of ∃x.P(x) it

finds the variable v s.t. P(v).

r_{∃} rex (var, Pf) ) Pf ∃ elim Given a proof of ∃x.P(x) it

finds the proof of P(v).

∂_{true}  decide true  Pr ) Pr  ∂_{true} intro  Maps any proof to true
∂_{false}  decide false  Pr ) Pr  ∂_{false} intro  Maps any proof to false
isr  is right  Pr ) Pr  ∨ right intro A marker for the right hand

branch of a proof.

isl is left Pr ) Pr ∨ left intro A marker for the left hand

branch of a proof.

∨_{ind}  induction  Logic operator  Induction  Behaves as a ∨ also
or  Rules  a marker for induction
join  join  P ) P ) P  Many  Puts together two non-

disjoint parameter lists

merge merge P ) P ) P Many Puts together two

disjoint parameter lists

\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.

Notice the effect of applying r_{∨} to isl(ϕ). This happens when we ask for a the proof of a right hand branch of an ∨ which has between proved using its left branch. The resulting program will then signal an error. It would be nice to avoid this situation. To do this we would have to alter our notion of ∨ introduction or ∂∨ elimination. l_{∨} behaves a symmetrically similar way. isl(ϕ) and isr(ϕ) behave as ϕ and can be removed as soon as there are outside the scope of any l_{∨} or r_{∨} .

7.2.3 Lambda: λ and Apply: ( )

Implication maps one proof to another. ) introduction provides λαϕ as a proof of A ) B where α represent a proof of A and ϕ is a proof of B which may use α.

If a proof of A ) B is used in an elimination it will be expected to take a proof of A and return a proof of B. This can be do by substitution at the λ stage:

\begin{matrix}(λα.ϕ)(ψ)  = & ϕ[ψ/α] \\ ((G_{1} ∧ ϕ) ∨_{ind} (G_{2} ∧ ψ))(θ) = & (G_{1} ∧ (ϕ(θ)) ∨_{ind} (G_{2} ∧ ψ(θ))) \\ defn1[X](ϕ)  = & ψ(ϕ) \\ θ((G_{1} ∧ ϕ) ∨_{ind} (G_{2} ∧ ψ)) = & (G_{1} ∧ θ(ϕ)) ∨_{ind} (G_{2} ∧ θ(ψ)) \\ θ(defn2[Y])  = & θ(ϕ) \end{matrix}

where defn1[X] ⌊ ψ

defn2[Y] ⌊ ϕ

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

7.2.4 subs

subs is used for ∀ elimination. That is going from a proof of ∀x : τ.A to a proof of A. So if α is a proof of ∀x : τ.A and t is a term of type τ then subs(α, x, t) is proof of A[t/x]. However we must also consider the case when α is a predicate call and x is being introduced to the environment. Here t must be inserted into the parameter call in the place of x.

\begin{matrix}subs(defn[X], x, t)= & defn[X][t/x] & if x ∈ X \\ subs(defn[X], x, t)= & defn([t]joinX) & if ¬x ∈ X \\ subs(ϕ, x, t) = & ϕ[x/t] & if ¬(ϕ = defn[X]) \end{matrix}

7.2.5 Lex: l_{∃}, Rex: r_{∃}, and exists proof: ( , )

( , ) is used to make a proof of ∃x : τ.A. The first element of the pair is a witness and the second element is a proof of that witness:

(an object: t of type τ , a proof of A[t/x])

(t, ϕ) will behave as ϕ. The l_{∃} and r_{∃} functions will break up this pair into its first and second element:

r_{∃}(t, ψ)  =  ψ
r_{∃}((G_{1} ∧ ϕ) ∨_{ind} (G_{2} ∧ ψ)) = (G_{1} ∧ r_{∃}(ϕ)) ∨_{ind} (G_{2} ∧ r_{∃}(ψ))
r_{∃}(defn[X]) = r_{∃}(ϕ) =
where defn[X] ⌊ ϕ

l_{∃} is defined in a symmetrically similar way.

7.2.6 Decides true and false: ∂_{true} , ∂_{false}

∂_{true} maps its argument to the program true excepted in the case where the program relies on an equality or binding of two variables in which case the equality mush become part of the program.

\begin{matrix}∂_{true} (ψ ∧ ϕ)  = & ∂_{true} (ψ) ∧ ∂_{true} (ϕ) \\ ∂_{true} (ψ ∨ ϕ)  = & ∂_{true} (ψ) ∨ ∂_{true} (ϕ) \\ ∂_{true} (x = y in τ)  = & x = y \\ ∂_{true} (G_{1} ∧ ϕ) ∨_{ind} (G_{2} ∧ ψ) = & (G_{1} ∧ ∂_{true} (ϕ)) ∨_{ind} (G_{2} ∧ ∂_{true} (ψ)) \\ ∂_{true} (defn[X])  = & ∂_{true} (ϕ) \\ ∂_{true} (θ)  = & true \end{matrix}

where defn[X] ⌊ ϕ

and θ is any formula not defined here.

∂_{false} behaves in the same way except it maps formulae to false rather than true.

7.3 Other Syntax

7.3.1 induction or: ∨_{ind}

This is the ∨ which is used in an induction between the base case and the step case. I behaves just like an normal ∨. It is distinguished form ∨ so that the destructor functions know when they are being applied to a induction.

7.3.2 Join and Merge

As I have said in section 6 These are for putting together lists of parameters. join puts together two list of disjoint variables. So it simply has appends them:

\begin{matrix}join([ ], YS) = & YS \\ join([X|XS], YS)= & [X|join(XS, YS)] \end{matrix}

merge puts together two lists of parameters of the same object. Therefore any repetitions in the lists refer to the same variable and should be removed:

merge(XS, [ ]) =  XS  ,
merge(XS, [Y|YS])= merge(XS, YS) , if Y ∈ XS
merge(XS, [Y|YS])=merge(XS, YS) ++Y, if ¬(Y ∈ XS)

To avoid variable capture it may be necessary to rename some of the local variables.

8 Implementation

8.1 The Implementation Method

Now we have the full logic we can use it to synthesise programs. This is important to gain a better understanding of how the logic works and see if any developments are needed, as well as demonstrating that the system works. However the logic is so complicated that only the very simplest examples can be done by hand, so I have chosen to implement the logic in a system called Mollusc, which is out lined, in [RKSW94] and in the Mollusc Manual [RS95].

Mollusc allows a user to define and use any sequent calculus. It runs as a Prolog session and proofs are created, in the refinement style, by applying rules to a sequent to produce subsequents; these then form a tree. The user can then navigate the tree and examine the rule applied at any node. The proof is finished when all nodes lead to other nodes or a call to a lemma or axiom. Mollusc is currently implemented in the Sicstus dialect of Prolog. To define a calculus I must provide 6 modules or files:

inference rules.pl This file defines how each of the rules works. It exports two predicates: is rule/1 and rule/3. The first of these is simply true for any rule name. The second defines an inference rule. It takes the form:

rule(rule name(arguments), sequent in, [sequent(s) out])

For an axiom the sequent out list is simply left empty. The rule:

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

would be implemented

rule(intro, Sequent in, [Sequent out1, Sequent out2]) : −

Prolog code which ensures Sequent in is of the form:

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

Prolog code which ensures Sequent out1 is of the form: Γ ⊢_{P(ε_{1})⌊ϕ} A,

Prolog code which ensures Sequent out2 is of the form: Γ ⊢_{P(ε_{2})⌊ψ} B.

These pieces of code can be written with the help of access and parsing predicates which are generated automatically from the files below.

printer.pl This file defines how Mollusc will display the sequents, and other expressions used in the calculus. In particular it must define the predicates: print proof state, that prints a sequent to a given output stream and print definition, that defines how to display a definition.

utility.pl This files simply gathers together any standard predicates that are needed in other files.

logic.pl, parser.pl, access.pl logic.pl names the logic and all the types of definition in the logic with the predicates logic name and kinds of definitions. The file parser.pl defines the operators in the calculus and how to parse them. access.pl defines functions that assemble and disassemble expressions such as hypothesis that gets the hypothesis from a sequent or leftexp that accesses the left expression of a binary operator.

I have listed these three files together because they can all be generated by a program called define logic which is part of the standard Mollusc distribution. In order to use this utility you must write a file called specification.pl. This file must define the grammar of the logic with additional annotations to label the parts that are to be accessible using predicates. These annotation use the keywords af, aaf and faf. For example given the piece of grammar:

conjection = term ∧ term

it could be annotated thus:

conjunction = term af left exp ∧ term af right exp
aaf args faf conjunction

and the define logic program would then produce the code:

left exp(A ∧ B, A).
right exp(A ∧ B, B).
args(Term, Args) :- term = ..[∧|Args].
conjunction(( ∧ ), ∧).

For more information on these files, see the Mollusc manual [RS95].

8.2 Work Carried Out

Wiggins’ work on this subject was also implemented in Mollusc so I have been able to make use of this. However this did leave a lot of design and to be done.

The files printer.pl and untility.pl have been used with only very minor changes. I have added the definitions of all the new destructor functions to the specification.pl file as well as the information necessary to parse them I have also had to make other minor alteration to account for fixes for the problems I outlined in section 3.5.1 My different treatment of parameters, as well as the large number of differences in my calculus, meant that I could not use any of the old whelk rules directly. I have given the code for two of my rules in appendix C, which give the general flavour of the implementation. Wiggins’ work was also implemented in the Quintus dialect of Prolog as a posed to the Sicstus dialect which I am using. This has lead to some minor bugs that were trivial but time consuming to correct.

Once the system was up and running I was able to synthesise programs that would be very messy if done by hand, such as the subset example in the next section. Having a computer calculate the new sequents and program extracts also enforces a rigour which which is not possible using pen and paper. This is when I first found the inconsistency in the use of the parameters and the substitution rule. It also lead me to consider destructor function being applied to predicate names and inductions.

9 Examples

For my main example I will synthesise the subset predicate from the specification:

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

This is complex enough to demonstrate the system but not so complex that the proof will become hard to follow. I will first present the proof and then work back to the specification building up the program as I go. For the sake of clarity I will not write in hypotheses which are of no relevance to the proof. In the proof I will use the following lemma about the decidable of the natural numbers:

∀(x : nat, ∀(y : nat, x = y in nat ∨ ¬(x = y in nat)))

This lemma will have the extract:

P(x : nat, y : nat) ⌊ ((x = y in nat) ∨ (¬(x = y in nat)))

and the lemmas:

∀x : nat.∀.y : nat.∀z : nat list.(x ∈ [y|z]) ⌊ (x = y in nat ∨ x ∈ z)
∀x : nat.¬x ∈ [ ]
x ∈ [k1|k0] ⌊ x = k1 in nat ∨ x ∈ k0
∀x.x = x

9.1 The Proof

The proof is started by applying ∀ induction to get the new goal:

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

I now use the induction rules to give me a base case:

⊢ ∀(l : nat list.∂(∀(x : nat, x ∈ [ ] ) x ∈ l))
(2a)

and a step case:

k1 : nat, k0 : nat list,
∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))
⊢ ∀(l : nat list.∂(∀(x : nat, x ∈ [k1|k0] ) x ∈ l))
(2b)

I will take the similar base case first. The base case antecedent is x ∈ [ ] which is false. And as false implies anything I can use this to do the proof. So we start using ∀ introduce to move the list l into the environment. This yields:

l : nat list ⊢ ∂(∀(x : nat, x ∈ [ ] ) x ∈ l))
(3a)

I can always prove x ∈ [ ] ) x ∈ l as true so we use ∂_{true} introduction to get rid of the ∂:

l : nat list ⊢ ∀(x : nat, x ∈ [ ] ) x ∈ l)

(4a)

Another ∀ introduction moves the x : nat into the environment and introducing the implication then gives:

l : nat list, x : nat, x ∈ [ ] ⊢ x ∈ l
(5a)

We now have a contradiction in the environment so we are effectively done. But we still have to show x ∈ [ ] is a contradiction. To do this we add the lemma: ∀z : nat.¬z ∈ [ ] and use ∀ elimination to put x in for z. This leaves us with:

l : nat list, x : nat, x ∈ [ ], ¬(x ∈ [ ]) ⊢ x ∈ l
(6a)

So applying the thin rule then ¬ elimination and axiom finish this part of the proof. So back to the step case (2b):

k1 : nat, k0 : nat list,
∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))
⊢ ∀(l : nat list.∂(∀(x : nat, x ∈ [k1|k0] ) x ∈ l))
(2b)

We can now rewrite this using the substitution:

∀x : nat.(x ∈ [k1|k0] ) x ∈ l)

⌊

((∀x : nat.x = k1 in nat ) x ∈ l)
∧(∀x : nat.x ∈ k0 ) x ∈ l))

This substitution is proven by using the lemma:

x ∈ [k1|k0] ⌊ x = k1 in nat ∨ x ∈ k0

and standard logical equivalences. This leaves the goal:

k1 : nat, k0 : nat list,
∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))
⊢ ∀l : nat list.∂((∀x : nat.x = k1 in nat ) x ∈ l)
∧ (∀x : nat.x ∈ k0 ) x ∈ l))
(3b)

To prove this we start by introducing the ∀ and the ∧ to get the two goals:

k1 : nat, k0 : nat list, l : nat list,
∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))
⊢ ∂(∀x : nat.x = k1 in nat ) x ∈ l)
(4ba)

and:

k1 : nat, k0 : nat list, l : nat list,
∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))
⊢ ∂(∀x : nat.x ∈ k0 ) x ∈ l)
(4bb)

Lets us start with (4bb) as that is the easier of the two branches. In fact we can prove this by using that induction hypotheses:

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

by first using ∀ elimination with the variable l to get the hypotheses ∂(∀(x : nat, x ∈ k0 ) x ∈ l)) and then applying the axiom rule.

That leaves us with (4ba). To prove this we must look at contains of the list l. This is done by applying the induction rule:

k1 : nat, k0 : nat list ∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))
⊢ ∂(∀x : nat.x = k1 in nat ) x ∈ [ ])
(5baa)

And

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list ∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))

∂(∀x : nat.x = k1 in nat ) x ∈ l0)

⊢ ∂(∀x : nat.x = k1 in nat ) x ∈ [l1|l0])

(5bab)

The conclusion in the base case, x ∈ [ ] is false so we can prove the base case by applying the ∂_{false} rule and then ¬ introduction to get

k1 : nat, k0 : nat list ∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))
∀x : nat.x = k1 in nat ) x ∈ [ ]
⊢ {}
(6baa)

To make the conclusion true the antecedent: x = k1 must also be true. So we can use ∀ elimination with the variable k1. Then ) elimination and the lemma ∀x.x = x will give us the false conclusion as a hypotheses:

k1 : nat, k0 : nat list ∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))
∀x : nat.x = k1 in nat ) x ∈ [ ]
k1 = k1 in nat ) k1 ∈ [ ]
k1 ∈ [ ]
⊢ {}
(7baa)

We can now call the lemma ∀x.¬x ∈ [ ] to establish the contradiction. So now back to the induction step (5bab):

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list ∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))

∂(∀x : nat.x = k1 in nat ) x ∈ l0)

⊢ ∂(∀x : nat.x = k1 in nat ) x ∈ [l1|l0])

(5bab)

We start off here by applying the substitution:

x = k1 in nat ) x ∈ [l1|l0]
⌊
(x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0)

This is proved using the lemma:

∀x : nat.∀.y : nat.∀z : nat list.(x ∈ [y|z]) ⌊ (x = y in nat ∨ x ∈ z)

We also which to use the decidability of natural numbers lemma. So that is added to the hypothesis list:

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list ∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))

∂(∀x : nat.x = k1 in nat ) x ∈ l0)

∀(x : nat, ∀(y : nat, x = y in nat ∨ ¬(x = y in nat)))

⊢ ∂(∀x : nat.(x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0))

(6bab)

We wish to use this lemma with k1 and l1 so we use ∀ elimination to put those variables in. So dropping unnecessary hypothesis we get:

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list ∀(l : nat list.∂(∀(x : nat, x ∈ k0 ) x ∈ l))

∂(∀x : nat.x = k1 in nat ) x ∈ l0)

...
k1 = l1 in nat ∨ ¬(k1 = l1 in nat))) (x)

⊢ ∂(∀x : nat.(x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0))

(7bab)

So now we wish to consider the two cases: k1 = l1 and ¬k1 = l1. For use ∨ elimination on (x). To give the two sub sequents: k1 : nat, k0 : nat list, l1 : nat, l0 : nat list

...

k1 = l1 in nat

⊢ ∂(∀x : nat.(x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0))

(8baba)

and

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list

...

¬k1 = l1 in nat

⊢ ∂(∀x : nat.(x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0))

(8babb)

(8baba) can always be decided true because given k1 = l1 we know that x = k1 ) x = l1). So we apply ∂_{true} and ∀ introduction to get:

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list

...

k1 = l1 in nat
x : nat

⊢ (x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0))

(9baba)

It is the left branch we wish to prove so ∨ left introduction gives us:

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list

...

k1 = l1 in nat
x : nat
⊢ (x = k1 in nat ) x = l1 in nat)
(10baba)

) introduction produces the sequent:

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list
...
k1 = l1 in nat
x : nat
x = k1 in nat ⊢ x = l1 in nat

(11baba)

which is proved by substituting k1 for x and applying to the equality lemma. Back to (8babb):

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list
...
¬k1 = l1 in nat

⊢ ∂(∀x : nat.(x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0))

(8babb)

We now apply the substitution:

(x = k1 in nat ) x = l1 in nat)
∨(x = k1 in nat ) x ∈ l0))
⌊
x = k1 in nat ) x ∈ l0)

This substitution is still more complex that the others so I will go though its justification. Which involves proving the two sequents:

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list
...
¬k1 = l1 in nat, x : nat

⊢ (x = k1 in nat ) x ∈ l0) ) ((x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0))

(9babbb)

and k1 : nat, k0 : nat list, l1 : nat, l0 : nat list

...

¬k1 = l1 in nat, x : nat

⊢ ((x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0)) ) (x = k1 in nat ) x ∈ l0)

(9babbc)

So taking (9babbb) first, we apply ) introduction and then ∨ right introduction to get:

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list

...

¬k1 = l1 in nat, x : nat
(x = k1 in nat ) x ∈ l0) (xx)
⊢ (x = k1 in nat ) x ∈ l0)
(10babbb)

Then apply axiom with (xx). Taking the other implication (9babbc) and apply ) introduction twice we get:

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list

...

¬k1 = l1 in nat, x : nat

((x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0)) (y) x = k1 in nat vdashx ∈ l0

(10babbc)

∨ elimination on (y) gives us the two sequents:

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list

...

¬k1 = l1 in nat, x : nat (y)

((x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0)) x = k1 in nat (yy)

x = k1 in|nat ) x = l1 in nat

⊢ x = l1

(11babbca)

and

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list
...
¬k1 = l1 in nat, x : nat (w)

((x = k1 in nat ) x = l1 in nat) ∨ (x = k1 in nat ) x ∈ l0)) x = k1 in nat (zz)

x = k1 in nat ) x ∈ l0) (z)

⊢ x ∈ l0

(11babbcb)

The first can be proved by contradiction with the aid of hypothesis (y) and (yy). Where as the second can be proved by ) elimination of (z) with (zz). This proves the substitution valid. So now we can go back to (8babb) and make the substitution:

k1 : nat, k0 : nat list, l1 : nat, l0 : nat list
...
∂(∀x : nat.x = k1 in nat ) x ∈ l0) (w)
¬k1 = l1 in nat
⊢ ∂(∀x : nat.x = k1 in nat ) x ∈ l0)

(9babba)

This is now proved by a simple axiom call to (w) which is the induction hypothesis from the second induction call.

This completes the proof.

9.2 The Program

I will now work back though the proof to show how the program is made. Please refer the the proof diagram opposite while reading this section. When axioms are called I will label then with a name and then replace this with code when the program fragment associated with the is defined in the proof. First the base case of k = [ ], (6a) to (2a).

Let us call the axiom called here: axiom1. ¬ elimination and thin leave to unchanged therefore at (6a) we have the program:

P′(nil) ⌊ axiom1
(6a)

This program is unaffected until the ) introduction rule is applied, turning the program into a λ expression. This rule also defines axiom1.

P′(nil) ⌊ λ(var, var)
(4a)

There var is a proof of false i.e. it is non-existent therefore this is a valid proof of:

l : nat list ⊢ ∀(x : nat, x ∈ [ ] ) x ∈ l)

(4a)

Indeed this is a valid proof of any implication with a false antecedent. The ∂_{ture} introduction rule places a ∂_{true} on to the program. Then another ∀ introduction joins on the l:

P′([l : nat list]join[ ]) ⌊ ∂_{true} (λ(var, var))
(2a)

How jumping to the bottom let us look at (11baba) to (8baba). I will call the proof extract associated with this axiom used to prove (11baba), axiom2 until we can see how is is build up. The ) introduction to 10baba turns this into a λ expression:

P′′([ ]) ⌊ λvar2.axiom2
(10baba)

The ∨ left adds a isl to the program. The ∀ introduction removes the universal quantification then the ∂_{true} introduction adds a ∂_{ture} to the program to give the program:

P′′([ ]) ⌊ ∂_{true} (isl(λvar2.axiom2))

(8baba)

The program for (8babb) is also need to construct (7bab) so let us now look at this. The form of substitution used in this proof does not effect the program extract therefore the program for (8babb) is the same as that of (9babba). This is proved by calling an axiom. I will can this program axiom3 until we can see how it is constructed.

(7bab) is constructed from (8baba) and (8babb) by ∨ elim this works in two ways. First it puts the programs for (8baba) and (8babb) together with a ∨ and merges there argument lists. Secondly it breaks up a program of a ∨, in the hypotheses list, into its two parts and applies ror and lor to the hypotheses’ program to form the new programs for these parts. One of these hypotheses happens to be the one associated with axiom2 so let us define axiom2 as lor(axiom2′). Therefore we have:

P′′(([ ]merge[ ]) ⌊
∂_{true} (isl(λvar2.lor axiom2′)) ∨axiom3
(7bab)

The two ∀ elimination substitute the variables l1 and k1 into axiom2′:

P′′([ ]merge[ ]) ⌊
∂_{true} (isl(λvar2.lor subs(subs(axiom2′′, x, k1), y, l1))) ∨axiom3
(6bab)

and the lemma call now defines axiom2′′:

P′′([ ]merge[ ]) ⌊

∂_{true} (isl(λvar2.lor subs(subs(x = y in nat ∨ ¬x = y in nat, x, k1), y, l1))) ∨axiom3

(5bab)

This is the step case of the induction on l who’s base case is defined by (5baa) to (7baa). This branch is formed by ∂_{false} introduction and then ¬ introduction. The second introduction adds:

∀x : nat.x = k1 in nat ) x ∈ [ ]

into the hypotheses list with program true. A ∀ elimination changes this to

k1 = k1 in nat ) x ∈ [ ] (v)

with program subs(true, x, k1). This hypothesis is then split up to give a program for x ∈ [ ] by applying a proof of k1 = k1 in nat to the proof of (v) above. Therefore (5baa) has program extract:

P′[ ] ⌊ ∂_{false} (apply(subs(true, x, k1), true))
(5baa)

So we can now put these together used the induction rules to make 4(ba). This induction also adds the induction hypotheses to our lists of hypotheses’, this has the program: subs(P′′[k0 : natlist, k1 : nat, l : nat list]), l, l0) This is the hypotheses we call to give us axiom3. Therefore we can replace axiom3 with subs(P′′[k0 : natlist, k1 : nat, l : nat list]), l, l0).

P′([ ]merge([ ]merge[ ])) ⌊ P′′([k0 : natlist, k1 : nat, l : nat list]join([ ]merge([ ]merge[ ])))

where

P′′([k0 : nat list, k1 : nat, l : nat list]join([ ]merge([ ]merge[ ])) ⌊

(l = [ ]in nat list ∧ ∂_{false} (apply(subs(true, x, k1), true)))
∨ (∃l0 : nat list.∃l1 : nat.l = [l1|l0]in nat ∧ ∂_{true} (isl(λvar2.lor subs(subs(x =
y in nat ∨ ¬x = y in nat, x, k1), y, l1)))
∨subs(P′′[k0 : natlist, k1 : nat, l : nat list]), l, l0))
(4ba)

(3b) is then constructed with ∧ elimination and the program for (4bb). This program is produces by a ∀ elim with the variable l for a variable name, also l and then a call the axiom rule. So introduction axiom4 we get:

P′() ⌊ subs(axiom4, l, l)
(4bb)

and then:

P′(([ ]merge([ ]merge[ ])merge[ ]) ⌊ P′′([k0 : natlist, k1 : nat, l :
nat list]join([ ]merge([ ]merge[ ])))) ∧ subs(axiom4, l, l)
(3b)

As the step from (3b) to (2b) was performed using a substitution (2b) has the same program. The induction rule is then applied with k on (2b) and (2a). The induction hypothesis produced here is also axiom5

P(([l : nat list]join[ ])merge([ ]merge([ ]merge[ ])merge[ ])) ⌊ P′([k : nat list]join(([l :

nat list]join[ ])merge([ ]merge([ ]merge[ ])merge[ ])))

where

P′([k : nat list]join(([l : nat list]join[ ])merge([ ]merge([ ]merge[ ])merge[ ]))) ⌊

(k = [ ]in nat list ∧ ∂_{true} (λ(var, var))) ∨(∃k0 : nat list.∃k1 : nat.k = [k1|k0]in nat ∧ P′′([k0 : nat list, k1 : nat, l :

nat list]join([ ]merge([ ]merge[ ]))) ∧ subs(subs(P′([k : nat list]), k : nat list, k0 :

nat list), l, l))

where ..
(1)

The last ∀ introduction then produces the finished program:

P([k : nat list]join(([l : nat list]join[ ])merge([ ]merge([ ]merge[ ])merge[ ]))) ⌊ P′([k : nat list]join(([l : nat list]join[ ])merge([ ]merge([ ]merge[ ])merge[ ])))

where

P′([k : nat list]join(([l : nat list]join[ ])merge([ ]merge([ ]merge[ ])merge[ ]))) ⌊

(k = [ ]in nat list ∧ ∂_{true} (λ(var, var)))

∨(∃k0 : nat list.∃k1 : nat.k = [k1|k0]in nat ∧ P′′([k0 : nat list, k1 : nat, l : nat list]join([ ]merge([ ]merge[ ]))) ∧ subs(subs(P′([k : nat list]), k : nat list, k0 :

nat list), l, l))

where

P′′([k0 : nat list, k1 : nat, l : nat list]join([ ]merge([ ]merge[ ])) ⌊

(l = [ ]in nat list ∧ ∂_{false} (apply(subs(true, x, k1), true))) ∨ (∃l0 : nat list.∃l1 : nat.l = [l1|l0]in nat ∧ ∂_{true} (isl(λvar2.lor subs(subs(x =

y in nat ∨ ¬x = y in nat, x, k1), y, l1))) ∨subs(P′′[k0 : natlist, k1 : nat, l : nat list]), l, l0))

Or removing the joins, merges, ∂_{true} and the ∂_{false} subs:

P([k : nat list, l : nat list]) ⌊ P′([k : nat list, l : nat list])

where

P′([k : nat list, l : nat list]) ⌊ (k = [ ]in nat list ∧ true)

∨(∃k0 : nat list.∃k1 : nat.k = [k1|k0]in nat

∧P′′([k0 : nat list, k1 : nat, l : nat list]) ∧ P′([k0 : nat list, l : nat list]))

where

P′′([k0 : nat list, k1 : nat, l : nat list]) ⌊ (l = [ ]in nat list ∧ false)

∨(∃l0 : nat list.∃l1 : nat.l = [l1|l0]in nat ∧∂_{true} (isl(λvar2.lor (k1 = l1 in nat ∨ ¬k1 = l1 in nat)))

∨P′′[k0 : natlist, k1 : nat, l0 : nat list])

In prolog this would be come:

P(X, Y)  :- P′(X, Y).

P′([ ], Y).

P′([X|XS], Y)  :- P′′(X, XS, Y), P′(XS, YS)
P′′(X, XS, [Y|YS]) :- X = Y.
P′′(X, XS, [Y|YS]) :- P′′(X, XS, YS).

P′ is the standard Prolog definition of subset and with out the XS, P′′ would be the standard member predicate. The XS could easily be removed from such predicates with a simple check to see if it is used.

10 Conclusion and Further Work

10.1 Conclusion

The aim of this project was to develop a new calculus to synthesise non-deterministic, relational logic programs. This I have done. I have demonstrated that destructor functions are not only viable but useful, although they do produce new problems such as that of substitution, mentioned in section 6 or ∨ introduction outlined in section 7.2.2 and below.

I have demonstrated the system with examples carried out in a working implementation, examples that could not be done in any other system. However there is still much work to be done.

10.2 Further Work

Further work would include:

• Make substitution safe my implementing the proof substitution function outlined in section 6.

• Matching the structure of ∨ proofs and ∂ ∨ proofs.

\frac{Γ ⊢_{ϕ} A}{Γ ⊢_{is left(ϕ)} A ∨ B} ∨ −intro(left)

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

The difference lies in the fact that both branches have to be proven if the ∨ is under a ∂ where as if it is not only one branches the means that you can not always get a proof of both A and B from a proof of A ∨ B. For instance:

∂(true ∨ otherprog)

can be proved by ∂_{true} introduction then left ∨ introduction. Hence giving no information about otherprog.

A solution to this would be to 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}

This has not been pursued due to lack of time.

• Adding the higher order transfinite induction rules. The Transfinite Induction Principle states that:

∀y.(∀x.((x < y) ) P(x)) ) P(y) ) ∀z.P(z)

The current induction rules are special cases of this. Implementing this rule would make algorithms that use divide and conquer strategies, such as quick sort, much easier to synthesise.

• Automating the destructor functions and translation to Prolog or Gödel. No extra theory is needed here indeed this has been done in [Wig92]. The computation of the destructor functions are described in section(7.2) and the pure logic language is already computable. But it would be nice to get programs which could be runs straight away.

• Automating the proof planning with a program such as CLAM. The proofs required to synthesise a program in my system take the same form as the proofs required to prove theorems in CLAM system. Therefore CLAM could easily be altered to produce programs automatically, from there specifications. If this and the automation of the translation to Prolog where implemented we would be able to enter a specification, press a button and get the desired program back.

• Investigation of how to synthesise efficient proofs. At the moment proof planners are set up to produce simple and clear proofs (this often means short). It would be interesting to see how the heuristics could be altered to produce efficient programs instead.

A Martin-Löf Type Theory Rules and Language

A.1 General Rules

\begin{matrix}\frac{a ∈ A}{a = a ∈ A} Reflexivity & \frac{A type}{A = A} Reflexivity \\ \frac{a = b ∈ A}{b = a ∈ A} Symmetry & \frac{A = B}{B = A} Symmetry \end{matrix}

\frac{a = b ∈ A b = c ∈ A}{a = c ∈ A} Transitivity

\frac{A = B B = C}{A = C} Transitivity

\frac{a ∈ A A = B}{a ∈ B} Equality of types

\frac{a = b ∈ A A = B}{a = b ∈ B} Equality of types

\frac{a ∈ A B type (x ∈ A)}{B(ax)type} Substitution

\frac{a = c ∈ A B = D (x ∈ A)}{B(ax) = D(typecx)} Substitution

\frac{a ∈ A b ∈ B (x ∈ A)}{b(ax) ∈ B(ax)} Substitution

\frac{a = c ∈ A b = d ∈ B (x ∈ A)}{b(ax) = d(cx) ∈ B(ax)} Substitution

\overline{x ∈ A} Assumption

A.2 Cartesian Product of a Family of Types

\frac{A type Btype (x ∈ B)}{(Πx ∈ A)B type} Πformation

\frac{A = C B = B (x ∈ A)}{(Πx ∈ A)B = (Πx ∈ C)D} Πformation

\frac{b ∈ B (x ∈ A)}{(λx)b ∈ (Πx ∈ A)B} Πintroduction

\frac{b = d ∈ B (x ∈ A)}{(λx)b = (λx)d ∈ (Πx ∈ A)B} Πintroduction

\frac{c ∈ (Πx ∈ A)B a ∈ A}{c(a) ∈ B(ax)} Πelimination

\frac{c = f ∈ (Πx ∈ A)B a = d ∈ A}{c(a) = f(d) ∈ B(ax)} Πelimination

\frac{a ∈ A b ∈ B (x ∈ A)}{((λx)b)(a) = b(a/x) ∈ B(ax) ∈ B(ax)} Π − equality

\frac{c ∈ (Πx ∈ A)B}{(λx)(c(x)) = c ∈ (Πx ∈ A)B} Π − equality

A.3 Disjoint Union of a Family of Types

\frac{A type B type}{A + Btype} + −formation

\frac{A = C B = D}{A + B = C + D} + −formation

\frac{a ∈ A}{i(a) ∈ A + B} + −introduction

\frac{a = c ∈ A}{i(a) = i(c) ∈ A + B} + −introduction

\frac{b ∈ B}{j(b) ∈ A + B} + −introduction

\frac{b = d ∈ B}{j(b) = j(d) ∈ A + B} + −introduction

\frac{c ∈ A + B d ∈ C(i(x)z) e ∈ C(j(y)z)}{(Dx, y)(i(a), d, e) ∈ C(cz)} + −elimination

\frac{c = f ∈ A + B d = g ∈ C(i(x)z) e = h ∈ C(j(y)z)}{(Dx, y)(c, d, e) = (Dx, y)(f, g, h) ∈ C(cz)} + −elimination

\frac{a ∈ A d ∈ C(i(x)/z) e ∈ C(j(y)z)}{(Dx, y)(I(a), d, e) = d(ax) ∈ C(i(a)z)} + −equality

\frac{b ∈ B d ∈ C(i(x)z) e ∈ C(j(y)z)}{(Dx, y)(j(b), d, e) = e(by) ∈ C(j(b)z)} + −equality

Other rules deal with: the identity relation, finite types, natural numbers, well orderings. There are also rules dealing with “Universes”, these allow Martin-Löf to avoid Russel’s paradox which states that you can not have a set that contains all sets or equivalently you can not have a type that contains all types.

A.4 The Language

To execute c(a), first execute c. If you get (λx)b then execute b(a/x).

To execute (Ex, y)(c, d), execute c. If you get (a, b) then execute d(a, b/x, y).

To execute (Dx, y)(c, d, e), first execute c. If you get i(a) then execute d(a/x). But if you get j(b) for c then execute e(b/y).

To execute J(c, d), first execute c. If you get r then execute d.

To execute R_{n}(c, c_{0}, ...c_{n−1}), first execute c. If you get m_{n} for some m = 0...n − 1 then execute c_{m}.

B The Rules of [Wig92]

B.1 Axiom

axiom \overline{[[Γ, [[A]]_{ϕ} , Δ ⊢ A]]_{P(nil)⌊ϕ}}  axiom \overline{Γ, \{\}, Δ ⊢ A}

B.2 ∃ Introduction

∃ intro \frac{Γ ⊢ A⟨t/x⟩}{Γ ⊢ ∃x:τ.A}

B.3 ∀ Introduction

∀ intro \frac{[[Γ, x:τ ⊢ ∂ A]]_{P(E)⌊ϕ}}{[[Γ ⊢ ∀x:τ.∂ A]]_{P((x:τ).E)⌊ϕ}}  ∀ intro \frac{[[Γ, x:τ ⊢ ∂ A]]_{P(E)⌊ϕ}}{[[Γ ⊢ ∂ (∀x:τ.A)]]_{P(E)⌊ϕ}}

B.4 ∧ Introduction

∧ intro \frac{[[Γ ⊢ ∂ A]]_{P(E)⌊ϕ} [[Γ ⊢ ∂ B]]_{P(E)⌊ψ}}{[[Γ ⊢ ∂ (A ∧ B)]]_{P(E)⌊ϕ∧ψ}}

B.5 ∨ Introduction

∨ intro \frac{[[Γ ⊢ ∂ A]]_{P(E)⌊ϕ} [[Γ ⊢ ∂ B]]_{P(E)⌊ψ}}{[[Γ ⊢ ∂ (A ∨ B)]]_{P(E)⌊ϕ∨ψ}}

B.6 ) Introduction

) intro \frac{Γ ⊢ A Γ, A ⊢ B}{Γ ⊢ A ) B}  ) intro \frac{[[Γ ⊢ ∂ A]]_{P(E)⌊ϕ} [[Γ, A ⊢ ∂ B]]_{P(E)⌊ψ}}{[[Γ ⊢ ∂ (A ) B)]]_{P(E)⌊ϕ)ψ}}

B.7 ∂ Introduction

∂_{true} intro \frac{[[Γ ⊢ A]]_{P(E)⌊ϕ}}{[[Γ ⊢ ∂ A]]_{P(nil)⌊true}}  ∂_{false} intro \frac{[[Γ ⊢ ¬A]]_{P(E)⌊ϕ}}{[[Γ ⊢ ∂ A]]_{P(nil)⌊false}}

B.8 ∀ Elimination

∀ elim \frac{[[Γ, [[∂ ∀x:τ.A]]_{P(E′)}, Δ, [[∂ A⟨t/x⟩]]_{P(E′′)} ⊢ A]]_{P(E)⌊ϕ}}{[[Γ, [[∂ ∀x:τ.A]]_{P(E′)}, Δ ⊢ A]]_{P(E)⌊ϕ}}

∀ elim \frac{[[Γ, [[∀x:τ.∂ A]]_{P(E′)}, Δ, [[∂ A⟨t/x⟩]]_{P(E′′)} ⊢ A]]_{P(E)⌊ϕ}}{[[Γ, [[∀x:τ.∂ A]]_{P(E′)}, Δ ⊢ A]]_{P(E)⌊ϕ}}

∀ elim \frac{Γ, ∀x:τ.A, A⟨t/x⟩, Δ ⊢ B}{Γ, ∀x:τ.A, Δ ⊢ B}

B.9 ¬ Elimination

¬ elim \frac{Γ, ¬A, Δ ⊢ A}{Γ, ¬A, Δ ⊢ \{\}}

B.10 ∨ Elimination

∨ elim \begin{matrix}[[Γ, A, Δ ⊢ C]]_{P(E)⌊ϕ} & [[Γ, B, Δ ⊢ C]]_{P(E)⌊ψ} \\ [[Γ, Δ ⊢ ∂ A]]_{P(E)⌊α} & [[Γ, Δ ⊢ ∂ B]]_{P(E)⌊β} \\ [[Γ, A ∨ B, Δ ⊢ C]]_{P(E)⌊(α∧ϕ)∨(β∧ψ)} \end{matrix}

B.11 Induction on Lists

induction \begin{matrix}[[Γ, x:list(τ), Δ ⊢ A⟨[ ]/x⟩]]_{P′(E)⌊ϕ} \\ [[Γ, x:list(τ), Δ, v_{0}:τ, v_{1}:list(τ), [[A⟨v_{1}/x⟩]]_{P′(E′)} ⊢ A⟨[v_{0}|v_{1}]/x⟩]]_{P′(E)⌊ψ} \\ [[Γ, x:list(τ), Δ ⊢ A]]_{P(E)⌊P′(E)} \end{matrix}

E′ is the environment at the time of application of the rule, and P′ is defined by P′(E′) ⌊x= [ ] ∧ ϕ ∨ ∃v0:τ.∃v1:τ.x=_{list(τ)} [v0 | v1] ∧ ψ

B.12 Substitution

sub \frac{Γ ⊢ [[B ⌊ C]]_{P(E)⌊ψ} Γ ⊢ [[A⟨C/B⟩]]_{P(E)⌊ψ∧ϕ}}{Γ ⊢ [[A]]_{P(E)⌊ϕ}}  rewrite \frac{Γ ⊢ [[E]]_{P(E)⌊ϕ}}{Γ ⊢ [[D]]_{P(E)⌊ϕ}}

B.13 New Hypotheses

lemma \frac{[[Γ, [[B]]_{P′(nil)} ⊢ A]]_{P(E)⌊ϕ}}{[[Γ ⊢ A]]_{P(E)⌊ϕ}}

C Two Coded Rules

C.1 ∂_{true} introduction

The rule:

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

is implement like this:

%%% File:     dec.pl
%%% Author:   Tom Chothia <tomc@kintore.dai.ed.ac.uk>
%%% Created:  Tue Jul 14 1998
:- module( 'rules_intro_dec', [\,] ).
:- use_module( ['../../utility','../../access',library(lists),
                '../../substitution'] ).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% d true:             G ==>{P(e) iff o} A
%               ----------------------------
%               G ==>{P(nil) iff dtrue(o)} A dec
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
rule( intro( True ), Conjecture, [SubConjecture] ) :-
        parser:truesymbol( True ),
        % decompose input conjecture and check it is a decidability
        conclusion( Conjecture, ConclusionDA ),
        decidability( ConclusionDA, _),
        subexp(ConclusionDA, SubConclusion ),
        hypotheses( Conjecture, Hypotheses ),
        extract( Conjecture, Extract ),
        head( Extract, Head),
        relation_number( Head, RelNumber ),
        parameters(Head, [\,]-[\,]),

        body( Extract, DtBody ),
        dectrue(DtBody, Body),
        % assemble sub extract
        extract( SubConjecture, SubExtract ),
        head( SubExtract, SubHead),
        relation_number( SubHead, RelNumber ),
        body( SubExtract, Body ),
        % assemble the sub conclusion
        hypotheses( SubConjecture, Hypotheses ),
        conclusion( SubConjecture, SubConclusion ),
        extract( SubConjecture, SubExtract ).

C.2 ∀ elimination

And the rule:

\frac{Γ, A[t/x]_{subs(α,t,x)} ⊢_{ϕ} B}{Γ, (∀x.A)_{α} ⊢_{ϕ} B} ∀ elim

is implemented thus:

%%% File:     forall.pl
%%% Author:   Tom Chothia <tomc@braemar.dai.ed.ac.uk>
%%% Created:  Mon Jul 27 1998

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% forall elimination:   G,forall( x:s, A ){a}, A[t/x]{subs(a,t,x)} ==>{o} L
%                       ----------------------------------------------------
%                            G, forall( x:s, A ){a} ==>{o} L
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- module( 'rules_elim_forall', [\,] ).
:- use_module( ['../../utility','../../access',library(lists),

        '../../substitution'] ).
rule( elim( Term, Number ), Sequent, [SubSequent] ) :-
integer( Number ),
% decompose sequent and hypothesis
hypotheses( Sequent, Hypotheses ),
conclusion( Sequent, Conclusion ),
extract( Sequent, Extract ),
nth( Number, Hypotheses, Hypothesis ),
hypothesis( Hypothesis, HypBody ),
extract( Hypothesis, HypExt ),
universal_quantifier( HypBody, _),
bound_expression( HypBody, BoundExp ),
bound_variable( HypBody, BoundVar ),
variable_type( BoundVar, Type ),
variable_name( BoundVar, VarName ),
environment( Hypotheses, Environment ),
% Make SubSequent Hyps.
substitute( BoundExp, [VarName], [Term], NewHypB,
                                       [BoundVar|Environment] ),
substitution(NewHypExt,_),
subs_exp(NewHypExt,HypExt),
new_term(NewHypExt,VarName),
old_term(NewHypExt,Term),
hypothesis( NewHyp, NewHypB ),
extract( NewHyp, NewHypExt ),
append( Hypotheses, [NewHyp], SubHypotheses ),
% Make subsequent.
hypotheses( SubSequent, SubHypotheses ),
conclusion( SubSequent, Conclusion ),
extract( SubSequent, Extract ).

References

[Bar84] Barendregt. Lambda calculus : its Syntax and Semantics. North Holland, 1984.

[BvHHS90] Bundy, van Harmelen, Horn, and Smaill. The oyster-clam system. 10th International Conference on Automated Deduction, 1990.

[Con82] Constable. Programs as proofs. Technical Report Tech report TR 82-532, Dept of Computer Science, Cornell University, 1982.

[Cur58] Curry. Combinatory logic vol. 1. 1958.

[EucBC] Euclid. The Books of Elements, c. 300BC.

[Fri90] Fribourg. Extracting logic programs from proof that use extented prolog execution and induction. Logic Programming:Proceedings of 7th International Congress, 1990.

[Gen69] G. Gentzen. The Collected Papers of Gerhard Gentzen. North Holland, 1969. Edited by Szabo, M. E.

[Ham78] Hamilton. Logic for Mathematicians. CUP, 1978.

[How58] Howard. The formulae-as-types notion of construction. 1958.

[Kol32] Kolmogorov. Mathematische zeitschrift: Zur deutung der intuitionistischenn logik. 1932.

[LP90] Lau and Prestwich. Top down synthesis of recursive logic procedures from first order logic specification. Logic Programming:Proceedings of 7th International Congress, 1990.

[ML84] Martin-Löf. Constructive mathematics and computer programming. Proceedings of 6th International Congress for Logic, Methodology and Philosophy of Science, 1984.

[RKSW94] Richards, Kraan, Smaill, and Wiggins. Mollusc: a general proof development shell for sequent-based logics. Proceedings of CADE 12, Springer Verlag LNAI 723, 1994.

[RS95] Richards and Smail. Mollusc User’s Guide, 1995. Version 1.3.

[Wig92] Wiggins. Synthesis and transformation of logic programs in the whelk proof development system. Proceedings of JICSLP’92, 1992.