An Implementation of G4ip in Pizza
Warning:
This page is now rather old! While you might still be interested
in the algorithms, Robert Macdonald reported that Pizza and the current Java
implementation (version 1.3.0) do not work together. This means you need to
install an older Java version if you want to recompile the files given below.
I am happy to answer all question concerning the prover, but be aware that
currently for any kind of Java stuff I am using MLJ, which as of writing
this note has not yet been made available for the general audience (maybe
in the future also its OCaml equivalent). So I am not very fluent in Pizza
anymore. Update Pizza development is continued and starting from version
0.40 it should work
with recent Java implementations.
Jump to the implementation.
Introduction
A convenient representation of intuitionistic logic is Getzen's
sequent calculus LJ (also G1i). A sequent of LJ can be proved
by applying inference rules until one reaches axioms, or can make no further
progress in which case one must backtrack or even abandon the search.
Unfortunately an interpreter for LJ using this depthfirst strategy cannot
guarantee termination of the proof search. Several modifications can be
made to LJ's inference rules without loss of soundness and completeness.
As result an efficient depthfirst proof search can be designed for the
propositional fragment of intuitionistic logic. The name G4ip has been
assigned to the corresponding calculus in
[Troelstra and Schwichtenberg, 1996].
This calculus is also known as LJT which has been studied thoroughly
in [Dyckhoff, 1992]. The inference rules of
G4ip are given here.
It is not very complicated to implement an interpreter for G4ip using a logic
programming language (backtracking is directly supported within the language).
Our first implementation is written in the logic programming language
Lambda Prolog
and can be found here. Another implementation by
Hodas and Miller written in Lolli
can be found here
(see [Hodas and Miller, 1994]). These are simple and
straightforward implementations of G4ip's rules. On the other hand it seems
that imperative languages need a rather high overhead of code when implementing
a logic calculus. For example choice points are usually implemented with stacks.
We shall demonstrate the implementation technique of success
continuations which provides an equally simple method for implementing logic calculi
in imperative languages. This technique is not new: it has been introduced in
[Carlsson, 1984]. This paper presents a rather technical
implementation of Prolog in LISP. Later an excellent paper,
[Elliot and Pfenning, 1991], appeared which
describes a fullfledged implementation of Lambda Prolog in SML.
We demonstrate the technique of success continuations for G4ip in
Pizza.
Pizza is an objectoriented programming language and an attractive extension of
Java. Although Pizza is a superset of
Java, Pizza programs can be translated into Java or compiled into ordinary
Java Byte Code (see [Odersky and Wadler, 1997]
for a technical introduction to Pizza). We make use of the following two new
features of Pizza:
 higherorder functions, i.e. functions may be passed as parameters or returned
from methods,
 class cases and pattern matching: this allows much simpler and more readable code.
These features are not directly present in Java, but Pizza makes them accessible by
translating them into Java. Pizza provides the programmer with the same
extensive libraries for graphic and network applications as Java. The higherorder
functions are essential for the technique of success continuations. The success
continuations are functions passed as parameters or returned as values.
The Representation of Formulae and Sequents
Amongst the new language features of Pizza are class cases and pattern
matching, which provide a very pleasant syntax for algebraic data types. The
formulae of G4ip are specified by the following grammar:
F ::= false  A  F & F  F v F  F > F
The class cases allow a straightforward implementation of this specification;
it is analogous to the SML implementation of
Lambda Prolog's
formulae in [Elliot and Pfenning, 1991]. The class
of formulae for G4ip is given below:
 public class Form {
 case False();
 case Atm(String c);
 case And(Form c1,Form c2);
 case Or(Form c1,Form c2);
 case Imp(Form c1,Form c2);
 }
