[TYPES] Is naive freshness adequate to avoid capture?

[Vincent van Oostrom]

Maybe it's interesting to note that each of the three reduction steps
of the canonical counterexample as given by Beniamonino corresponds
to a phenomenon that, when forbidden, yields a calculus that
is safe (cf. the work of Blum and Ong in the typed case),
in the sense that the initial term can be renamed
such that alpha-free-substitution is correct during reduction:
(1) Duplicating step. Forbidding gives linear lambda-calculus;
(2) Created step. Forbidding gives developments (Rene points out);
(3) Step below lambda. Forbidding gives weak reduction.
For more on this see pp. 24-38 of our presentation:
http://www.phil.uu.nl/~oostrom/publication/talk/terese181110.pdf
In the corresponding paper (also available from my homepage):
http://dx.doi.org/10.1016/j.tcs.2011.04.011
it is shown that mu-reduction as captured by the rule
   mu x.Z(x) -> Z(mu x.Z(x))
is safe in the above sense (without more). A general setting
encompassing both the mu-rule and developments as in (2) above, is
provided by a certain class of higher-order recursive program schemes
for which "self-capture-freeness" is preserved under reduction
(freshness is not preserved as Beniamonino points out).

kind regards,
Vincent van Oostrom

On 28-04-12 00:13, Rene Vestergaard wrote:
> [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> All residual (non-renaming) beta-steps are enabled for fresh terms,
> i.e., all beta-reductions of redexes that are not newly created with
> respect to the fresh term we start from have enabled renaming-free
> substitutions. This follows from (what Vincent van Oostrom once told me
> is called) Hyland's Disjointness Property: within beta-residual theory,
> two descendants of a given redex are disjoint, i.e., neither contains
> the other.
>
> Theorem 2.17 in my PhD thesis (The primitive proof of the
> lambda-calculus) shows that any sequence of residual beta-steps from a
> fresh term can be residually-completed. The setting of the result is the
> marked lambda-calculus, with a marked and an unmarked application
> constructor and only (renaming-free) beta-reduction for the former kind.
> Residual completion is the (partial) function that attempts to contract
> all marked redexes inside-out.
>
> Hope this help with the slightly bigger picture,
> Rene
>
>
> On 4/27/12 8:14 PM, Philip 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
>>
>