Lambda Calculus Interpreter

Status: Ready to use | Auto-trigger: Yes | Script: python examples/interpreter.py

Triggers

This skill activates when user mentions:

• Implementing lambda calculus interpreters
• Building functional language interpreters
• Understanding beta reduction, closures
• Learning evaluation strategies (CBV, CBN)

Action Prompts

Use these prompts directly:

Implement a call-by-value lambda calculus interpreter with:
- Var, Abs, App AST nodes using dataclasses
- Environment-based closure implementation
- Beta reduction with proper substitution
- Support for Church numerals

Add call-by-name lazy evaluation to existing interpreter:
- Implement Thunk class for delayed evaluation
- Memoize forced thunks
- Compare performance with call-by-value

Extend interpreter with:
- Fixed-point combinator (Y combinator) for recursion
- Simple type system (Bool, Int, Fun types)
- Type inference using bidirectional checking

When to Use

• Learning functional programming foundations
• Implementing interpreters for functional languages
• Studying evaluation strategies (CBV, CBN, parallel)
• Exploring meta-programming concepts

What This Skill Does

1. Parses lambda terms - Concrete → abstract syntax
2. Implements reductions - β-reduction, η-reduction
3. Handles closures - Captures lexical environment
4. Compares strategies - Call-by-value, call-by-name, etc.

Church Encoding Implementation

def church_to_int(n):
    """Convert Church numeral to integer"""
    # Church numeral n is λf. λx. f^n(x)
    # Apply to successor function and zero
    succ = lambda x: x + 1
    return n(succ)(0)

def int_to_church(n):
    """Convert integer to Church numeral"""
    # Build: λf. λx. f(f(...f(x)...)) with n applications
    return lambda f: lambda x: f**n(x) if hasattr(f, '__pow__') else None

# Church arithmetic
church_add = Abs("m", Abs("n", 
    Abs("f", Abs("x", 
        App(App(Var("m"), Var("f")), 
            App(App(Var("n"), Var("f")), Var("x")))))))

church_mult = Abs("m", Abs("n", 
    Abs("f", 
        App(Var("m"), App(Var("n"), Var("f"))))))

church_pred = Abs("n", 
    Abs("f", Abs("x",
        App(
            App(App(Var("n"), 
                   Abs("g", Abs("h", App(Var("h"), App(Var("g"), Var("f")))))),
                Abs("u", Var("x"))),
            Abs("u", Var("u"))))))

Simply-Typed Lambda Calculus (STLC)

# Types
TInt = "int"
TBool = "bool"
TFun = lambda t1, t2: ("fun", t1, t2)

def type_check(t: Term, env: dict) -> Type:
    """Simply-typed lambda calculus type checker"""
    
    match t:
        case Var(x):
            return env[x]
        
        case Abs(param, body):
            # Analyzed from context
            pass
        
        case App(func, arg):
            tf = type_check(func, env)
            if not isinstance(tf, tuple) or tf[0] != "fun":
                raise TypeError(f"Cannot apply non-function: {tf}")
            _, dom, cod = tf
            ta = type_check(arg, env)
            if ta != dom:
                raise TypeError(f"Argument type mismatch: {ta} ≠ {dom}")
            return cod
    
    raise ValueError(f"Unknown term: {t}")

# STLC with type inference (bidirectional)
def synth(t: Term, env: dict) -> tuple[Type, list[Constraint]]:
    """Synthesize type"""
    match t:
        case Var(x):
            return (env[x], [])
        
        case App(e1, e2):
            a = fresh_tvar()
            t1, c1 = synth(e1, env)
            t2, c2 = check(e2, t1[1], env)  # Check arg against domain
            return (t1[2], c1 + c2 + [(t1, ("fun", t2, a))])
        
        # ... more cases

def check(t: Term, expected: Type, env: dict) -> tuple[None, list[Constraint]]:
    """Check term has expected type"""
    match t, expected:
        case Abs(param, body), ("fun", dom, cod):
            return check(body, cod, {**env, param: dom})
        
        case _:
            t, c = synth(t, env)
            return (None, c + [(t, expected)])

Test Cases

Using the Script

# Run the interpreter
cd lambda-calculus-interpreter
python examples/interpreter.py --help

# Run with custom input
python examples/interpreter.py --input "(λx. x) (λy. y)" --strategy cbv

Evaluation Strategies

Tips

• Use de Bruijn indices to avoid alpha-renaming
• Implement environments as immutable maps
• Consider sharing (pointers) for efficiency
• Add letrec for recursion (fixed-point)
• Trace reductions for debugging

