[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.