Inverse typechecker and theorem proving in intuitionistic and classical logics

Another cool demonstration from Oleg:

I'd like to point out a different take on Djinn:

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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Oleg here uses Mini-Kanren,

Oleg here uses Mini-Kanren, the LP system for Scheme that accompanies The Reasoned Schemer. This book and system are worth checking out; besides being extremely educational, I'm finding the system easy and useful. Plus, since it's so simple and small (+/- 100 lines!), it's a snap to tinker with the interior.

I built a type inference example similar to the one Oleg presents up there (but not as good) in half a day, as a proof of concept.

Plus, one final thing: Scheme is the ideal language to do type inference, because there are none of those stupid types to get in the way.


I should have mentioned that this is based on Kanren. TRS was discussed here at length.


Actually, I just wanted to get in on the Reasoned Schemer love-fest, since I missed it the first time 'round.

Or, just use Coq


Definition cont (a r : Set) := (a->r)->r.

Lemma shift : forall (a b r : Set),
((a -> (cont b r))->(cont b b)) -> (cont a b).

Extraction shift.


let shift h h0 =
h (fun h1 h2 -> h2 (h0 h1)) (fun h1 -> h1)