I'd like to point out a different take on Djinn:
http://cvs.sourceforge.net/viewcvs.py/kanren/kanren/mini/type-inference.scm
http://cvs.sourceforge.net/viewcvs.py/kanren/kanren/mini/logic.scm
The first defines the Hindley-Milner typechecking relation for a
language with polymorphic let, sums and products. We use the Scheme
notation for the source language (as explained at the beginning of the
first file); ML or Haskell-like notations are straightforward. The
notation for type terms is infix, with the right-associative arrow.
The typechecking relation relates a term and its type: given a term we
obtain its type. The relation is pure and so it can work in reverse: given a type, we can obtain terms that have this type. Or, we can give a term with blanks and a type with blanks, and ask the relation to fill in the blanks.
As an example, the end of the file type-inference.scm shows the derivation for the terms call/cc, shift and reset from their types in the continuation monad. Given the type
(((a -> . ,(cont 'b 'r)) -> . ,(cont 'b 'b)) -> . ,(cont 'a 'b))
we get the expression for shift:
(lambda (_.0) (lambda (_.1)
((_.0 (lambda (_.2) (lambda (_.3) (_.3 (_.1 _.2)))))
(lambda (_.4) _.4))))
It took only 2 milli-seconds.
More interesting is using the typechecker for proving theorems in
intuitionistic logic: see logic.scm. We formulate the proposition in types, for example:
(,(neg '(a * b)) -> . ,(neg (neg `(,(neg 'a) + ,(neg 'b)))))
This is one direction of the deMorgan law. In intuitionistic logic,
deMorgan law is more involved:
NOT (A & B) == NOTNOT (NOT A | NOT B)
The system gives us the corresponding term, the proof:
(lambda (_.0)
(lambda (_.1)
(_.1 (inl (lambda (_.2)
(_.1 (inr (lambda (_.3) (_.0 (cons _.2 _.3))))))))))
The de-typechecker can also prove theorems in classical logic,
via double-negation (aka CPS) translation. The second part of
logic.scm demonstrates that. We can formulate a proposition:
(neg (neg `(,(neg 'a) + ,(neg (neg 'a)))))
and get a (non-trivial) term
(lambda (_.0) (_.0 (inr (lambda (_.1) (_.0 (inl _.1))))))
It took only 403 ms. The proposition is the statement of the Law of
Excluded Middle, in the double-negative translation.
So, programming languages can help in the study of logic.
Recent comments
17 weeks 14 hours ago
17 weeks 14 hours ago
17 weeks 14 hours ago
23 weeks 1 day ago
1 year 11 weeks ago
1 year 11 weeks ago
1 year 11 weeks ago
1 year 33 weeks ago
1 year 37 weeks ago
1 year 39 weeks ago