[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