Re: requiring proper tail recursion

[ramsdell@linus.mitre.org (John D. Ramsdell)]

Let me thank Richard for providing a syntactic description of tail
recursion in form that could be put into R5RS.  This effort is a good
start and the text could be refined into something useful.  Before we
go too far down this path, I would like to describe another syntactic
approach that people may prefer.  I have only developed it for the
Lambda Calculus, so I'll focus on it.

Recall that the standard syntax of lambda terms is defined by:

  M --> c | x | \x.M | (M M)		Lambda terms

where c is the syntactic category for constants, x is for variables,
and \ is lambda in ASCII.  The equivalent of the grammar approach I
suggested earlier for Scheme is below.

  T --> V | (U U)			Values and tail combinations
  U --> V | (U U)			Values and non-tail combinations
  V --> c | x | \x.T			Values

where T is the start symbol.

Combinations in the language generated by T are tail combinations and
the ones generated by U are not.

The alternate approach to defining tail combinations is to use
combination contexts.  A combination context is a lambda term when
its hole is replaced by a combination.

  X --> [] | \x.X | (X M) | (M X)	Combination contexts

The term that results from substituting combination (M M') into the
hole in X is X[(M M')].

The set of tail combination contexts is defined by the language
generated by Y.

  Y --> [] | Z				Tail combination contexts
  Z --> \x.Y | (Z M) | (M Z)

Given a term M = X[(M' M")], (M' M") is defined to be a tail
combination if X is a tail combination context.

I have not worked out the details of defining and using procedure call
contexts in Scheme for defining Scheme tail calls.  It looks messy.

John