Theses     Last modified: 05/02/05 07:47:18 AM

S.W. Smith
The Apparent Link Between Typability and Computational Complexity in Lambda-Calculus
Department of Mathematics, Princeton University.
May 1987.

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.

Back to home page Maintained by Sean Smith,