Theses
https://www.cs.dartmouth.edu/~sws/abstracts/lambda.shtml
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.
Abstract
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.
