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

MIT TOC Seminar--Harry Mairson--Wed Nov 1



Date: Mon, 30 Oct 89 09:44:46 EST
To: theory-seminars@theory.LCS.MIT.EDU

                Massachusetts Institute of Technology
                    Theory of Computation Seminar

                  DATE: Wednesday, November 1, 1989
                         REFRESHMENTS: 3:15pm
                             TALK: 3:30pm
                      PLACE: NE43 8th Floor Playroom

                  Deciding ML Typability is Complete
                  for Deterministic Exponential Time

                           Harry G. Mairson
                    Department of Computer Science
                         Brandeis University
                        Waltham, Massachusetts

The functional programming folklore that ML-style expressions can be
typed efficiently is not true.  Some simple ML programs can be
exhibited whose smallest types are enormous -- of exponential size in
the size of the expression.  Indeed, Kanellakis and Mitchell recently
showed that deciding ML expression typability is PSPACE-hard.

We improve the latter result, showing that deciding ML typability is
DEXPTIME-complete.  The proof consists of a straightforward
"simulation" of any deterministic one-tape Turing machine M with input
x running in O(c^{|x|}) time by a polynomial-sized ML formula
Phi_{M,x} such that M accepts x iff Phi_{M,x} is typable.  The key
insight is how ML polymorphism can be used to succinctly express
function composition.  We conjecture this insight will yield stronger
lower bounds for various extensions to the ML typing system.

This talk should be understandable to anyone who understands the
mechanics of ML let-polymorphism and knows what a Turing Machine is.
We hope it will interest both theorists, functional programming
enthusiasts, and those interested in practical type checking.

HOST: Prof. Albert Meyer