27 Apr 13:14 2012

### [TYPES] Is naive freshness adequate to avoid capture?

[ 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 -- --(Continue reading)