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

Unwinding Theorem



Date: Thu, 12 Dec 91 15:05:06 EST

Literature search question: does anyone know other references for
the THEOREM below?

Consider the lambda calculus with
        1. Basic arithmetic operations and
        2. A recursion construct mu x:t. M
The language PCF would do: Scott and Plotkin's langauge has a Y operator,
Y(\ x:t. M) is equivalent to mu x:t. M.  Now, suppose we are given an
operational semantics for this langauge in the form of rules such as

      		 [(mu x:t. M) / x] M => V
      		 ------------------------
      		      mu x:t. M => V

where => should be read as `evaluates to'.

Everybody knows that if you have a term M of ground type in such a
language, then a recursion subterm mu x:t. N of M can be replaced by
an unwinding [(mu x:t. N) / x] N without affecting the results of the
evaluation of the term.  Let me write
        mu^n x:t. M = [(mu^n x:t. M) / x] M  if n>0
        mu^0 x:t. M = mu x:t. x
where M is any term (not necessarily of gound type).  If the
evaluation of M terminates, then no recursion subterm of M was unwound
more than finitely many times.  My question is, who has published
proof of a kind of converse of this:

THEOREM: If (mu^n x:t. M)(N)...(N') => V is of ground type, then
(mu x:t. M)(N)...(N') => V.

The result can be proved using adequacy, but it is also possible to
prove adequacy using it.  (Plotkin omits the proof of his version of
this result---based there on a transition semantics---in his `LCF as a
programming language' paper.)  There is a syntactic proof of a closely
related result and a kind of converse in the Cornell thesis of Scott
Smith.