Computational Models Based on Explicit Substitution with an Address Oracle Using Parallel Reduction

Kristoffer H. Rose
University of Aarhus

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 M^a, 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 := N^a>        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)

          M^a 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.

Kristoffer H. Rose

BRICS
Department of Computer Science
University of Aarhus
Ny Munkegade, building 540
DK - 8000 Århus C
Denmark
Email: krisrose@brics.dk
Home page: http://www.brics.dk/~krisrose/

Back to the list of talks

Computational Models Based on Explicit Substitution with an Address Oracle Using Parallel Reduction

Kristoffer H. Rose University of Aarhus

References

Kristoffer H. Rose

Kristoffer H. Rose
University of Aarhus