tail recursion (was Re: a (revised) draft of R5RS)

[William D Clinger <will@ccs.neu.edu>]

John Ramsdell wrote:
> Following their model, a language designer can make precise the
> requirement that an implementation of a programming language behave as
> if it uses tail-call elimination by requiring that, asymptotically,
> implementations use no more space then a memory aware abstract machine
> which uses tail-call elimination.  Let me call implementations that
> meet this requirement tail-call aware implementations.

This is the same as saying that

>     An implementation of Scheme is properly tail recursive
>     if and only if for every Scheme program P and inputs D,
>     the space required to execute P on D is O(N), where N
>     is the space required by implementation X,

where X is a memory aware abstract machine that uses tail-call
elimination.  Not only can this definition be made precise, it
can be formalized, as I sketch below.

If the Scheme authors feel there is actually a need for this
level of precision or formalism, then I volunteer to write a
tutorial on this.

Will

----

A suitable implementation X is sketched below.  I omitted a few
things and surely added a few bugs, since I just now dashed it
out, but the basic ideas are sound.

There are some technical difficulties caused by nondeterminism
and garbage collection.

Definition.  An implementation of Scheme is safe-for-space
(in the sense of a naive interpreter) if and only if for
every Scheme program P and inputs D, the space required to
execute P on D is O(N), where N is the maximum space required
by the abstract machine described below for the closed program
formed from P and D, taken over all execution sequences that
have the following two properties:

  1. Assignments evaluate to value(#F).  [This restriction
     does not affect portable programs.  Allowing arbitrary
     values for assignments, as allowed by the semantics below,
     can create space leaks.]

  2. A GC rule is applied as soon as it becomes applicable.
     [This has the effect of requiring garbage collection
     without specifying how often the gc must run, thanks
     to the asymptotic bound.]

Definition.  An implementation of Scheme is properly tail
recursive if it is safe for space as defined above.

Alternative definition.  An implementation of Scheme is properly
tail recursive if and only if the space required for continuations
is O(M), where M is the space required for continuations by the
abstract machine.  [This begs the question of which space should be
charged against continuations in real implementations, so I don't
think this definition is as useful as the previous definition.]

The space required by an execution sequence is the maximum space
required by any configuration in the sequence.  The space required
by a configuration is the sum of the space required by its four
components.  The space required by an expression is zero; the space
required by any other component is the number of nodes in its
abstract syntax tree.  It doesn't matter exactly how we define
the abstract syntax trees, because we are interested only in an
asymptotic bound.

Syntax of Core Scheme

  E  -->  K  |  I  |  L
       |  (if E0 E1 E2)
       |  (set! I E)
       |  (E0 E1 ... En)
  L  -->  (lambda (I1 ... In) E)

Small-step semantics for Core Scheme

A configuration consists of
  an expression or value
  an environment (a finite function from identifiers to locations)
  a continuation (see below)
  a store (a finite function from locations to values)

A continuation is given by the following syntax:

  k  -->  halt  |  branchf(E1,E2) :: k  |  store(loc) :: k
       |  evlis(permutation,<v1, ...>,<E1, ...>) :: k
       |  applyto(<v1, ...>) :: k

The initial continuation is "halt".  The initial environment
and store implement the standard Scheme library in a reasonable
way, which I won't define other than to remark that the space
required by the library doesn't matter because of the asymptotic
bound; all that matters is that calling the library procedures
does not cause them to allocate and to retain asymptotically
more space than would a reasonable implementation.

The following help functions and notions are left as exercises
for the reader: value, hold, contents, "fresh for".

Rules

  < K, r, k, s >  ->  < value(K), r, k, s >

  < I, r, k, s >  ->  < contents(hold r I), r, k, s >

  < L, r, k, s >  ->  < closure(L, r), r, k, s >

  < (if E0 E1 E2), r, k, s >  ->  < E0, r, (branchf(E1,E2) :: k), s >

  < (set! I E), r, k, s >  ->  ( E, r, (store(hold r I) :: k), s >

The following rule is actually a rule scheme: for every natural
number n, there is one rule for every permutation pi of 0..n.
Let pi(E0 E1 ... En) stand for the permutation pi applied to
(E0 E1 ... En) instead of 0..n, and let pi(E0 E1 ... En)[i]
stand for the i-th element of that sequence (0-origin).

  < (E0 E1 ... En), r, k, s >  ->
  < pi(E0 E1 ... En)[0],
    r,
    (evlis(pi^{-1},
           <>,
           < pi(E0 E1 ... En)[1], ..., pi(E0 E1 ... En)[n] >)
     :: k),
    s >

The following rules describe the action of various kinds of
continuation upon a value v.  Some of them are rule schema.

  < v, r, halt, s >  ->  v

  < v, r, (branchf(E1,E2) :: k), s >  ->  < E1, r, k, s >
      provided v is not value(#F).

  < value(#F), r, (branchf(E1,E2) :: k), s >  ->  < E2, r, k, s >

  < v, r, (store(loc) :: k), s >  ->  < v', r, k, s[loc:=v] >
      where v' is any value.

  < v, r, (evlis(pi^{-1}, < v0, ... >, < Ei, Ei+1, ... >) :: k), s >
  ->
  < Ei, r, (evlis(pi^{-1}, < v0, ..., v >, < Ei+1, ... >) :: k), s >

  < vn, r, (evlis(pi^{-1}, < v0, ..., vn-1 >, <>) :: k), s >
  ->
  < pi^{-1}(<v0, ..., vn-1, vn>)[0],
    r,
    (applyto(< pi^{-1}(<v0, ..., vn-1, vn>)[1],
               pi^{-1}(<v0, ..., vn-1, vn>)[2],
               ...,
               pi^{-1}(<v0, ..., vn-1, vn>)[n] >)
     :: k),
    s >

  < closure((lambda (I1 ... In) E), r),
    r',
    (applyto(< v1, ..., vn >) :: k),
    s >
  ->
  < E, r[I1:=loc1]...[In:=locn], k, s[loc1:=v1]...[locn:=vn] >
      where loc1, ..., locn are fresh for r, r', v1, ..., vn, k, s.

We'll need a few primops to implement the standard library:

  < primop(f), r, applyto(< v1, ..., vn >) :: k), s >
  ->
  < f(v1, ..., vn), r, k, s >

Finally, we have two GC rule schema:

If loc1, ..., locn are fresh for v, r, k, and s, then

  < E, r, k, s[loc1:=v1]...[locn:=vn] >  ->  < E, r, k, s >

  < v, r, k, s[loc1:=v1]...[locn:=vn] >  ->  < v, r, k, s >

End of small-step semantics.