Python Lambda Calculus 3 1 0

lambda_calculus 3.1.0

Overview

lambda_calculus is a pure Python library implementing the core operations of Lambda calculus as an educational tool. It provides three fundamental term types — Variable, Abstraction, and Application — along with visitor-based traversal, beta/eta reduction, alpha conversion, and safe substitution. The library includes Church encodings for booleans, arithmetic, pairs, and well-known combinators (Y, S, K, I, B, C, W).

It is not optimized for speed and expects all terms to be finite. Infinite terms or excessively complex evaluations may raise RecursionError.

When to Use

• Building lambda calculus interpreters or evaluators in Python
• Performing symbolic manipulation of lambda terms (substitution, reduction, variable analysis)
• Encoding computation using Church encodings (booleans, numbers, pairs)
• Teaching functional programming concepts with executable examples
• Implementing custom term transformations via the visitor pattern

Installation

python3 -m pip install lambda-calculus

Core Concepts

Three Term Types

Every lambda expression is built from three constructors:

Building Terms

from lambda_calculus import Variable, Abstraction, Application

# λx.x (identity)
identity = Variable("x").abstract("x")

# λx.λy.x (K combinator)
k = Variable("x").abstract("x", "y")

# Apply identity to a variable
app = identity.apply_to(Variable("a"))

Use .abstract(*vars) on any term to bind variables, and .apply_to(*args) to create applications. For multiple bindings/arguments, pass them positionally — they are curried from first to last.

Analyzing Terms

term = Abstraction.curried(("x", "y"), Application(Variable("x"), Variable("z")))

term.free_variables()     # {"z"}
term.bound_variables()    # {"x", "y"}
term.is_combinator()      # False (has free variable "z")
term.is_beta_normal_form()  # True

Reducing Terms

# Create a redex: (λx.x) a
redex = Application(identity, Variable("a"))
redex.is_redex()           # True
reduced = redex.beta_reduction()  # Variable("a")

# Full beta-normalization via visitor
from lambda_calculus.visitors.normalisation import BetaNormalisingVisitor
visitor = BetaNormalisingVisitor()
for conversion, intermediate in visitor.visit(some_term):
    print(f"{conversion}: {intermediate}")

Substitution with Collision Safety

# Safe substitution — raises CollisionError if free variables would be captured
term.substitute("x", replacement_term)

# Manual alpha conversion before substitution
new_abs = abstraction.alpha_conversion("z")  # rename bound variable

Advanced Topics

Terms API: Term base class, Variable, Abstraction, Application with all methods → Terms API

Visitors API: Visitor pattern, substitution strategies, beta normalization, term traversal → Visitors API

Predefined Constructs: Church booleans, arithmetic, pairs, combinators, letter variables → Predefined Constructs