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

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

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 ]
>