[TYPES] Is naive freshness adequate to avoid capture?
Rene Vestergaard
vester at jaist.ac.jp
Fri Apr 27 18:13:19 EDT 2012
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
>
More information about the Types-list
mailing list