We derive a sequence of minimalist theorem provers for the implicational fragment of intuitionistic logic. Starting from Roy Dyckhoff's sound and complete LJT calculus we apply declarative program transformations steps, while highlighting connections, via the Curry-Howard isomorphism to type inference mechanisms for the simply typed lambda calculus. We follow a test-driven development process with testing on formulas known to be tautologies that are inferred as types of lambda terms, as well as as by using exhaustive and random formula generators. We chose Prolog as our meta-language. Being derived from essentially the same formalisms as those we are covering reduces the semantic gap and results in surprisingly concise and efficient declarative implementations. Our code is available at: https://github.com/ptarau/TypesAndProofs.
The implicational fragment of propositional intuitionistic logic can be defined by two axiom schemes: K : A ! (B ! A) S : (A ! (B ! C)) ! ((A ! B) ! (A ! C)) and the modus ponens inference rule: MP : A; A ! B ` B.
In its simplest form, the Curry-Howard isomorphism [
Besides the syntactically identical axioms for the combinators S and K and the axioms of the logic, an intuitive reason for this isomorphism between types and formulas is that one can see propositions as sets of proofs on which functions, corresponding to implications A ! B act as transformers of proofs of A into proofs of B.
Our interest in theorem provers for this minimalist logic fragment has been triggered
by its relation, via the Curry-Howard isomorphism, to the inverse problem
corresponding to inferring types for lambda terms, type inhabitation, with direct applications to
the generation of simply typed lambda terms that meet a given specification, more
efficiently than trying out all possible terms of increasing sizes for a match [
At the same time, generating large lambda terms can help test correctness and
scalability of compilers for functional languages [
As SAT-problems are solvable quite efficiently in practice, despite being NP-complete,
one might want to see if this extends to the typical PSPACE-complete problem of
finding proofs for intuitionistic propositional calculus formulas. If so, an alternate method
would emerge for finding types and inhabitants of comparable sizes as those obtained
from Boltzmann samplers [
Given the possibly subtle semantic variations between our provers, we have also focused on setting up an extensive combinatorial and random testing framework to ensure correctness, as well as to evaluate their scalability and performance.
The paper is organized as follows. Section 2 overviews sequent calculi for implicational propositional intuitionistic logic. Section 3 describes a direct encoding of the LJT calculus as a Prolog program. Section 4 describes successive derivation steps leading to simpler and/or faster programs, including nested Horn clause representations and adaptations to support classical logic via Glivenko’s double-negation translation. Section 5 describes our testing framework and section 6 provides performance evaluation. Section 7 overviews related work and section 8 concludes the paper. 2
Proof systems for implicational intuitionistic propositional logic
Initially, like for other fields of mathematics and logic, Hilbert-style axioms were
considered for intuitionistic logic. While simple and directly mapped to SKI-combinators
via the Curry-Howard isomorphism, their usability for automation is very limited. In
fact, their inadequacy for formalizing even ”hand-written” mathematics was the main
trigger of Gentzen’s work on natural deduction and sequent calculus, inspired by the
need for formal reasoning in the foundation of mathematics [
Thus we start with Gentzen’s own calculus for intuitionistic logic, simplified here to only cover the purely implicational fragment, given that our focus is on theorem provers working on formulas that correspond to types of simply-typed lambda terms. 2.1
Gentzen’s LJ calculus, restricted to the implicational fragment of
propositional intuitionistic logic
We assume familiarity with basic sequent calculus [
As one can easily see, when trying a goal-driven implementation that uses the rules in upward direction, the unchanged premises on left side of rule LJ3 would not ensure termination as nothing prevents A and G from repeatedly trading places during the inference process. 2.2
Dyckhoff’s LJT calculus, restricted to the implicational fragment of
propositional intuitionistic logic
Motivated by problems related to loop avoidance in implementing Gentzen’s LJ
calculus, Roy Dyckhoff [
A;G ` A A;G ` B G ` A!B A!B;G ` A B;G ` G
A!B;G ` G A;G ` A A;G ` B G ` A!B
B;A;G ` G A!B;A;G ` G D!B;G ` C!D B;G !G
(C!D)!B;G ` G LJ1 : LJ2 : LJ3 : LJT1 : LJT2 : LJT3 : LJT4 :
This avoids the need for loop checking to ensure termination. The rules work with
the context G being a multiset, but it has been shown later [
For supporting negation, one also needs to add LJT5 that deals with the special term f alse. Then negation of A is defined as A ! f alse.
LJT5 :
f alse;G ` G
Interestingly, as it is not unusual with logic formalisms, the same calculus has been
discovered independently in the 50’s by Vorob’ev and in the 80’s by Hudelmaier [
This brings up the question if, in the tradition of ”lean theorem provers”, we can build one directly from the LJT calculus, in a goal oriented style, by reading the rules from conclusions to premises.
Thus, we start with a simple, almost literal translation of rules LJT1 : : : LJT4 to Prolog with values in the environment G denoted by the variable Vs. lprove(T):-ljt(T,[]),!. ljt(A,Vs):-memberchk(A,Vs),!. ljt((A->B),Vs):-!,ljt(B,[A|Vs]). ljt(G,Vs1):-atomic(G), select((A->B),Vs1,Vs2), atomic(A), memberchk(A,Vs2), !, ljt(G,[B|Vs2]). ljt(G,Vs1):select( ((C->D)->B),Vs1,Vs2), ljt((C->D), [(D->B)|Vs2]), !, ljt(G,[B|Vs2]).
% LJT_1 % LJT_2 % LJT_3 % LJT_4
Note the use of select/3 to extract a term from the environment (a
nondeterministic step) and termination, via a multiset ordering based measure [
Note also that integers can be used instead of atoms, flexibility that we will use as needed.
Besides the correctness of the bf LJT rule set (as proved in [
This simpler form will facilitate our next transformations.
Extracting the proof terms (lambda terms having the formulas we prove as types) is achieved by decorating in the code with application nodes a/2, lambda nodes l/2 (with first argument a logic variable) and leaf nodes (with logic variables, same as the identically named ones in the first argument of the corresponding l/2 nodes).
The simplicity of the predicate bprove/1 and the fact that this is essentially the
inverse of a type inference algorithm (e.g., the one in [
Thus lambda nodes decorate implication introductions and application nodes decorate modus ponens reductions in the corresponding calculus. Note that the two clauses of ljs imp provide the target node T that, when seen from the type inference side, results from cancelling the source type S and the application type S ! T . Note also that we added in the third clause of ljs/3 a test eliminating non-tautologies, for faster rejection of unprovable formulas and modified the second clause of ljs imp/4 to make obvious the addition of lambda binders for assumptions C and D->B. Calling sprove/2 on the formulas corresponding to the types of the S; K and I combinators, we obtain: ?- sprove(((0->1->2)->(0->1)->0->2),X).
X = l(A, l(B, l(C, a(a(A, C), a(B, C))))). ?- sprove((0->1->0),X).
X = l(A, l(B, A)). ?- sprove((0->0),X).
X = l(A, A). % S % K % I
Note also the addition of the predicate head of that eliminates non-tautologies by making sure that in the third clause of ljs, the goal G is the last element of at least one implication chain. More on why this works, in subsection 4.4.
Replacing the multiset context with sets eliminates repeated computations. The larger the terms, the more likely this is to be useful. It combines simplicity of bprove and duplicate avoidance via the add new/3 predicate. pprove(T):-ljp(T,[]),!. ljp(A,Vs):-memberchk(A,Vs),!. ljp((A->B),Vs1):-!,add_new(A,Vs1,Vs2),ljp(B,Vs2). ljp(G,Vs1):- % atomic(G), select((A->B),Vs1,Vs2), ljp_imp(A,B,Vs2), !, add_new(B,Vs2,Vs3), ljp(G,Vs3). ljp_imp(A,_,Vs):-atomic(A),!,memberchk(A,Vs). ljp_imp((C->D),B,Vs1):add_new((D->B),Vs1,Vs2), ljp((C->D),Vs2). add_new(X,Xs,Ys):-memberchk(X,Xs),!,Ys=Xs. add_new(X,Xs,[X|Xs]). 4.4 Implicational formulas as nested Horn Clauses Given the equivalence between: B1 ! B2 : : : Bn ! H and (in Prolog notation) H :B1; B2; : : : ; Bn, where we chose H is to be the atomic formula ending a chain of implications, we can recursively transform an implicational formula into one built form nested clauses, as follows. toHorn((A->B),(H:-Bs)):-!,toHorns((A->B),Bs,H). toHorn(H,H). toHorns((A->B),[HA|Bs],H):-!,toHorn(A,HA),toHorns(B,Bs,H). toHorns(H,[],H).
Note also that the transformation is reversible and that lists (instead of Prolog’s conjunction chains) are used to collect the elements of the body of a clause. ?- toHorn(((0->1->2)->(0->1)->0->2),R).
R = (2:-[(2:-[
R = (3:-[(4:-[
This suggests transforming provers for implicational formulas into equivalent provers working on nested Horn clauses. hprove(T0):-toHorn(T0,T),ljh(T,[]),!. ljh(A,Vs):-memberchk(A,Vs),!. ljh((B:-As),Vs1):-!,append(As,Vs1,Vs2),ljh(B,Vs2). ljh(G,Vs1):- % atomic(G), G not on Vs1 memberchk((G:-_),Vs1), % if non-tautology, we just fail select((B:-As),Vs1,Vs2), % outer select loop select(A,As,Bs), % inner select loop ljh_imp(A,B,Vs2), % A is in the body of B !,trimmed((B:-Bs),NewB), % trim empty bodies ljh(G,[NewB|Vs2]). ljh_imp(A,_B,Vs):-atomic(A),!,memberchk(A,Vs). ljh_imp((D:-Cs),B,Vs):- ljh((D:-Cs),[(B:-[D])|Vs]). trimmed((B:-[]),R):-!,R=B. trimmed(BBs,BBs).
Note that we have also added a second select/3 call to the third clause of ljh, to give ljh imp more chances to succeed and commit. Basically, the nested Horn clause form of implicational logic helps bypassing some intermediate steps, by focusing on the head of the Horn clause, which corresponds to the last atom in a chain of implications. This can also be used to speed up non-tautology rejection, by checking in the third clause of ljh that the goal G is actually the head of at least one of the clauses in the environment Vs1.
In fact, it might be worth formalizing and studying the properties of this nested Horn-clause prover directly, as a new calculus, given also its significant speed-up (as shown in section 6), relative to all the other provers. 4.5 A lifting to classical logic, via Glivenko’s transformation The simplest way to turn a propositional intuitionistic theorem prover into a classical one is to use Glivenko’s translation that prefixes a formula with its double negation. By adding the atom f alse, to the language of the formulas and a rewriting of the negation of x into x ! f alse, we obtain, after adding the special handling of false as the first line of ljk/2: :- op(425, fy, ~ ). % negation gprove(T0):-dneg(T0,T),kprove(T). kprove(T0):-expand_neg(T0,T),ljk(T,[]),!. ljk(_,Vs):-memberchk(false,Vs),!. ljk(A,Vs):-memberchk(A,Vs),!. ljk((A->B),Vs):-!,ljk(B,[A|Vs]). ljk(G,Vs1):select((A->B),Vs1,Vs2), ljk_imp(A,B,Vs2), !, ljk(G,[B|Vs2]). ljk_imp((C->D),B,Vs):-!,ljk((C->D),[(D->B)|Vs]). ljk_imp(A,_,Vs):-memberchk(A,Vs). expand_neg(A,R):-atomic(A),!,R=A. expand_neg(~A,R):-!,expand_neg(A,B),R=(B->false). expand_neg((A->B),(X->Y)):-expand_neg(A,X),expand_neg(B,Y).
Note that the predicate kprove/1 simply extends implicational propositional calculus, as implemented by bprove/1, with the negation operator ~/1, while the predicate gprove/1 prefixes a classical formula with double negation. 5
Correctness can be checked by identifying false positives or false negatives. A false positive is a non-tautology that the prover proves, breaking the soundness property. A false negative is a tautology that the prover fails to prove, breaking the completeness property.
While classical tautologies are easily tested (at small scale against truth tables, at medium scale with classical propositional provers and at larger scale with a SAT solver), intuitionistic provers require a more creative approach.
As a first bootstrapping step, assuming that no ”gold standard” prover is available one can look at the other side of the Curry-Howard isomorphism, and rely on generators for (typable) lambda terms and generators of formulas for implicational logic expressions, with results being checked against a trusted type inference algorithm.
As a next step, a trusted prover can be used as a gold standard to test both for false positives and negatives. 5.1
Finding false negatives by generating the set of simply typed normal forms of a given size A false negative is identified if our prover fails on a type expression known to have an inhabitant. Via the Curry-Howard isomorphism, such terms are the types inferred for lambda terms, generated by increasing sizes.
We refer to [
Finding false positives by generating all well-formed type expressions of a given size A false positive is identified if the prover succeeds finding an inhabitant for a type expression that does not have one.
We obtain type expressions by generating all binary trees of a given size, extracting
their leaf variables and then iterating over the set of their set partitions, while unifying
variables belonging to the same partition. We refer to [
The code describing the all-tree and set partition generation as well as their integration as a type expression generator is at: https://github.com/ptarau/TypesAndProofs/blob/master/allPartitions.pro.
We tested the predicate lprove/1 as well as all other provers derived from it for false negatives against simple types of terms up to size 15 (with size defined as 2 for applications, 1 for lambdas and 0 for variables) and for false positives against all type expressions up to size 7 (with size defined as the number of internal nodes). 5.3 Testing against a trusted reference implementation Assuming we trust an existing reference implementation (e.g., after it passes our generatorbased tests), it makes sense to use it as a ”gold standard”. In this case, we can identify both false positives and negatives directly, as follows: gold_test(N,Generator,Gold,Silver, Term, Res):call(Generator,N,Term), gold_test_one(Gold,Silver,Term, Res),
Res\=agreement. gold_test_one(Gold,Silver,T, Res):( call(Silver,T) -> \+ call(Gold,T),
Res = wrong_success ; call(Gold,T) -> % \+ Silver
Res = wrong_failure ; Res = agreement ).
When specializing to a generator for all well-formed implication expressions, and using Dyckhoff’s dprove/1 predicate as a gold standard, we have: gold_test(N, Silver, Culprit, Unexpected):gold_test(N, allImpFormulas, dprove, Silver, Culprit, Unexpected).
To test the tester, we design a prover that randomly succeeds or fails. badprove(_) :- 0 =:= random(2).
?- gold_test(6,lprove,T,R). false. % indicates that no false positive or negative is found ?- gold_test(6,badprove,T,R).
T = (0->1->0->0->0->0->0), R = wrong_failure ; ... ?- gold_test(6,badprove,T,wrong_success).
T = (0->1->0->0->0->0->2) ; T = (0->0->1->0->0->0->2) ; T = (0->1->1->0->0->0->2) ; ...
More complex implicit correctness tests can be designed, by comparing the behavior of a prover that handles false, with Glivenko’s double negation transformations that turns an intuitionistic propositional prover into a classical prover, working on classical formulas containing implication and negation operators.
After defining: gold_classical_test(N,Silver,Culprit,Unexpected):gold_test(N,allClassFormulas,tautology,Silver, Culprit,Unexpected).
We can run it against the provers gprove/1 and kprove/1, using Melvin Fitting’s
classical tautology prover [
Culprit = ((false->false)->0->0->((1->false)->false)->1), Error = wrong_failure ; Culprit = ((false->false)->0->1->((2->false)->false)->2), Error = wrong_failure . ...
While gprove/1, implementing Glivenko’s translation, passes the test, kprove/1 that handles intuitionistic tautologies (including negated formulas) will fail on classical tautologies that are not also intuitionistic tautologies. 6
Once passing correctness tests, our provers need to be tested against large random terms.
The mechanism is similar to the use of all-term generators.
6.1 Random simply-typed terms, with Boltzmann samplers
We generate random simply-typed normal forms, using a Boltzmann sampler along
the lines of that described in [
It works as follows: ?- ranTNF(10,XT,TypeSize).
XT = l(l(a(a(s(0), l(s(0))), 0))) : (((A->B)->B->C)->B->C).
TypeSize = 5. ?- ranTNF(60,XT,TypeSize),nv(XT).
XT = l(l(a(a(0, l(a(a(0, a(0, l(...))), s(s(0))))),
l(l(a(a(0, a(l(...), a(..., ...))), l(0))))))) : (A->((((A->A)- ...)->D)->D)->M)->M), TypeSize = 34.
Interestingly, partly due to the fact that there’s some variation in the size of the terms
Boltzmann sampler generate and more to the fact that the distribution of types favors
(as seen in the second example) the simple tautologies where an atom identical to the
last one is contained in the implication chain leading to it [
Our code combines an implementation of Re´my’s algorithm [
We refer to [
As automatic Boltzmann sampler generation is limited to fixed numbers of
equivalence classes from which a CF- grammar can be given, we build our the random set
partition generator that groups logical variables in leaf position into equivalence classes
by using an urn-algorithm described in [
Once a random binary tree of size N is generated with the ->/2 constructor labeling internal nodes, the N + 1 leaves of the tree are decorated with logic variables. As variables sharing a name define equivalence classes on the set of variables, each choice of them corresponds to a set partition of the N + 1 nodes.
The combined generator, that generates in a few seconds terms of size 1000, works as follows: ?- ranImpFormula(20,F).
F = (((0->(((1->2)->1->2->2)->3)->2)->4->(3->3)->
(5->2)->6->3)->7->(4->5)->(4->8)->8) . ?- time(ranImpFormula(1000,_)). % includes tabling large Stirling numbers % 37,245,709 inferences,7.501 CPU in 7.975 seconds (94% CPU, 4965628 Lips) ?- time(ranImpFormula(1000,_)). % much faster now, thanks to tabling % 107,163 inferences,0.040 CPU in 0.044 seconds (92% CPU, 2659329 Lips) Note that we use Prolog’s tabling (a form of automated dynamic programming) to avoid costly recomputation of the (very large) Sterling numbers.
Testing for false positives and false negatives for random terms proceeds in a similar manner to exhaustive testing with terms of a given size.
Assuming Roy Dyckhoff’s prover as a gold standard, we can find out that our nested Horn Clause prover hprove/1 can handle 100 terms of size 50 as well as the gold standard. ?- gold_ran_imp_test(50,100,hprove, Culprit, Unexpected). false. % indicates no differences with the gold standard
In fact, the size of the random terms handled by hprove/1 makes using provers an appealing alternative to random lambda term generators in search for very large lambda term simple type pairs. Interestingly, on the side of random simply typed terms, limitations come from their vanishing density, while on the other side they come from the known PSPACE-complete complexity of the proof procedures. 6.4
Can lean provers actually be fast? A quick performance evaluation
https://github.com/ptarau/TypesAndProofs/blob/master/benchmarks.pro.
The following table compares several provers on exhaustive ”all-terms” benchmarks, derived from our correctness test. First, we run them on the types inferred on all lambda terms of a given size. Next we run them on all implicational formulas of a given size (set to be about half of the former, as the number of these grows much faster).
Note that the size of the implicational formulas in the case of the ”Mix of examples” is half of the size of the lambda terms whose type are used in the case of ”Positive examples”
The nested Horn clauses based hprove/1 turns out to be a clear winner. Most likely, this comes from concentrating its non-deterministic choices in the two select/3 calls. These calls happen in constant space and replace with a faster ”shallow backtracking” loop, the ”deep backtracking” the other provers might need to cover the same search space.
In fact, hprove/1 seems to also scale well on larger formulas, following closely the increase in the numbers of test formulas. Note that ”pos” marks formulas known to be tautologies, generated by typable lambda terms of sizes 16,17 and 18 and ”mix” marks implicational formulas of sizes 8, 8 and 9. ??- forall(between(16,18,N),bm(N,hprove)). [prog=hprove,size=16,pos=90.257,mix=30.411,total=120.668] [prog=hprove,size=17,pos=425.586,mix=32.214,total=457.8] [prog=hprove,size=18,pos=2108.01,mix=657.807,total=2765.818]
Testing exhaustively on small formulas, while an accurate indicator for average speed, might not favor provers using more complex heuristics or extensive preprocessing. But if that happens, one would expect it to result in a constant factor ratio, rather than a fast increasing gap as it happens, for instance between Dyckhoff’s original dprove and our best prover hprove. 7
The related work derived from Gentzen’s LJ calculus is in the hundreds if not in the thousands of papers and books. Space constraints limit our discussion to the most closely related papers, directly focusing on algorithms for implicational intuitionistic propositional logic.
Among them the closest are [
Similar calculi, key ideas of which made it into the Coq proof assistant’s code, are
described in [
On the other side of the Curry-Howard isomorphism [
Using hypothetical implications in Prolog, although all with a different semantics
than Gentzen’s LJ calculus or its LJT variant, go back as early as [
Overviews of closely related calculi, using the implicational subset of propositional
intuitionistic logic are [
Our empirically oriented approach has found variants of lean propositional intuitionistic provers that are comparable to their more complex peers, derived from similar calculi. Among them, the nested Horn clause prover might be worth formalizing as a calculus and subject to deeper theoretical analysis. Given that it shares its main data structures with Prolog, it seems interesting to optimize it via partial evaluation or compilation to Prolog.
Our renewed interest in finding lightweight implementations of these classic theoretically hard (PSPACE-complete) combinatorial search problems, is also motivated by the possibility of parallel implementations using multi-core and GPU algorithms.
We plan future work in formalizing the nested Horn-clause prover in sequent-calculus and explore compilation techniques and parallel algorithms for it.
A generalization to nested Horn clauses with universally quantified variables seems also promising to explore, with either grounding techniques as used by SAT and ASPm solvers or via compilation to Prolog.
This research has been supported by NSF grant 1423324.