A C++ implementation of a lambda calculus interpreter. Interpreter supports named expressions, allowing you to define and reuse common lambda expressions.
- Pure Lambda Calculus Core: Supports variables, abstractions (λx.M), and applications (M N)
- Named Expressions: Define expressions once and reuse them by name
- Beta Reduction: Properly handles variable substitution with alpha conversion
- Normal Order Evaluation: Implements the standard evaluation strategy for lambda calculus
- Church Encodings: Pre-loaded examples of Church numerals, booleans, and operations
- Interactive Mode: Command-line interface for experimenting with lambda expressions
- CMake 3.10 or higher
- C++17 compatible compiler
mkdir build
cd build
cmake ..
cmake --build ../lambda_calculus> zero = \f.\x.x
Defined zero = λf.λx.x
> one = \f.\x.f x
Defined one = λf.λx.f x
> plus = \m.\n.\f.\x.m f (n f x)
Defined plus = λm.λn.λf.λx.m f (n f x)
> (plus one one)
Parsed: ((λm.λn.λf.λx.m f (n f x) λf.λx.f x) λf.λx.f x)
Result: λf.λx.f (f x)
This is equivalent to: two
:defs- Show all defined expressions:help- Display help information:quitor:exit- Exit the interpreter
The interpreter comes pre-loaded with several Church encodings:
- Numerals:
zero,one,two,three - Arithmetic:
succ,plus,mult,pred - Booleans:
true,false - Control Flow:
if,iszero - Recursion:
Y(Y combinator)
The project is structured around these key components:
- Expression Hierarchy: Defines the AST structure
- Visitor Pattern: Separates operations from AST structure
- Parser: Converts strings to expression trees
- Evaluator: Performs beta reduction according to normal order rules
- Environment: Stores and manages named expressions
Some possible extensions to consider:
- Applicative Order Evaluation: Implement innermost-first reduction
- Type Checking: Add simple types and type inference
- Standard Library: More pre-defined combinators and utilities
- Step-by-Step Evaluation: Show the intermediate steps of reduction
- Y-Combinator: Fixing issues with y-combinator definition