Two examples that illustrate the use of the representation are as follows:
p > p
is represented as Imp(Atm("p"),Atm("p"))
a v (a > false)
is represented as Or(Atm("a"),Imp(Atm("a"),False()))
The class cases of Pizza also support an implementation of formulae specified
by a mutually recursive grammar. This is required, for example, when
implementing hereditary Harrop formulae.
The sequents of G4ip, which have the form Gamma=>G
, are represented
by means of the class below. The lefthand side of each sequent is specified by a multiset
of formulae. Therefore, we do not need to worry about the order in which the
formulae occur.
 public class Sequent {
 Form G;
 Context Gamma;
 public Sequent(Context _Gamma, Form _G) {...};
 }
We have a constructor for generating new sequents during proof search.
Context
is a class which represents multisets; it is a simple
extension of the class Vector
available in the Java libraries.
This class provides methods for adding elements to a multiset (add
),
taking out elements from a multiset (removeElement
) and testing
the membership of an element in a multiset (includes
).
The Technique of Success Continuations
We have to distinguish between the concepts of proof obligations (which must
be proved) and choice points (which can be tried out to construct a proof).
The first argument of the method prove
is the sequent being
proved; the second argument is an anonymous function. The function prove
is now
of the form prove(sequent,sc)
. Somewhat simplified the
first argument is the leftmost premise and the second argument sc
,
the success continuation, represents the other proof obligations. In case we
succeed in proving the first premise we then can attempt to prove the other
premises. The technique of success continuations will be explained using the following
proof (each sequent is marked with a number):
The inference rules fall into three groups:
 inference rules with a single premise (e.g. >_R, &_L),
 inference rules with two premises (e.g. v_L) and
 inference rules without premises (e.g. Axiom).
The following picture shows the order in which the sequents are being proved.
Suppose we have called prove
with a sequent s and a
success continuation is. The inference rules of the first
group manipulate s obtaining s' and call prove
again with the new sequent s' and the current success continuation
(Steps 12, 34 and 56). The inference rules
of the second group have two premises, s1 and s2.
These rules call prove
with s1 and a new success
continuation prove(s2,is)
(Step 23).
The third group of inference rules only invoke the success continuation
if the rule was applicable (Steps 45 and 67).
We are going to give a detailed description of the code for the rules: &_L,
>_R, v_Ri, v_L and Axiom. The function prove
receives as arguments
a sequent Sequent(Gamma,G)
and a success continuation
sc
. It enumerates all formulae as being principal and
two switch statements select a corresponding case depending on the form
and the occurrence of the principal formula.
The &_L rule is in the first group; it modifies the sequent being proved and calls
prove
again with the current success continuation sc. The code is as
follows (Gamma
stands for the set of formulae on the lefthand
side of a sequent excluding the principal formula; G
stands
for the goal formula of a sequent; B
and C
stand
for the two components of the principal formula).
 case And(Form B, Form C):
 prove(new Sequent(Gamma.add(B,C),G),sc); break;
The code for the >_R rule is similar:
 case Imp(Form B, Form C):
 prove(new Sequent(Gamma.add(A),B),sc); break;
The v_Ri rule is an exception in the first group. It breaks up a goal
formula of the form B1 v B2
and proceeds with one of its component.
Since we do not know in advance which component leads to a successful proof we have
to try both. Therefore this rule acts as a choice point, which is encoded by a
recursive call of prove
for each case.
 case Or(Form B1,Form B2):
 prove(new Sequent(Gamma,B1),sc);
 prove(new Sequent(Gamma,B2),sc); break;
The v_L rule falls into the second group where the current success
continuation, sc, is modified. It calls prove
with the first premise,
B,Gamma=>G
, and wraps up the success continuation with the
new proof obligation, C,Gamma=>G
. The construction
fun()>void {...}
defines an anonymous function: the new
success continuation. In case the sequent B,Gamma=>G
can be
proved, this function is invoked.
 case Or(Form B,Form C):
 prove(new Sequent(Gamma.add(B),G),

fun()>void {prove(new Sequent(Gamma.add(C),G),sc);}
 ); break
