free variables in lambda terms ?

[Marko Schuetz]

Konst,

From: "Konst Sushenko" <konsu@microsoft.com>
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" <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?

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