This project is a small lambda calculus interpreter written in Python.
It was developed as part of the Logic and Computation course practical work.
The interpreter parses lambda expressions, builds an internal abstract syntax tree (AST), and performs beta-reduction using a normal-order (left-most / outer-most) evaluation strategy.
It also applies alpha-conversion when needed to avoid variable capture during substitution.
- Variables (e.g.,
x,y,x1) - Lambda abstractions (
\x. bodyorλx. body) - Applications (e.g.,
f x y) - Parentheses for grouping
( ... ) - Beta-reduction
- Alpha-conversion (capture-avoiding substitution)
- Step-by-step reduction (can be turned on/off)
This interpreter uses normal-order reduction (left-most, outer-most redex first).
This strategy guarantees that if a normal form exists, it will be found.
- Python 3.10 or higher
- No external libraries are required
Open a terminal inside the project folder and run:
python main.py
---
After running the program, you can type lambda expressions directly in the terminal.
Type `quit` to exit.
Optional commands:
- `:steps on` – show all reduction steps
- `:steps off` – show only the final result
---
## Example
Input:
(\x.x) y
Output:
y
---
## Limitations
- No type system is implemented.
- There is a maximum reduction step limit to prevent infinite loops.
- The pretty-printer is simple and always uses parentheses for clarity.