The Axiom rule falls into the third group. It first checks if the
principal formula (which is an atom) matches with the goal formula and
then invokes the success continuation sc in order to prove all remaining
proof obligations.
 case Atm(String c):
 if (G instanceof Atm) {
 if (G.c.compareTo(c) == 0) { sc(); }
 } break;
The proof search is started with an initial success continuation is.
This initial success continuation is invoked when a proof has been found.
In this case we want to give some response to the user, an
example for the initial success continuation could be as follows:
 public void initial_sc() { System.out.println("Provable!"); }
Suppose we attempt to start the proof search with prove(p,p => p,is)
.
We would find that the prover responds twice with "Provable!"
, because
it finds two proofs. In our implementation this problem is avoided by encoding
the proof search as a thread. Whenever a proof is found, the initial success
continuation displays the proof and suspends the thread. The user can
decide to resume with the proof search or abandon the search.
Conclusion
The implementation cannot be considered as optimal in terms of speed.
A much more efficient algorithm for G4ip (but less clear) has been
implemented by Dyckhoff in Prolog. Similar ideas can be encoded in our
Pizza implementation; but our point was not the efficiency but the clarity
of the implementation using success continuations.
The technique is applicable elsewhere whenever backtracking is required. We
compared the code of our implementation with an implementation in
Lambda Prolog:
the ratio of code is approximately 2 to 1.
(see LambdaProlog code and
Pizza code).
This result is partly due to the fact that we had to implement a class for
multisets. In a future version of Java, we could have accessed a package
in the library. The technique of success continuation can also be applied
to a firstorder calculus as shown in [Elliot and Pfenning, 1991],
but the required mechanism of substitution needs to be implemented separately.
However, we think the technique of success continuations provides a remarkable
simple implementation for logic calculi.
We had to make some compromises in order to support as many platforms
as possible. This should change with the release of new browsers and a stable
Javaspecification (resp. Pizzaspecification).
A paper about the implementation appeared in the LNAI series No 1397,
Automated Reasoning with Analytic Tableaux and Related Methods,
ed. Harry de Swart, International Conference Tableaux'98 in Oisterwijk,
The Netherlands. The title is: Implementation of Proof Search in
the Imperative Programming Language Pizza (pp. 313319). The paper can be
found here: DVI, Postscript
(© SpringerVerlag LNCS).
Acknowledgements: I am very grateful for Dr Roy Dyckhoff's constant
encouragement and many comments on my work. I thank Dr Gavin Bierman who
helped me to test the prover applet.
Implementation
Readme
Prover Applet
Jar Version
(slightly faster, but requires Netscape 4 or MS Explorer 4).
References

[Carlsson, 1984]
M. Carlsson, On Implementing Prolog in Functional Programming,
New Generation Computing, pp 347359.

[Dyckhoff, 1992]
R. Dyckhoff,
ContractionFree Sequent Calculi for Intuitionistic Logic,
Journal of Symbolic Logic 57(3), pp 795807.

[Elliot and Pfenning, 1991]
C. Elliot,
F. Pfenning,
A SemiFunctional Implementation of a HigherOrder Programming Language,
In Peter Lee, editor, Topics in Advanced Language Implementation, MIT Press,
pp 289352.
Available electronically.

[Hodas and Miller, 1994]
J. Hodas,
D. Miller,
Logic Programming in a Fragment of Intuitionistic Linear Logic,
Information and Computation 110(2), pp 327365.
Available electronically.

[Odersky and Wadler, 1997]
M. Odersky,
P. Wadler,
Pizza into Java: Translating Theory into Practice,
In Proceedings of the 24th ACM Symposium on Principles of Programming Languages.
Available electronically.

[Troelstra and Schwichtenberg, 1996]
A. Troelstra,
H. Schwichtenberg,
Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science,
Cambridge University Press.
Christian Urban
Last modified: Sun Sep 23 12:04:47 BST 2001