free variables in lambda terms ?

[John Hughes]

	"konsu" <konsu@hotmail.com> wrote in message
	news:<ATOx8.42722$t65.9246@nwrddc02.gnilink.net>...
	> hello,
	> 
	> as an exercise, i am trying to implement a pure lambda calculus
	interpreter.
	> i am using normal order reduction with textual substitution of terms.
	> 
	> a program that my interpreter accepts is a list of name/term
	declarations:
	> 
	> <name 1> = <lambda term 1>
	> ...
	> <name N> = < lambda term N>
	> 
	> each declaration defines a global name and binds a term to it, and the
	> interpreter starts evaluation with the term named 'main'.
	> 
	> 
	> i implemented all the functions necessary to evaluate a closed lambda
	term,
	> and now i got to the point where i need to handle free variables in a
	term.
	> my assumption is that free variables denote terms declared as above.
	> 
	> my question is when should i expand free variables? i also would
	appreciate
	> any references to literature, etc. where this is discussed.
	> 
	> so far i believe the way to do it is to reduce a term to its normal
	form
	> without handling free variables, and then, if it has free variables,
	look up
	> their definitions in the environment and replace them with their
	bodies,
	> evaluate the resulting term to its normal form again, and keep
	repeating
	> this process until no free variables are found.
	> 

This is certainly one reasonable possibility. Alternatively, you could replace
a free variable by its value as soon as you encounter it in a reduction
context (i.e. at the point where your reducer would make the next reduction
step). Since you're aiming for normal forms rather than weak head normal
forms, you presumably will substitute for free variables under lambdas.

I assume you're being careful not to capture variable names during
substitution -- beware of cases like

	     f = g
	     g = 1
	     main = (\g.f) 2

where substituting for f in main must rename the local variable g to avoid a
name clash with the global g.

Given the Church-Rosser property, it doesn't really matter when you substitute
for free variables -- you should get the same result in any case. The only
thing to be careful of is that you don't substitute "too eagerly", and thus
fall into an infinite loop. Global definitions are presumably the only way to
achieve recursion in your system (apart from using Y); substituting too
eagerly in recursive definitions will of course lead to loops. Just consider

fac = \n. if (== n 0) 1 (* n (fac (- n 1)))

where if you substitute for fac before applying the lambda-expression, you
clearly fall into a loop.

John Hughes