Home

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:

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.

By Ehud Lamm at 2006-02-05 09:09 | Fun | Lambda Calculus | Type Theory | other blogs | 9913 reads

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.

By David Fisher at Sun, 2006-02-05 16:54 | login or register to post comments

Right

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

By Ehud Lamm at Sun, 2006-02-05 17:34 | login or register to post comments

Actually...

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

By David Fisher at Sun, 2006-02-05 18:07 | login or register to post comments

Or, just use Coq

This:

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).
firstorder.
Qed.

Extraction shift.

yields

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

By Nick Benton at Sun, 2006-02-05 19:58 | login or register to post comments