[TYPES] Is naive freshness adequate to avoid capture?

[LD]

[Resending from former email address as current one is rejected by  
list.]

Dear Philip,

Such freshness resembles usual axiomatisations in proof-theoretic
logical treatments of (typed) lambda calculus.

Keeping track of lambda subterm free variables invariantly for beta and
eta (open) reduction (working like a static type) avoids variable  
capture,
dispensing alpha conversion and simplifying substitution (N/y of term N
for variable y) to replacement (otherwise in general possibly  
capturing).

Write

X for an useq; ie sequence without repetitions of free variables (eg  
x,y,z)

X # Y for disjoint X and Y ie when X and Y have no common elements

[X]M for an (X free variables) annotated lambda term M; derived by rules
	[X,y,Z]y if (X # Z and X # y and y # Z); ie all pairwise disjoint

	[X](M N) if ([X]M and [X]N)

	[X](\y.M) if (X # y and [X,y]M)

[X]C{[X,Y]} for an annotated context ie an annotated term with hole {}

[X]C{[X,Y]M} for [X]C{[X,Y]} with {} replaced by [X,Y]M.

Then I expect

[X]((\y.M) N) -beta-> [X]((N/y)M)

[X](\y.(M y)) -eta-> [X]M if X includes all free variables of M

[X]C{[X,Y]M} -> [X]C{[X,Y]M'} if [X,Y]M -> [X,Y]M'

X=X' if [X]M ->* [X']M' ie
free variables (super)useq is preserved by reduction (like type
preservation ie subject reduction in typed lambda calculi)

to follow gradually from the above.

Hope this basis-like typed formalisation helps even for lambda  
reduction.

Cheers,
Luis Dominguez

On 2012/04/27, at 12:14, 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
>
> -- 
> .\ 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.
>