Reduction Semantics

# Explicit substitution
def subst(t: Term, x: str, s: Term) -> Term:
    """Substitute s for x in t"""
    match t:
        case Var(y) if y == x:
            return s
        case Var(y):
            return t
        case Abs(y, body) if y != x:
            return Abs(y, subst(body, x, s))
        case App(e1, e2):
            return App(subst(e1, x, s), subst(e2, x, s))
        case _:
            return t

# β-reduction step
def beta_step(t: Term) -> Term:
    """One step of β-reduction"""
    match t:
        case App(Abs(x, body), arg):
            return subst(body, x, arg)  # β-redex
        # ... add congruence rules

Related Skills

• operational-semantics-definer - Language semantics
• type-inference-engine - Hindley-Milner
• simply-typed-lambda-calculus - STLC with types

Canonical References

Research Tools & Artifacts

For lambda calculus implementations, these are the gold-standard references:

Interactive Lambda Calculus Environments

• Lambda Calculi Tool (Cambridge) - Visualization of reductions
• Proof assistants: Coq, Agda, Lean for formalizing lambda calculus
• LEAP (Lambda, Evaluation, Application, Programming) - Educational framework

Research Frontiers

1. Optimal Reduction

• Goal: Reduce to normal form with minimal work
• Key technique: Sharing via graphs, not trees
• Paper: "An Algorithm for Optimal Lambda Calculus Reduction" (Lamping, POPL 1990)
• Implementation: Interaction nets, Gonthier et al. refinement

2. Explicit Substitutions

• Goal: Formalize substitution as a computational step
• Key technique: Environments, stacks, closures
• Paper: "Explicit Substitutions" (Abadi, Cardelli, Curien, 1991)
• Why it matters: Foundation for implementing functional languages

3. Normalization by Evaluation (NbE)

• Goal: Efficiently compute normal forms
• Key technique: Interpret in a continuation-based meta-language
• Paper: "Normalization by Evaluation" (Berger & Schwichtenberg, 1991)
• Implementation: Agda, Coq, Dedukti

4. Abstract Machines

• Goal: Bridge lambda calculus and real execution
• Key technique: SECD, Krivine, CAM
• Paper: "The Mechanical Evaluation of Expressions" (Landin, 1964), "A call-by-name lambda-calculus machine" (Krivine, 1985; published 2007)
• Implementation: Most functional language compilers

Implementation Pitfalls

The following traps have caused real bugs in production systems:

The "Omega Combinator" Problem

The classic omega combinator Ω = (λx. x x) (λx. x x) diverges. Implementations must handle this:

# Safe evaluation with step limiting
def eval_with_limit(term, env, max_steps=10000):
    for _ in range(max_steps):
        if is_value(term):
            return term
        term = step(term, env)
    raise RuntimeError("Non-termination detected")

De Bruijn Index Pitfalls

When implementing de Bruijn indices, common bugs include:

1. Index shifting during substitution: lift must adjust indices correctly
2. Capture in substitution: Must check free variable sets
3. Weak vs strong reduction: Whether to reduce under lambdas

# Correct de Bruijn substitution
def subst(term, index, replacement):
    match term:
        case DB(index') if index' == index:
            return replacement
        case DB(index') if index' > index:
            return DB(index' - 1)  # Shift down
        case Abs(body):
            return Abs(subst(body, index + 1, replacement.lift(1)))
        # ... more cases

Connections to Real Systems

Lambda calculus implementations connect to major systems:

Tradeoffs and Limitations

Evaluation Strategy Tradeoffs

When NOT to Use Pure λ-Calculus

• For practical languages: Add concrete syntax, recursion (Y combinator), constants
• For performance-critical code: Consider closure conversion, compilation to bytecode
• For verification: Use simply-typed or linear variants for stronger guarantees

Limitations

• Encoding overhead: Natural numbers, booleans require Church encodings (inefficient)
• No recursion: Must use fixed-point combinator (Y = λf.(λx.f(x x))(λx.f(x x)))
• α-equivalence: Variables are not identical under renaming; requires care
• Normalization: Untyped λ-calculus is not strongly normalizing (may diverge)

Assessment Criteria

A high-quality λ-calculus interpreter should have:

Quality Indicators

✅ Good: Correct β-reduction, handles closures, configurable strategies ⚠️ Warning: Missing η-reduction, inefficient environments ❌ Bad: Capture-avoidance bugs, infinite loops on normal terms