[Prev][Next][Index][Thread]

computer proves a "types" theorem

Date: Wed, 30 Oct 91 14:47:04 -0500

Type inference for the simply-typed lambda calculus 
is complete for PTIME:   Proof by computer program
-----------------------------------------------------

Motivated by Jerzy Tiuryn's survey paper on type inference, John
Mitchell recently posted a "one liner" proof, without details
concerning first order unification, that type inference for the simply
typed lambda calculus is complete for PTIME.

This note shows how the result can also be proved "by computer
program," giving some explicit detail of the unification process: the ML
type inference algorithm (without use of "let") can be used to compute
the output of circuits.  (Recall that this problem, the Circuit Value
Problem, is PTIME-complete.)

The programs we write to evaluate circuits are not perverse: they are
completely natural, straightforward, and built out of the standard
Church codings.  Here they are:
  - fun True x y=x;
  val True = fn : 'a -> 'b -> 'a
  - fun False x y=y;
  val False = fn : 'a -> 'b -> 'b
  - fun And p q= p q False;
  val And = fn : ('a -> ('b -> 'c -> 'c) -> 'd) -> 'a -> 'd
  - fun Or p q= p True q;
  val Or = fn : (('a -> 'b -> 'a) -> 'c -> 'd) -> 'c -> 'd
  - fun Pair x y= fn z=> z x y;
  val Pair = fn : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c

Now one wrinkle: a logical "fanout" gate: it duplicates a Boolean
value (stored in "pairs"): the two copies of the variable do not share
type variables:
  - fun Fanout p= p (Pair True True) (Pair False False);
  val Fanout = fn : (((('a -> 'b -> 'a) -> ('c -> 'd -> 'c) -> 'e) ->
  'e) -> ((('f -> 'g -> 'g) -> ('h -> 'i -> 'i) -> 'j) -> 'j) -> 'k) -> 'k
  - Fanout True;
  val it = fn : (('a -> 'b -> 'a) -> ('c -> 'd -> 'c) -> 'e) -> 'e
  - Fanout False;
  val it = fn : (('a -> 'b -> 'b) -> ('c -> 'd -> 'd) -> 'e) -> 'e
  
As an example, we choose a circuit from Dwork, Kanellakis, and
Mitchell (``On the Sequential Nature of Unification,'' J. Logic
Programming, 1985, p. 43), represented in straight-line code as:

input e1 e2 e3 e4 e5 e6;
e7= And e2 e3; e8= And e4 e5; e9=e10= And e7 e8;
e11= Or e1 e11; e12= Or e10 e6;
output (Or e11 e12);

which we realize as:

  - fun circuit e1 e2 e3 e4 e5 e6=
  (fn e7=>
    (fn e8=>
      (Fanout (And e7 e8))
        (fn e9=> fn e10=>
          (fn e11=>
            (fn e12=> Or e11 e12)
            (Or e10 e6))
          (Or e1 e9)))
    (And e4 e5))
  (And e2 e3);
  val circuit = fn : (('a -> 'b -> 'a) -> 'c -> ('d -> 'e -> 'd) -> 'f
  -> 'g) -> ('h -> ('i -> 'j -> 'j) -> 'k -> ('l -> 'm -> 'm) -> ((('n
  -> 'o -> 'n) -> ('p -> 'q -> 'p) -> 'r) -> 'r) -> ((('s -> 't -> 't)
  -> ('u -> 'v -> 'v) -> 'w) -> 'w) -> ('c -> (('x -> 'y -> 'x) -> 'z ->
  'f) -> 'g) -> 'ba) -> 'h -> ('bb -> ('bc -> 'bd -> 'bd) -> 'k) -> 'bb
  -> 'z -> 'ba

The use of ``let'' is incidental: we could have used the code for the
logic gates instead of their names.

We can now plug inputs into the circuit, and the type inference
mechanism is forced to ``evaluate'' the circuit, ``solving'' the
Circuit Value Problem:

  - circuit False True True True True False;
  val it = fn : 'a -> 'b -> 'a

(The output is ``True'' -- True is the only normal form with the given
type!) A curious consequence of this example is that the clever
unification gadgets of Dwork, Kanellakis, and Mitchell are not unique:
typed versions of standard combinators work fine, and are perfectly
suited for discussion of type inference as well as unification.

Harry Mairson