free variables in lambda terms ?

Konst Sushenko
Thu, 25 Apr 2002 20:07:01 -0700

hi, would someone please help me with the question below? i tried asking
on comp.lang.functional list but noone responded...

"konsu" <> wrote in message
> hello,
> as an exercise, i am trying to implement a pure lambda calculus
> i am using normal order reduction with textual substitution of terms.
> a program that my interpreter accepts is a list of name/term
> <name 1> =3D <lambda term 1>
> ...
> <name N> =3D < 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
> and now i got to the point where i need to handle free variables in a
> my assumption is that free variables denote terms declared as above.
> my question is when should i expand free variables? i also would
> 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
> without handling free variables, and then, if it has free variables,
look up
> their definitions in the environment and replace them with their
> evaluate the resulting term to its normal form again, and keep
> this process until no free variables are found.
> is this the right way to do it? or should i check for free variables
when i
> compute the WHNF, etc.? any advice from the experts?
> thanks
> konst