[TYPES] Is naive freshness adequate to avoid capture?

[Philip Wadler]

Say that a lambda term is 'fresh' if each lambda abstraction binds a
distinct variable.  For instance, (\x.(\y.\z.y)x) is fresh, but
(\x.(\y.\x.y)x) is not.

Consider lambda terms without the alpha rule, where capture avoiding
substitution is a partial function.  For instance, [x/y](\z.y) is
defined, but [x/y](\x.y) is undefined, because the substitution would
result in capture.

Consider a sequence of beta reductions where no alpha reduction is
allowed.  In our first example, this terminates in a normal form:

  (\x.(\y.\z.y)x) -->  \x.\z.x

In our second example, we get stuck.

  (\x.(\y.\x.y)x) -/->

Attempting to beta reduce the redex would result in capture.

Starting with a fresh term and performing beta reductions but no alpha
reductions, are there reduction sequences which get stuck?  I suspect
the answer is yes, but I am having difficulty locating a
counter-example in the literature or creating one on my own.

Answers gratefully received.  Yours,  -- P

-- 
.\ Philip Wadler, Professor of Theoretical Computer Science
./\ School of Informatics, University of Edinburgh
/  \ http://homepages.inf.ed.ac.uk/wadler/

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.