Re: [TYPES] Is naive freshness adequate to avoid capture?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

http://cstheory.stackexchange.com/questions/8947/closed-term-and-alpha-conversion

On Fri, Apr 27, 2012 at 7:14 AM, Philip Wadler <wadler@...> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
> 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.
>
>