[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: "John D. Ramsdell" <ramsdell@linus.mitre.org>*Subject*: tail recursion (was Re: a (revised) draft of R5RS)*From*: William D Clinger <will@ccs.neu.edu>*Date*: Mon, 26 May 1997 18:38:17 -0500*Cc*: rrrs-authors@martigny.ai.mit.edu, will@ccs.neu.edu*Organization*: Northeastern University*References*: <ogt9113jk73.fsf@linus.mitre.org>*Reply-To*: 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.

**Follow-Ups**:**Re: tail recursion (was Re: a (revised) draft of R5RS)***From:*ramsdell@linus.mitre.org (John D. Ramsdell)

**References**:**Re: a (revised) draft of R5RS***From:*ramsdell@linus.mitre.org (John D. Ramsdell)

- Prev by Date:
**Re: a (revised) draft of R5RS** - Next by Date:
**Re: tail recursion (was Re: a (revised) draft of R5RS)** - Prev by thread:
**Re: a (revised) draft of R5RS** - Next by thread:
**Re: tail recursion (was Re: a (revised) draft of R5RS)** - Index(es):