Last modified: 05/02/05 07:47:18 AM
The Apparent Link Between Typability and Computational Complexity
Department of Mathematics, Princeton University.
Senior thesis. Advisor: Andrew Appel.
The untyped lambda-calculus is a formal system, equivalent in power to the
Turing machine, for representing functions. The typed lambda-calculus is
a restricted subsystem with the added property that all computations will
terminate. However, the typed system apparently features a major drawback
in that the complexity of a computation in the typed calculus seems higher
than the complexity of the corresponding computation in the untyped calculus.
Simple operations on natural representations of the natural numbers
and lists readily manifest this difference---constant time versus linear.
This paper explores this complexity difference and develops typable lists
which approach logarithmic time, rather than linear, as well as typable
logarithmic numerals. This paper also presents the foundations for a possible
proof that no typable lists can take constant time.