Re: free variables in lambda terms ?
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
Re: free variables in lambda terms ?
Konst,
From: Konst Sushenko [EMAIL PROTECTED]
Subject: free variables in lambda terms ?
Date: 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 [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.
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?
You want to substitute the definitions of your names when
you apply one to an expression.
name = \x - body
main = name (4+5)
main
- name (4+5)
- (\x - body) (4+5)
- body[(4+5)/x]
@Book{peyton-jones87,
author= {Peyton Jones, Simon L.},
title = {The Implementation of Functional Programming Languages},
publisher = {Prentice-Hall International},
address = {London},
year = 1987
}
Also read about name capture.
Marko
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
