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

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

Bentiamino,  Many thanks for your counter-example.  Yours, -- P

On Fri, Apr 27, 2012 at 4:19 PM, Beniamino Accattoli
<beniamino.accattoli@...> wrote:
> Dear Philip,
> My first observation has been that it is easy to break "freshness",
> just consider the reduction of \delta \delta. But in this case is
> however possible to reduce without ever using alpha.
>
> If I understand the problem correctly, this is a counter-example for
> both freshness and alpha:
>
> (\l z.zz) (\ly.\lx.yx)
> ->
> (\ly.\lx.yx) (\ly.\lx.yx)
> ->
> \lx.((\ly.\lx.yx)x)
> -/->
>
> Best,
> Beniamino Accattoli
>
> On Fri, Apr 27, 2012 at 1:14 PM, 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.