; Classical and Intuitionistic logic with Kanren
;
; This file illustrates the use of the typechecking relation (file
; ./type-inference.scm) for proving theorems in Intuitionistic and
; Classical logics.
;
; The type-checking relation, in the term-reconstruction mode,
; reconstructs a term (i.e., a proof) for a type (i.e., a proposition).
; The proposition may contain eigenvariables (for universally-quantified
; variables) and logical variables (for existentially quantified variables),
; and so the de-typechecker is a theorem prover for the fragment of
; intuitionistic predicate logic where all terms are in prenex form.
; $Id: logic.scm,v 1.2 2006/01/26 22:32:13 oleg Exp $
(load "type-inference.scm")
; Definitions:
;
; Atomic formula (proposition) P is represented by a term of some type P
; (P & Q) is represented by a term of a type (P * Q)
; (P | Q) (P + Q)
; NOT P P -> F
;
; where F is some distinguished type (which can be abstract for what we
; care).
; we will be using sums, products, and applications. We will be interested
; in the terms in the normal form
; We restrict the app-rel to avoid the redexes. We don't want to generate
; terms with redexes anyway...
; The above prevents call-by-name redexes. We may wish to exclude only CBV
; redexes (lambdas and variables in the operand position). It is interesting
; how it changes the result...
(define appn-rel
(lambda (s!-)
(let ((!- (s!- s!-)))
(lambda (e t)
(fresh (t-rand rand rator)
(== e `(app ,rator ,rand))
(fresh (_) (conde ((== rator `(var ,_)))
((== rator `(car (var ,_))))
((== rator `(cdr (var ,_))))
(else (== rator `(app . ,_)))))
(!- rator `(,t-rand -> . ,t))
(!- rand t-rand))))))
(define c!-
(make-! lambda-rel appn-rel ; implications, (P ->. Q)
cons-rel car-rel cdr-rel ; products, type (P * Q)
inl-rel inr-rel either-rel ; sums, type (P + Q)
))
(define F 'F) ; The falsity type
;------------------------------------------------------------------------
; Intuitionistic logic
(test-check "law-of-contradiction"
(time
(map unparse
(run 1 (q) (c!- q `(((b -> . F) * b) -> . F)))))
'((lambda (_.0) ((car _.0) (cdr _.0))))
)
; The result shows that there is a term of the type (((b -> . F) * b) -> . F)
; namely
; ((lambda (_.0) ((car _.0) (cdr _.0))))
; That term is a proof that the law of contradiction (NOT P & P) -> F
; holds in intuitionistic logic.
(test-check "law-of-conj"
(time
(map unparse
(run 1 (q) (c!- q `((a * b) -> . a)))))
'((lambda (_.0) (car _.0)))
)
; The result proves (A & B) -> A
(test-check "law-of-disj"
(time
(map unparse
(run 1 (q) (c!- q `((a + a) -> . a)))))
'((lambda (_.0) (either (_.1 _.0) _.1 _.1)))
)
; The result proves (A | A) -> A
(test-check "conseq-of-F"
(time
(map unparse
(run 1 (q) (c!- q `(F -> . (a -> . F))))))
'((lambda (_.0) (lambda (_.1) _.0)))
)
; The result shows that F -> (NOT A) for any A.
; That is, there exists a term, namely, \x -> \k -> x of the type
; F -> (A->F). Which means that falsity entails the negation of any
; formula. Falsity does not entail everything, in intuitionistic logic.
; Another useful law:
(test-check "conseq-of-triple-not"
(time
(map unparse
(run 1 (q) (c!- q '((((a -> . F) -> . F) -> . F) -> a -> . F)))))
'((lambda (_.0) (lambda (_.1) (_.0 (lambda (_.2) (_.2 _.1))))))
)
; which is the proof of
; NOT NOT NOT A --> NOT A
; Obviously, NOT NOT A does not entail A in intuitionistic logic. But
; the converse does hold:
(test-check "impl-for-double-not"
(time
(map unparse
(run 1 (q) (c!- q '(a -> . ((a -> . F) -> . F))))))
'((lambda (_.0) (lambda (_.1) (_.1 _.0))))
)
; So A -> NOT NOT A.
; De Morgan laws turn out to be more interesting in intuitionistic
; logic: Although
; NOT (A | B) -> (NOT A & NOT B)
; as before
; proof:
(test-check "DeMorgan-disj"
(time
(map unparse
(run 1 (q) (c!- q '(((a + b) -> . F) -> .
((a -> . F) * (b -> . F)))))))
'((lambda (_.0)
(cons (lambda (_.1) (_.0 (inl _.1))) (lambda (_.2) (_.0 (inr _.2))))))
)
(test-check "DeMorgan-disj-inv"
(time
(map unparse
(run 1 (q) (c!- q '(((a -> . F) * (b -> . F)) -> .
((a + b) -> . F)
)))))
'((lambda (_.0)
(lambda (_.1)
(either (_.2 _.1) ((car _.0) _.2) ((cdr _.0) _.2)))))
)
; It does not intuitionistically follow that
; NOT (A & B) -> (NOT A | NOT B)
; Rather, we should have
; NOT (A & B) -> NOTNOT (NOT A | NOT B)
; Proof:
(cout nl "DeMorgan-conj will take some 6 secs" nl)
(define (neg x) `(,x -> . F))
(test-check "DeMorgan-conj"
(time
(map unparse
(run 1 (q) (c!- q `(,(neg '(a * b)) -> .
,(neg (neg `(,(neg 'a) + ,(neg 'b)))))))))
'((lambda (_.0)
(lambda (_.1)
(_.1 (inl (lambda (_.2)
(_.1 (inr (lambda (_.3) (_.0 (cons _.2 _.3)))))))))))
)
; Here's is the proof of the inverse implication
(test-check "DeMorgan-conj-inv"
(time
(map unparse
(run 1 (q) (c!- q `(,(neg (neg `(,(neg 'a) + ,(neg 'b))))
-> . ,(neg '(a * b)))))))
'((lambda (_.0)
(lambda (_.1)
(_.0 (lambda (_.2)
(either (_.3 _.2) (_.3 (car _.1)) (_.3 (cdr _.1))))))))
)
; So, intuitionistically,
; NOTNOT (A | B) = NOT( NOT A & NOT B) = NOTNOT (NOTNOT A | NOTNOT B)
;------------------------------------------------------------------------
; Classical logic
;
; Although lambda-calculus corresponds to intuitionistic logic,
; we can handle classical logic as well, via a double-negation translation:
;
; TR(P) ==> NOT NOT P, or (p->F)->F, P is atomic
; TR(NOT P) ==> NOT P, or p->F, if P is atomic
; TR(NOT A) ==> NOT TR(A) ; for a general formula A
; TR(A & B) ==> NOTNOT( TR(A) & TR(B) )
; TR(A | B) ==> NOTNOT( TR(A) | TR(B) )
; TR(A ->B) ==> NOTNOT( A -> TR(B) )
; Now, regarding the law
; TR(NOT P) = NOT P, P atomic
; In general, that should be
; TR(NOT A) = NOT (TR A)
; So, for atomic A we get TR(NOT A) = NOT NOT NOT A, but the triple
; negative entails the single one (see above).
;
; The translation has the property that A -> TR(A) is provable
; in intuitionistic logic. We have already seen the validity of
; all the cases above but the last one, for the implication.
; For the latter, we ask Kanren to
; derive us the term with the type (A->B) -> NOTNOT (A -> NOTNOT B)
(test-check "tr-impl, or CPS of functions"
(time
(map unparse
(run 1 (q) (c!- q `((a -> . b) -> .
,(neg (neg `(a -> . ,(neg (neg 'b))))))))))
'((lambda (_.0)
(lambda (_.1)
(_.1 (lambda (_.2) (lambda (_.3) (_.3 (_.0 _.2))))))))
)
; The result is a CPS translation for functions, btw. So, Kanren
; was able to derive the CPS transform...
; The result A -> TR(A) can be regarded, from the perspective of the
; modal logic, as the law of necessitation, or as a CPS transform, or,
; from the perspective of the translation, that a theorem of
; intuitionistic logic entails the theorem in the translation.
; Chung-chieh Shan has pointed out that the above translation
; is, in fact, the NOTNOT translation of Glivenko and
; Kolmogorov. Thus, CPS does prove one direction of
;
; Glivenko's Theorem: An arbitrary propositional formula A is
; classically provable, if and only if NOTNOTA is intuitionistically
; provable.
; The translation TR is CPS (it's easy to see that's how it was
; derived. The logical justification (as well as terms-as-proof) came
; later, for me. Historically, it was the other way around). Of course,
; the translation from CPS back into the direct style (and introducing
; call/cc where the direct translation demands it) will let us encode
; classical theorems ``directly''.
; We shall see that the translation gives us classical logic indeed. First,
; we attempt to derive a term of the type
; ((F->F)->F) -> ((A->F)->F)
(test-check "from-F-all-follows"
(time
(map unparse
(run 1 (q) (c!- q `(,(neg (neg 'F)) -> . ,(neg (neg 'a)))))))
'((lambda (_.0) (lambda (_.1) (_.0 (lambda (_.2) _.2)))))
)
; That is, from TR(F) follows TR(A) for any formula A whatsoever. We get
; the classical result that falsity entails everything.
; The most interesting is the following term:
(test-check "LEM"
(time
(map unparse
(run 1 (q) (c!- q (neg (neg `(,(neg 'a) + ,(neg (neg 'a)))))))))
'((lambda (_.0) (_.0 (inr (lambda (_.1) (_.0 (inl _.1)))))))
)
; which proves TR( NOT A | A ). That is, we get the Law of Excluded Middle.
; A simpler proof: rather than pushing all NOTs down, we can just
; use the double-negated classical formula as it is, without futher
; transformations. Glivenko theorem applies to arbitrary propositional
; formulas.
; Thanks to Eijiro Sumii for pointing this out.
(test-check "LEM simpler"
(time
(map unparse
(run 1 (q) (c!- q (neg (neg `(a + ,(neg 'a))))))))
'((lambda (_.0) (_.0 (inr (lambda (_.1) (_.0 (inl _.1)))))))
)