We discussed how one can refine Church's lambda-calculus such that faithful
time and complexity measures can be extracted for algorithms executed this
way. The technique is to combine three things:
explicit substitution as originally discussed by Abadi,
Cardelli, Curien, and Levy [1991].
explicit addressing invented by many authors, among
them Felleisen and Friedman [1989].
The parallel reduction rewriting notion of Levy [1980].
Concretely, we proposed the following system, which we call \xa (here `\'
means `lambda' and `#' means `not equal' or `not in set'.)
The terms are \-terms with explicit substitution and addresses:
M,N,P ::= x | \x.M | MN | M | M^a
This set is restricted to those where for every Ma, a can be
interpreted as the memory address holding M (thus for each particular a all
the Ms must be identical).
Reduction is the usual lambda-reduction with explicit substitution, augmented
with addresses as follows (`fresh' means `globally fresh'):
(\x.M)N -> M<x := Na> a fresh (ba)
x<x:=P> -> N (xv)
y<x:=P> -> x x # y (xvgc)
(\y.M)<x:=P> -> \y.(M<x:=P>) (xab)
(MN)<x:=P> -> M<x:=P> N<x:=P> (xap)
Ma N -> MN (cpap)
M^a <x:=P> -> M<x:=P> (cpx)
This system has two crucial properties: each rule can be realised locally
except (ba) which needs an address oracle. We claim that this can be
coded
in constant time then all rules can be executed in constant time, hence the
reduction length is a faithful time complexity model.
Similarly, a notion of graph size is easily definable such that |M|
is the amount of memory occupied by the run-time representation of M.
This calculus is studied by Rose [1996]; a version restricted to weak
reduction (as used by all functional languages, for example), which makes the
use of de Bruijn indices (encoding environments on a stack) is described by
Benaissa, Lescanne, and Rose [1996].
References
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Levy:
Explicit Substitutions. J. Funct. Progr. 1(4):375-416, 1991.
Z.-E.-A. Benaissa, P. Lescanne, and K. H. Rose: Modeling sharing and
recursion for weak reduction strategies using explicit substitution.
PLILP-96, Aachen, Germany, Sept. 1996.
M. Felleisen and D. P. Friedman: A Syntactic Theory of Sequential State.
Theor. Comp. Science 69:243-287, 1989.
J.-J. Levy: Optimal Reductions in the Lambda Calculus.
In J. P. Seldin and J. R. Hindley (editors):
To H. B. Curry, Essays in Combinatory Logic, Lambda
Calculus, and Formalism, pp.159-191. Academic Press, 1980.
K. H. Rose: Operational Reduction Models for Functional Programming
Languages. Ph.D. thesis. DIKU (report 96/1),
University of Copenhagen, March 1996.