free variables in lambda terms ?

[Konst Sushenko]

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


"konsu" <konsu@hotmail.com> wrote in message
news:<ATOx8.42722$t65.9246@nwrddc02.gnilink.net>...
> hello,
>=20
> as an exercise, i am trying to implement a pure lambda calculus
interpreter.
> i am using normal order reduction with textual substitution of terms.
>=20
> a program that my interpreter accepts is a list of name/term
declarations:
>=20
> <name 1> =3D <lambda term 1>
> ...
> <name N> =3D < lambda term N>
>=20
> each declaration defines a global name and binds a term to it, and the
> interpreter starts evaluation with the term named 'main'.
>=20
>=20
> 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.
>=20
> my question is when should i expand free variables? i also would
appreciate
> any references to literature, etc. where this is discussed.
>=20
> 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.
>=20
> 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?
>=20
> thanks
> konst
>=20
>=20