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.

Test Cases

    case ClosureValue("f", body, env):
        # Apply to (λx. x + 1) and (λx. x)
        zero = Abs("x", Var("x"))
        succ = Abs("x", App(Var("f"), Var("x")))
        # This is simplified; real implementation needs care
        return n  # Return stored n
raise TypeError("Not a Church numeral")

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)

```python
# 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: "Optimal Lambda Reduction" (Lamping, 1990) - Sangiorgi's later work
• •Implementation: Optimal, Borough, Catt

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 SECD Machine" (Landin, 1964), "The Krivine Machine" (Krivine, 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