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,
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.
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