lambda calculus implementation 
Author Message
 lambda calculus implementation

I would like to implement for fun an interpreter for lambda calculus terms
(with
different reduction strategies).
I know at least two solutions to represent my terms (as inductive
datatypes). The easiest one would
be to represent variables as string, but i'd need to deal with explicit
renaming of bound variables.
The other solution would be to use De Bruijn indices which make subtitution
far more easy than
in the first solution.

I think there's an other solution, that is to use environment (as in the
SECD machine). I have only
vague ideas about this notion of environment.  It seems that it allow to
handle nicely the problem of
substition, but what are the drawbacks (as compared to the two first
solutions) ??? is it limited to
call-by-value reduction ? or  does it allow to reduce closed terms only ????

Thanks in advance for any ideas, or links
    K



Sat, 30 Jul 2005 00:40:15 GMT  
 lambda calculus implementation

Quote:

> I would like to implement for fun an interpreter for lambda calculus terms
> (with different reduction strategies).  I know at least two solutions to
> represent my terms (as inductive datatypes). The easiest one would be to
> represent variables as string, but i'd need to deal with explicit renaming of
> bound variables.  The other solution would be to use De Bruijn indices which
> make subtitution far more easy than in the first solution.

I came across this yesterday, you may find it useful or interesting.
http://pobox.com/~oleg/ftp/Computation/lambda-calc.html
--
Shae Matijs Erisson - 2 days older than RFC0226
#haskell on irc.freenode.net - We Put the Funk in Funktion


Sat, 30 Jul 2005 01:01:33 GMT  
 lambda calculus implementation

I started a similar project a while ago. Here are some pointers that
might be useful.

The SECD architechture is useful since derinving a compiler from a
stack architechture interpreter is... well understandable. Landin's
original machine can be fairly easily changed to support other
evaluation strategies. Some examples are for example in W.H.Burke's
book "Recursive Programming Techniques". As for the use of enviroments
the evaluator-related lectures in

http://www.swiss.ai.mit.edu/classes/6.001/abelson%2Dsussman%2Dlectures/

are certainly useful. Apparently graph reduction and compilation to
combinators have been popular since SECD style interpreters, and
looking up some information on the G-machine architecture might
also be useful. http://citeseer.nj.nec.com/cs is a good place
to start.

And as a shameless plug, there is a sort of graph reduction based
small interpreter at http://213.139.166.37/mindo along with a lambda
calculus interpreter written in itself and some other programs.

--
aki helin



Sat, 30 Jul 2005 03:35:50 GMT  
 lambda calculus implementation

Quote:

> I would like to implement for fun an interpreter for lambda calculus terms
> (with
> different reduction strategies).
> I know at least two solutions to represent my terms (as inductive
> datatypes). The easiest one would
> be to represent variables as string, but i'd need to deal with explicit
> renaming of bound variables.
> The other solution would be to use De Bruijn indices which make subtitution
> far more easy than
> in the first solution.

Even easier substitution can be made by using higher-order abstract
syntax, e.g.:

data lam t = APP (lam, lam) | LAM (t -> lam) | VAR t

You would then represent, e.g., the term \a.\b.(b a) as

LAM (\x-> LAM (\y-> APP (VAR y, VAR x)))

You can write a term using the show function:

  show t = show1 t "x"



  show1 (VAR x) v = x

For the above example, this yields

"(\x.(\xx.xx x))"

The show function can be refined to avoid redundant parenthesis and to
use better names (instead of "x", "xx", "xxx", etc.).

A call-by-name reducer (to WHNF) can then be written as

  cbn (APP (e1, e2)) = let (LAM f) = cbn e1 in f e2
  cbn (LAM f) = LAM f
  cbn (VAR x) = cbn x

A call-by-value reducer (to WHNF) can be written as

  cbv (APP (e1, e2)) = let (LAM f) = cbv e1 in f (cbv e2)
  cbv (LAM f) = LAM f
  cbv (VAR x) = x

        Torben Mogensen



Sat, 30 Jul 2005 19:01:23 GMT  
 lambda calculus implementation
Nice links.  It is W. H. Burge, though.

[Burge1975]
    Burge, William H. Recursive Programming Techniques. Addison-Wesley (Reading, MA: 1975). ISBN 0-201-14450-6.


Quote:

> I started a similar project a while ago. Here are some pointers that
> might be useful.

> The SECD architechture is useful since derinving a compiler from a
> stack architechture interpreter is... well understandable. Landin's
> original machine can be fairly easily changed to support other
> evaluation strategies. Some examples are for example in W.H.Burke's
> book "Recursive Programming Techniques". As for the use of enviroments
> the evaluator-related lectures in

> http://www.swiss.ai.mit.edu/classes/6.001/abelson%2Dsussman%2Dlectures/

> are certainly useful. Apparently graph reduction and compilation to
> combinators have been popular since SECD style interpreters, and
> looking up some information on the G-machine architecture might
> also be useful. http://citeseer.nj.nec.com/cs is a good place
> to start.

> And as a shameless plug, there is a sort of graph reduction based
> small interpreter at http://213.139.166.37/mindo along with a lambda
> calculus interpreter written in itself and some other programs.

> --
> aki helin



Thu, 11 Aug 2005 08:02:52 GMT  
 
 [ 5 post ] 

 Relevant Pages 

1. Lambda Calculus Question

2. Introduction to lambda calculus ?

3. Lambda Calculus Problem!

4. Negativism and division in lambda-calculus

5. Lambda calculus + Church numerals

6. Typed lambda calculus, recursion and halting

7. lambda calculus: delta rules

8. Need help on Lambda calculus reduction please.

9. Q: reduction strategies in lambda calculus

10. Lambda-Calculus

11. Introduction to Lambda Calculus

12. Typed Lambda calculus

 

 
Powered by phpBB® Forum Software