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: 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].


Kristoffer H. Rose

Department of Computer Science
University of Aarhus
Ny Munkegade, building 540
DK - 8000 Århus C
Home page:

Back to the list of talks