On a simple example, we contrast the style of inductive proofs conducted in logical frameworks, logic and functional logic programs. We highlight hypothetical reasoning in logic programming, solving goals under local assumptions. Hypothetical reasoning in Prolog requires building a meta-circular interpreter, using Prolog's meta-call mechanism.
Our running example is a simple inductive proof that the mirror operation on binary trees is involution, that is, is its own inverse. Formally (in Haskell notation, which is quite close to the mathematical one), we define the inductive datatype of binary trees
data Btree a = Leaf a | Node (Btree a) (Btree a) deriving Showand the operation to produce the mirror image of the tree, by recursively exchanging left and right branches:
mirror :: Btree a -> Btree a
mirror (Leaf x) = Leaf x
mirror (Node t1 t2) = Node (mirror t2) (mirror t1)
Here is a sample btree and the result of applying the mirror operation to it, once and twice:
-- A sample btree
btree1 = Node
(Node (Leaf 0) (Leaf 1))
(Leaf 2)
btree1' = mirror btree1
-- Node (Leaf 2) (Node (Leaf 1) (Leaf 0))
btree1'' = mirror btree1'
-- The same as btree1
We see that applying mirror twice yields the original tree. That is the general result we wish to prove:
mirror . mirror == id
or: mirror is its own inverse.
forall X. exists Y. prop (X,Y).Many theorems can be stated in this way, for example, the theorem that there is an infinite number of primes:
forall X:prime. exists Y:prime. Y > X.A constructive proof of such a formula is a computational procedure that given any
X will produce, in finite time, Y so that prop(X,Y) holds. In the case of the infinitude of primes, such a procedure was proposed by Euclid.
To formulate the mirror involution theorem, we first define the type of binary trees with two constructors leaf and node.
btree: type.
leaf: nat -> btree.
node: btree -> btree -> btree.
We then define the mirror operation. It is written as a binary relation, relating a tree with its mirror image. The mode declaration however makes mirror a function: the first argument of the mirror relation is the input and the second argument is the output:
mirror: btree -> btree -> type.
%mode mirror +B1 -B2.
mr-l: mirror (leaf N) (leaf N).
mr-b: mirror (node B1 B2) (node B2' B1')
<- mirror B1 B1'
<- mirror B2 B2'.
%worlds () (mirror _ _).
%total {B1} (mirror B1 _).
The labels mr-l and mr-b name the two clauses of the mirror function. We also regard the labels as the two constructors of the proof object of the type mirror B1 B2, witnessing that B2 is the mirror image of B1. We assert that mirror is a total function on binary trees; Twelf agrees.
We now state the main theorem: mirror is its own inverse. The theorem is written as a forall-exists formula:
mirror-inv-thm: mirror B B' -> mirror B' B -> type.
%mode mirror-inv-thm +P1 -P2.
(The variables B and B' are implicitly universally quantified.) In full, the formula is
forall B:btree, B':btree, P1:mirror B B'. exists P2:mirror B' B. true.In words: for all binary trees
B and B' such that B' is the mirror image of B, there exists a proof that B is the mirror image of B'.
We write the constructive proof of that formula as a computational procedure that computes the proof of mirror B' B from the proof of mirror B B'. In other words, to prove the involution theorem stated as the type of mirror-inv-thm, we have to show how to construct the inhabitants of the type mirror-inv-thm:
-: mirror-inv-thm mr-l mr-l.
-: mirror-inv-thm (mr-b P1L P1R) (mr-b P2R P2L)
<- mirror-inv-thm P1L P2L
<- mirror-inv-thm P1R P2R.
%worlds () (mirror-inv-thm _ _).
%total {P1} (mirror-inv-thm P1 _).
Twelf type-checks the two clauses, verifying that the two cases, if terminate, do indeed produce the proof of mirror B' B from the proof of mirror B B'. To complete the proof, we assert on the last line that there are no other cases and that the computation always terminates. Twelf admits the totality assertion, thus verifying the proof. The overall proof appears so simple because the complex part -- verifying termination by structural induction -- is done by the meta-theoretical engine of Twelf.
Enkitei is an interactive system: it displays the current judgements and lets the user apply deduction steps by entering various tactics. A tactic can prove the current goal, produce a new one, or split the current goal into subgoals. The proof concludes when there are no more goals.
Although Enkitei is written in Prolog, it cannot use Prolog directly to prove judgements. After all, Enkitei deals with arbitrary first-order logic formulas, not restricted to Horn clauses. All in all, Enkitei had to solve the following problems:
The (very long) comments in the source code explain how all these problems have been solved. We extensively rely on Prolog's meta-call facilities. One may regard Enkitei as a greatly extended, stepping meta-circular Prolog interpreter. The code contains many tests and examples, including inductive proofs from Pierce's Software Foundations course.
The first example proves that zero is the right unit of addition. We define natural numbers and the addition relation, by consulting the following Prolog program.
nat(z).
nat(s(N)) :- nat(N).
plus(z,N,N).
plus(s(N),M,s(R)) :- plus(N,M,R).
Here is the transcript of the proof session. User's input is after the prompt Command >.
?- main( forall(N, nat(N) -> plus(N,z,N)) ).
eigenvars: []
================
forall(_G2202, (nat(_G2202)->plus(_G2202, z, _G2202)))
Command >intros. % apply introduction rules as far as possible.
nat(_G2238)
eigenvars: [_G2238]
================
plus(_G2238, z, _G2238)
Command >induction.
eigenvars: [z]
================
plus(z, z, z)
plus(_G2489, z, _G2489)
nat(_G2489)
eigenvars: [s(_G2489)]
================
plus(s(_G2489), z, s(_G2489))
Command >simpl. % ask Prolog to prove the goal in judgement 1. It succeeds.
plus(_G2489, z, _G2489)
nat(_G2489)
eigenvars: [s(_G2489)]
================
plus(s(_G2489), z, s(_G2489))
Command >constructor. % unfold the definition of plus in the goal.
plus(_G2489, z, _G2489)
nat(_G2489)
eigenvars: [s(_G2489)]
================
plus(_G2489, z, _G2489)
Command >assumption. % search for the goal among assumptions, so to prove it.
QED
To prove the mirror theorem, we enter the following Prolog program, defining binary trees, the mirror relation and the theorem.
btree(leaf(_)).
btree(node(X,Y)) :- btree(X), btree(Y).
mirror(leaf(X),leaf(X)).
mirror(node(X,Y),node(Y1,X1)) :- mirror(X,X1), mirror(Y,Y1).
% The theorem: mirror is involutive
thm(BT) :- mirror(BT,BT1), mirror(BT1,BT).
Here is the abbreviated transcript of the proof session.
?- main( forall(B, btree(B) -> thm(B)) ).
Command >intros.
btree(_G2236)
eigenvars: [_G2236]
================
thm(_G2236)
Command >induction.
eigenvars: [leaf(_G2557)]
================
thm(leaf(_G2557))
thm(_G2523)
thm(_G2528)
btree(_G2523)
btree(_G2528)
eigenvars: [node(_G2523, _G2528)]
================
thm(node(_G2523, _G2528))
Command >simpl. % ask Prolog to solve the first goal, proving the judgement.
Command >destruct. move(3). destruct. % unfold thm in assumptions.
mirror(_G2806, _G2807)
mirror(_G2807, _G2806)
mirror(_G2818, _G2819)
mirror(_G2819, _G2818)
btree(_G2818)
btree(_G2806)
eigenvars: [_G2807, _G2819, node(_G2818, _G2806)]
================
thm(node(_G2818, _G2806))
Command >constructor. intros. constructor. intros. % unfold thm.
mirror(_G2806, _G2807)
mirror(_G2807, _G2806)
mirror(_G2818, _G2819)
mirror(_G2819, _G2818)
btree(_G2818)
btree(_G2806)
eigenvars: [_G2807, _G2819, node(_G2818, _G2806)]
================
mirror(_G2818, _G3106)
mirror(_G2806, _G2807)
mirror(_G2807, _G2806)
mirror(_G2818, _G2819)
mirror(_G2819, _G2818)
btree(_G2818)
btree(_G2806)
eigenvars: [_G2807, _G2819, node(_G2818, _G2806)]
================
mirror(_G2806, _G3105)
mirror(_G2806, _G2807)
mirror(_G2807, _G2806)
mirror(_G2818, _G2819)
mirror(_G2819, _G2818)
btree(_G2818)
btree(_G2806)
eigenvars: [_G2807, _G2819, node(_G2818, _G2806)]
================
mirror(node(_G3105, _G3106), node(_G2818, _G2806))
Command >assumption. assumption. % prove the first two judgements.
mirror(e99, e96)
mirror(e96, e99)
mirror(e98, e97)
mirror(e97, e98)
btree(e98)
btree(e99)
eigenvars: [e96, e97, node(e98, e99)]
================
mirror(node(e96, e97), node(e98, e99))
Command >constructor. intros. assumption. assumption. % prove the rest.
QED
Benjamin C. Pierce et al. Software Foundations. Course Notes, 2009.
< http://www.seas.upenn.edu/~cis500/current/sf/html/ >
The Coq Team: Coq Reference Manual, v8.1
< http://coq.inria.fr/V8.1/refman/Reference-Manual002 >
Specifically:
Chapter 4: Calculus of Inductive Constructions
Chapter 8: Tactics
Frederic Portoraro: Automated Reasoning
The Stanford Encyclopedia of Philosophy (Winter 2008 Edition), Edward N. Zalta (ed.).
< http://plato.stanford.edu/archives/win2008/entries/reasoning-automated/ >
forall X. g we introduce a fresh constant c (which has not been used in the proof before) and attempt to prove the formula g with X replaced with c. Such a fresh constant is called ``eigen-variable.''
Most texts on deduction calculi (such as the ``Automated reasoning'' entry in the Stanford Encyclopedia of Philosophy) say nothing more about eigen-variables, leaving the reader to puzzle over the question why the name eigen-variable was chosen for constants.
The LICS2003 paper by Miller and Tiu is a rare text that describes the use of eigen-variables as variables, that is, to mark the place for substitution. Miller and Tiu point out that although Gentzen never substituted for eigen-variables when constructing proofs (so, eigen-variables were indeed constants), Gentzen did substitute for eigen-variables in meta-theory, when transforming proofs, e.g., to eliminate cuts. Miller and Tiu discuss extended sequent calculi that do treat eigen-variables as variables, and propose a sequent calculus that harmonizes the constant--variable treatment of eigen-variables.
In this article, we illustrate the constant--variable duality of eigen-variables on a simple example. We use classical natural deduction (NK) with equality rather than intuitionistic sequent calculus. Crucially however, our calculus, like that of Miller and Tiu, supports definitions. It is in the applications of definitions where the variable aspect of eigen-variables emerges. To be sure, we can treat eigen-variables ``classically'', as constants during the proof construction, all the time. In fact, we start with such a classical derivation. We then show the abbreviation of thus constructed proof, eliminating the use of equality and injectivity axioms. We replace the axioms with an inference rule that may treat eigen-variables as variables, substituting for them when applying definitions to hypotheses. The new inference rule is particularly easy to apply using unification. The simplified calculus underlies the Prolog implementation of Enkitei, a natural deduction proof system with equality and definitions.
We are interested in classical natural deduction proofs, that is, in finding a derivation for a judgement
hs |- gwhere
g is a formula and hs is a possibly empty set of formulas (assumptions). Formula g is an arbitrary first-order formula; & will stand for conjunction and | for disjunction.
Let us enter the following definitions:
nat(0).
nat(X) :- pos(X).
pos(s(X)) :- nat(X).
where 0 and s are function symbols (of arity zero and one, respectively), and nat and pos are predicate letters of arity one. X is a schematic variable. (The definitions are in fact inductive; however, we won't be concerned with induction here).
We may regard the definitions as axioms
forall U. nat(U) <-> U = 0 | pos(U)
forall U. pos(U) <-> exists V. U = s(V) & nat(V)
We shall also assume the following axioms of equality for terms (injectivity)
forall X Y. s(X) = s(Y) -> X = Y
forall X. not (s(X) = 0)
along with the standard introduction and elimination rules for equality:
t1
[] |- t1 = t1
t1, t2 and a formula g, the judgments
[] |- t1 = t2
[] |- g
let us derive [] |- g{t1/t2} where g{t1/t2} is g with every occurrence of t1 replaced with t2.Our running example will be proving the theorem forall X. nat(s(X)) -> pos(s(X)) using the definitions of nat and pos shown earlier. We first demonstrate a ``classical'' derivation, using only the standard (and hence, boring) steps and indeed regarding the definitions as (domain) axioms. Thereby we demonstrate that we are not doing anything fishy; mainly, we will get an idea for short-cutting the most tedious steps.
Our goal is to derive the judgement
[] |- forall X. nat(s(X)) -> pos(s(X))By appealing to the forall-introduction rule of NK we convert our goal to
[] |- nat(s(c)) -> pos(s(c))where
c is a fresh constant, the function symbol of arity 0 -- the eigen-variable. After the implication introduction rule of NK, the goal judgement becomes
nat(s(c)) |- pos(s(c))The axiom for
pos (after instantiating U with s(c)) lets us conclude
exists V. s(c) = s(V) & nat(V) |- pos(s(c))We could then prove our goal judgment by the cut rule if we could prove
nat(s(c)) |- exists V. s(c) = s(V) & nat(V).
Let us indeed prove the latter judgment. We instantiate V to be c, converting the goal to
nat(s(c)) |- s(c) = s(c) & nat(c)The formula
s(c)=s(c) holds by reflection, and we only need to prove
nat(s(c)) |- nat(c)We may try the
nat axiom in the way we have just used the pos axiom, to re-write the conclusion of the judgement. It is easy to see that it won't do us any good. We have to re-write the assumption of the judgement.
The nat axiom after instantiating U with s(c) lets us conclude
nat(s(c)) |- s(c) = 0 | pos(s(c))If we could only prove
(s(c) = 0 | pos(s(c))) |- nat(c)we would derive the desired judgement, again by applying cut. We hence need to prove two judgements:
s(c) = 0 |- nat(c)
pos(s(c)) |- nat(c)
We get the first by contradiction (from the axiom not(s(c)=0)). For the latter, we apply the axiom pos to the assumption (as we have applied nat just before), giving us this judgement to prove:
exists V. s(c) = s(V) & nat(V) |- nat(c)or, after the existential elimination:
s(c) = s(d) & nat(d) |- nat(c)where
d is another eigen-variable. Applying the injectivity gives us
c = d & nat(d) |- nat(c)which is derivable by the equality elimination rule. We are done.
That was messy, wasn't it? Let us attempt to generalize and simplify the derivation steps. Suppose we have the following definition
p(0).
p(X) :- q(X).
where p and q are some predicates. We can write the definition in the form of an axiom
forall U. p(U) <-> U = 0 | q(U)Suppose we wish to prove the judgement
hs |- p(c) (where c is a constant; it could have been any term). If we follow the boring steps above we convert the judgement to
hs |- (c = 0 | q(c)).and then elect to continue the proof search with
hs |- q(c). We could obtained the latter judgement directly, if we unified p(c) with the head of the p definition in its original clausal form. There is no surprise here: the `direct' step is mere resolution. We stress that in this step, c is treated as a constant, not subject to substitutions.
Let us take a different judgement: hs, p(c) |- g where g is some formula. The boring steps of using the definition of p in its axiomatic form gives us two new judgements to prove
c=0 |- g
q(c) |- g
The first judgement after the equality elimination rule becomes [] |- g{c/0}. Again, we could have obtained the two judgements in one step, if we unified p(c) against the two clauses of p's original definition. If more than one clause unify, we obtain more than one judgement to prove. If none unify, we obtain the proof by contradiction. Crucially, during this step, c is being treated as a variable. It is now subject to substitution.
To summarize: when applying a definition to the conclusion of a judgement, we treat an eigen-variable as a constant during unification. When applying a definition to an assumption of a judgement, we treat eigen-variables as variables, subject to unification and substitution.
The new rules of applying definitions let us drop the axioms of equality. In other words, equality becomes definable:
eq(X,X).We can prove, for example, that our defined equality is transitive. The goal
[] |- forall X Y Z. (eq(X,Y) & eq(Y,Z)) -> eq(X,Z)after a series of introductions becomes
eq(c,d), eq(d,e) |- eq(c,e)where
c, d, and e are eigen-variables. We apply the definition of eq to the assumption, identifying eigen-variables c and d and obtaining
eq(c,e) |- eq(c,e)which is the axiom. The Prolog Enkitei code have many more examples of applying definitions.
Classically, eigen-variables are constants, not to be substituted for during the proof construction. However, the equality elimination rule does permit replacement of arbitrary terms, which are not necessarily variables. This fact lets us design an alternative to equality axioms, relying on unification and treating eigen-variables as regular variables when operating on assumptions of a judgement. The alternative inference rule is especially useful when applying definitions.
Frederic Portoraro: Automated Reasoning
The Stanford Encyclopedia of Philosophy (Winter 2008 Edition), Edward N. Zalta (ed.).
< http://plato.stanford.edu/archives/win2008/entries/reasoning-automated/ >
Dale Miller and Alwen Tiu: A proof theory for generic judgments. An extended abstract.
Proceedings of LICS 2003, Phokion Kolaitis, ed. Ottawa, July 2003, pp. 118-127.
oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML