Skip to content
A lambda calculus interpreter written in Python
Python
Latest commit 8b7f45a Oct 16, 2014 loris Merge branch 'simoncourtenage-master'
Failed to load latest commit information.
Makefile
README some stuff in the readme May 13, 2011
algorithms.py add test for weak head normal form and use this to terminate reduction Oct 15, 2014
lexer.py moved main out of parser.py Nov 23, 2011
parser.py now the abstraction rule creates an instance of Variable inside the a… Feb 21, 2012
pylambda.py towards adding of predicates on normal form Mar 27, 2012
terms.py
tests.py changed operations in algorithms Feb 21, 2012
todo todo updated Feb 21, 2012

README

pylambda: a lambda calculus interpreter written in python

1. Dependencies
---------------

pylamdbda relies on PLY (Python Lex Yacc). 
You can find it at http://www.dabeaz.com/ply/

2. Running the interpreter
--------------------------

From your shell, type 

$ make run

and you will enter the pylambda interpreter, whose prompt consist
of three '>', just like the python shell.
Time to play:

>>> (\x.x)
(\x.x)

So, what happened here? We have entered the term (\x.x) ('\' is an
alias for 'lambda') and we got the same term back. If you think about it,
(\x.x) is in 'normal form', so it cannot be 'reduced'.

Let's try with something more complicated:

>>>((\x.xx))(\a.az)z
(\x.xx)(\a.az)z  ->  (\a.az)z(\a.az)z
(\a.az)z(\a.az)z  ->  zz(\a.zz)z
zz(\a.zz)z  ->  zzzz
zzzz

Here, the interpreter picked up the expression we entered and 'reduced'
it to its 'normal form', via a multi-step 'beta reduction'. 
As one can notice, the choice of the 'redex' to reduce at every step
is made following a 'leftmost-outermost' strategy.


3. Future work
--------------

pylambda is in its very early stages. It needs

- better handling of lexical and syntax errors
- a suite of tests
- some *good* doc

Moreover, it would be nice to provide, with the next releases,
support for the following stuff:

- alpha-conversion
- church numerals
- typed lambda calculus
Something went wrong with that request. Please try again.