[TYPES] Is naive freshness adequate to avoid capture?
Philip Wadler
wadler at inf.ed.ac.uk
Fri Apr 27 11:26:45 EDT 2012
Bentiamino, Many thanks for your counter-example. Yours, -- P
On Fri, Apr 27, 2012 at 4:19 PM, Beniamino Accattoli
<beniamino.accattoli at gmail.com> 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 at inf.ed.ac.uk> 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.
>>
>
--
.\ 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.
More information about the Types-list
mailing list