"konsu" <[EMAIL PROTECTED]> wrote in message news:<ATOx8.42722$[EMAIL PROTECTED]>... > 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 _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell