Project 3: Reduction Visualizer

Metadata

Attribute	Value
Title	Lambda Calculus Reduction Visualizer
Difficulty	Advanced
Main Language	Haskell
Alternative Languages	Elm, PureScript, Racket
Prerequisites	Project 1 (Lambda Calculus Interpreter), basic terminal/web UI concepts
Estimated Time	1-2 weeks
Knowledge Area	Lambda Calculus / Evaluation Strategies
Main Book	“Types and Programming Languages” by Benjamin Pierce

Learning Objectives

By completing this project, you will be able to:

Identify all redexes in a lambda term and explain why each is a valid reduction site.
Implement multiple reduction strategies (normal order, applicative order, call-by-value, call-by-name) and articulate the tradeoffs between them.
Visualize the substitution process showing exactly what variable is replaced with what value and where capture-avoiding renaming occurs.
Demonstrate the Church-Rosser theorem practically by showing how different reduction paths converge to the same normal form.
Detect and report divergence by recognizing when terms loop indefinitely and explaining why.
Build an interactive exploration tool that allows users to manually select which redex to reduce, building intuition for reduction strategies.
Connect reduction strategies to evaluation in real languages by explaining how Haskell’s lazy evaluation and strict languages’ eager evaluation relate to these strategies.

Conceptual Foundation

What Is Reduction?

At its core, computation in lambda calculus is reduction: transforming a term step by step until it reaches a normal form (a term that cannot be reduced further) or diverges (runs forever).

The only computational step is beta-reduction: when you have a function applied to an argument, substitute the argument into the function body.

(lambda x. body) arg  -->  body[x := arg]

But here is the critical question: what if there are multiple places where reduction can happen?

Redexes: Sites of Computation

A redex (reducible expression) is any subterm of the form (lambda x. body) arg. Finding all redexes is the first step in understanding reduction.

Consider this term:

(lambda x. (lambda y. y) x) ((lambda z. z) w)

There are THREE redexes:

The whole term: (lambda x. (lambda y. y) x) ((lambda z. z) w)
Inside the body: (lambda y. y) x
In the argument: (lambda z. z) w

Which do you reduce first? The answer depends on your reduction strategy.

Reduction Strategies: A Taxonomy

Different reduction strategies are defined by which redex they choose:

Normal Order (Leftmost-Outermost)

Always reduce the leftmost redex that is not contained inside another redex.

“Leftmost” = closest to the beginning of the term (when written linearly)
“Outermost” = not inside another lambda body or application argument that is itself a redex

This is also called call-by-name evaluation (arguments are not evaluated before substitution).

Applicative Order (Leftmost-Innermost)

Always reduce the leftmost redex that does not contain another redex.

“Innermost” = all subterms are already reduced
This is call-by-value evaluation (arguments are evaluated before substitution)

Call-by-Value (Weak Head Normal Form)

Like applicative order, but do not reduce inside lambda bodies. Stop at weak head normal form (WHNF): a lambda abstraction or a neutral term (variable or application where the function is neutral).

Call-by-Need (Lazy Evaluation)

Like call-by-name, but memoize evaluated arguments. This is what Haskell uses - a combination of normal order’s termination properties with efficiency.

The Church-Rosser Theorem: Order Does Not Matter (Much)

One of the most beautiful results in lambda calculus:

Theorem (Church-Rosser / Confluence): If a term M can reduce to both N1 and N2 (possibly via different paths), then there exists a term N3 such that both N1 and N2 can reduce to N3.

Corollary: If a term has a normal form, that normal form is unique (up to alpha-equivalence).

This means that if you reach an answer, you reach the same answer regardless of strategy. But strategies differ in whether you reach an answer.

Normalization: When Strategies Diverge

Not all terms have normal forms. The classic example:

Omega = (lambda x. x x) (lambda x. x x)

Reducing this:

(lambda x. x x) (lambda x. x x)
--> (lambda x. x x) (lambda x. x x)   [x := (lambda x. x x)]
--> (lambda x. x x) (lambda x. x x)
--> ...forever

Every strategy loops on Omega. But consider:

K Omega = (lambda x. lambda y. x) Omega
       = (lambda x. lambda y. x) ((lambda z. z z) (lambda z. z z))

Normal order:

(lambda x. lambda y. x) Omega
--> lambda y. Omega[x := Omega]... wait, x does not appear in (lambda y. x)?
Actually x does appear: (lambda x. lambda y. x) Omega --> lambda y. x... no wait.
Let me be more careful:

(lambda x. lambda y. x) Omega
The redex is (lambda x. lambda y. x) applied to Omega.
Beta-reduce: substitute Omega for x in (lambda y. x)
Result: lambda y. Omega

Wait, that is wrong! x in (lambda y. x) should be replaced.
(lambda x. lambda y. x) Omega --> lambda y. Omega... no!

Let me reconsider. In (lambda x. lambda y. x):
- x is bound by the outer lambda
- The body is (lambda y. x)
- Substituting Omega for x: (lambda y. Omega)? No!

Actually the answer depends on whether we substitute before or after.

In (lambda x. lambda y. x):
- x is bound
- When we apply this to Omega:
- (lambda x. (lambda y. x)) Omega --> (lambda y. x)[x := Omega] = (lambda y. Omega)

Still wrong! Let me trace more carefully:

(lambda x. lambda y. x)
This is a function that takes x and returns (lambda y. x).

(lambda x. lambda y. x) Omega
Apply to Omega: substitute Omega for x in (lambda y. x)
= lambda y. Omega

This is still not right. In (lambda y. x), x is FREE (bound by the outer lambda).
Substituting Omega for x gives (lambda y. Omega).

But wait - Omega is the term ((lambda z. z z) (lambda z. z z)).
So we get: lambda y. ((lambda z. z z) (lambda z. z z))

This is in WHNF but not normal form (Omega is a redex inside).

But in NORMAL ORDER, we found the normal form: lambda y. Omega
Because normal order stops at WHNF? No, normal order goes to full normal form.

Let me reconsider the example. The key is that:
(lambda x. lambda y. x) Omega
--> lambda y. Omega

Now we have (lambda y. Omega). Is this in normal form?
The body is Omega = (lambda z. z z) (lambda z. z z), which is a redex.
So we should reduce inside the lambda:
lambda y. Omega --> lambda y. Omega --> ...loops

Hmm, so normal order also loops?

Let me try a better example:
(lambda x. lambda y. y) Omega

(lambda x. lambda y. y) Omega
--> (lambda y. y)[x := Omega]
--> lambda y. y   (x does not occur free in (lambda y. y))

This IS the normal form! Normal order terminates.

Now applicative order:
(lambda x. lambda y. y) Omega
First, try to reduce the argument Omega:
Omega --> Omega --> Omega --> ...loops

Applicative order never gets to reduce the outer redex because it tries to evaluate Omega first.

Key insight: Normal order finds the normal form whenever one exists. Applicative order may loop even when a normal form exists.

Why Visualization Matters

These concepts are abstract. A visualizer makes them concrete by:

Highlighting redexes: See exactly where reduction CAN happen
Showing substitution: Watch variables get replaced step by step
Comparing strategies: Same term, different paths, same (or different) result
Detecting divergence: Recognize patterns that indicate infinite loops
Building intuition: Interactive exploration beats passive reading

Positions and Paths in Lambda Terms

To implement a visualizer, we need to address subterms by their position. A path describes how to navigate from the root to a subterm:

Term: (lambda x. x y) z

Structure:
        App
       /   \
    Lam     z
   /   \
  x    App
      /   \
     x     y

Paths:
- Here (root): the whole term (lambda x. x y) z
- GoLeft.Here: (lambda x. x y)
- GoLeft.GoBody.Here: x y
- GoLeft.GoBody.GoLeft.Here: x
- GoLeft.GoBody.GoRight.Here: y
- GoRight.Here: z

We can represent paths as:

data Path = Here | GoLeft Path | GoRight Path | GoBody Path

Finding All Redexes

A redex is App (Lam x body) arg. To find all redexes, traverse the term and record positions:

findRedexes :: Term -> [(Path, Term)]
findRedexes (App (Lam x body) arg) =
  (Here, App (Lam x body) arg) :
  map (first GoLeft) (findRedexes (Lam x body)) ++
  map (first GoRight) (findRedexes arg)
findRedexes (App f a) =
  map (first GoLeft) (findRedexes f) ++
  map (first GoRight) (findRedexes a)
findRedexes (Lam x body) =
  map (first GoBody) (findRedexes body)
findRedexes (Var _) = []

Reduction at a Position

Once we have identified redexes and their positions, we can reduce at any position:

reduceAt :: Path -> Term -> Term
reduceAt Here (App (Lam x body) arg) = subst x arg body
reduceAt (GoLeft p) (App f a) = App (reduceAt p f) a
reduceAt (GoRight p) (App f a) = App f (reduceAt p a)
reduceAt (GoBody p) (Lam x body) = Lam x (reduceAt p body)
reduceAt _ term = error "Invalid path"

Implementing Strategies via Redex Selection

With findRedexes and reduceAt, strategies are just selection criteria:

Normal Order: Select the first redex in the list (if we traverse correctly, this is leftmost-outermost).

Applicative Order: Select the last redex in the list (deepest first).

User Choice: Present all redexes, let the user pick.

Detecting Divergence

Two approaches:

Step limit: After N steps without reaching normal form, report possible divergence.
Loop detection: Keep history of seen terms; if a term repeats, we are looping.

Loop detection requires comparing terms for equality. With alpha-equivalence, this is tricky. Options:

Use de Bruijn indices for comparison
Hash terms with a structural hash function
Limit history size and accept false negatives

Visualization Techniques

Text-Based (Terminal UI):

Step 1:
  [(lambda x. x y)]_{redex1} z

  Reducing redex1: (lambda x. x y) z
  Substitution: x := z in (x y)

Step 2:
  z y

  Normal form reached.

Graphical (AST Tree):

        App
       /   \
   [Lam]    z     <-- redex highlighted
   / \
  x  App
    /  \
   x    y

After reduction:

    App
   /   \
  z     y

Interactive:

Click on redexes to reduce them
Toggle between strategies
Step forward/backward through history
Show “what if” branches for different redex choices

The Trade-off Triangle

Reduction strategies balance three concerns:

Termination: Will we find the normal form if it exists?
- Normal order: Always (if NF exists)
- Applicative order: Not always
Efficiency: How much work do we do?
- Normal order: May duplicate work (evaluate same argument multiple times)
- Call-by-need: Best of both (lazy + memoized)
Predictability: What order do effects happen?
- Strict evaluation: Left-to-right, predictable
- Lazy evaluation: On-demand, surprising

Connection to Real Languages

Language	Strategy	Why
Haskell	Call-by-need	Lazy: termination + efficiency via memoization
ML/OCaml	Call-by-value	Strict: predictable effects, simpler reasoning
Scheme	Call-by-value	Strict with explicit delay/force for laziness
Python	Call-by-value	Strict: imperative heritage
JavaScript	Call-by-value	Strict: C-family conventions

Historical Note: The Standardization Theorem

Beyond Church-Rosser, the Standardization Theorem says that if a term has a normal form, the normal order reduction to that normal form has the shortest length among all reduction sequences.

Normal order is not just “safer” (always finds NF if it exists), it is also “optimal” in a precise sense.

Project Specification

Core Requirements

Build an interactive visualizer for lambda calculus reduction with the following capabilities:

1. Redex Identification

Find all redexes in any lambda term
Annotate redexes with their position (path)
Classify redexes: outermost, innermost, redex containing other redexes

2. Step-by-Step Reduction

Single-step reduction with user-chosen redex
Automatic reduction with selectable strategy
Show substitution details: what variable, what value, where

3. Multiple Strategies

Normal order (leftmost-outermost)
Applicative order (leftmost-innermost)
Call-by-value (weak head normal form)
Interactive (user selects redex)

4. Visualization

Highlight redexes in term display
Show reduction trace with step numbers
Indicate which redex was reduced at each step
Show substitution symbolically: [x := arg]

5. Divergence Detection

Detect when the same term appears twice (loop)
Step limit with warning
Display the repeating cycle when detected

6. Comparison Mode

Run two strategies side-by-side
Show where they diverge in choices
Demonstrate Church-Rosser by showing convergence

User Interface

Terminal UI Example:

==================================================
Lambda Calculus Reduction Visualizer
==================================================

Input: (\x. \y. x y) ((\z. z) a) b

Parsed AST:
  App
    App
      Lam x
        Lam y
          App (Var x) (Var y)
      App                        <-- REDEX [2]
        Lam z (Var z)
        Var a
    Var b                        <-- Outermost application
    ^-- REDEX [1]

Found 2 redexes:
  [1] (\x. \y. x y) ((\z. z) a)  @ position: root.left
      OUTERMOST
  [2] (\z. z) a                   @ position: root.left.right
      INNERMOST

Commands:
  n - Normal order step
  a - Applicative order step
  1,2,... - Reduce specific redex
  r - Run to normal form
  s - Switch strategy
  h - Show history
  q - Quit

Choice> n

--------------------------------------------------
Step 1 (Normal Order):
--------------------------------------------------

(\x. \y. x y) ((\z. z) a) b
     ^------------------------^ reducing this redex

Substitution: x := ((\z. z) a)

Result: (\y. ((\z. z) a) y) b

--------------------------------------------------
Step 2:
--------------------------------------------------

(\y. ((\z. z) a) y) b
^-------------------^ reducing this redex

Substitution: y := b

Result: ((\z. z) a) b

--------------------------------------------------
Step 3:
--------------------------------------------------

((\z. z) a) b
^---------^ reducing this redex

Substitution: z := a

Result: a b

--------------------------------------------------
NORMAL FORM REACHED: a b
Total steps: 3
Strategy: Normal Order
==================================================

Divergence Display:

Input: (\x. x x) (\x. x x)

Step 1:
  (\x. x x) (\x. x x)
  Substitution: x := (\x. x x)
  Result: (\x. x x) (\x. x x)

Step 2:
  (\x. x x) (\x. x x)
  Substitution: x := (\x. x x)
  Result: (\x. x x) (\x. x x)

WARNING: Divergence detected!
  The term has returned to a previously seen state.
  This expression has no normal form.

Cycle: Step 1 -> Step 2 -> Step 1 -> ...

Comparison Mode:

==================================================
Strategy Comparison: (\x. \y. y) ((\z. z z) (\z. z z))
==================================================

                NORMAL ORDER         |    APPLICATIVE ORDER
-------------------------------------|-------------------------------------
Step 1:                              |
  Reduce: (\x. \y. y) Omega          |  Reduce: Omega
  Result: \y. y                      |  Result: Omega
                                     |
Step 2:                              |
  NORMAL FORM: \y. y                 |  Reduce: Omega
                                     |  Result: Omega
                                     |
                                     |  Step 3: ... (diverges)

RESULT:
  Normal Order: \y. y (2 steps)
  Applicative Order: DIVERGES

This demonstrates why normal order is "safer" for finding normal forms.
==================================================

Commands

Command	Description
`<expr>`	Parse and display redexes
`:step`	Single step with current strategy
`:step n`	n steps
`:normal`	Single normal-order step
`:applicative`	Single applicative-order step
`:reduce N`	Reduce redex number N
`:run`	Run to normal form or limit
`:run N`	Run up to N steps
`:strategy <s>`	Set strategy (normal/applicative/cbv/interactive)
`:compare`	Run both strategies side-by-side
`:history`	Show reduction history
`:back`	Undo last reduction
`:tree`	Display AST as tree
`:limit N`	Set step limit (default 100)
`:help`	Show help
`:quit`	Exit

Solution Architecture

Data Structures

Lambda Term:

data Term
  = Var String
  | Lam String Term
  | App Term Term
  deriving (Eq, Show)

Position Path:

data Path
  = Here
  | GoLeft Path
  | GoRight Path
  | GoBody Path
  deriving (Eq, Show)

Redex Information:

data Redex = Redex
  { redexPath :: Path
  , redexTerm :: Term
  , redexIsOutermost :: Bool
  , redexIsInnermost :: Bool
  , redexVariable :: String
  , redexArgument :: Term
  }

Reduction Step:

data ReductionStep = ReductionStep
  { stepBefore :: Term
  , stepAfter :: Term
  , stepRedex :: Redex
  , stepSubstitution :: (String, Term)  -- (var, value)
  }

Reduction Result:

data ReductionResult
  = NormalForm Term [ReductionStep]
  | Diverges [ReductionStep] (Maybe (Int, Int))  -- cycle indices
  | StepLimitReached Term [ReductionStep]

Visualizer State:

data VisualizerState = VisualizerState
  { currentTerm :: Term
  , history :: [ReductionStep]
  , strategy :: Strategy
  , stepLimit :: Int
  , seenTerms :: Map Term Int  -- term -> step number (for cycle detection)
  }

Module Organization

src/
  Lambda/
    Syntax.hs         -- Term type, pretty printing
    Parser.hs         -- Parsing lambda expressions
    Path.hs           -- Position/path in term tree
    Redex.hs          -- Finding and classifying redexes
    Substitution.hs   -- Capture-avoiding substitution
    Reduction.hs      -- Single-step reduction
    Strategy.hs       -- Reduction strategies
    Visualizer.hs     -- Visualization formatting
    Divergence.hs     -- Loop detection
    REPL.hs           -- Interactive loop
  Main.hs
test/
  ...

Key Algorithms

Finding Redexes with Classification:

findRedexes :: Term -> [Redex]
findRedexes term = classify $ go Here term
  where
    go path t@(App (Lam x body) arg) =
      (path, x, body, arg) :
      go (GoLeft path) (Lam x body) ++
      go (GoRight path) arg
    go path (App f a) =
      go (GoLeft path) f ++ go (GoRight path) a
    go path (Lam x body) =
      go (GoBody path) body
    go path (Var _) = []

    classify rawRedexes =
      map (\(p, x, b, a) -> Redex
        { redexPath = p
        , redexTerm = App (Lam x b) a
        , redexVariable = x
        , redexArgument = a
        , redexIsOutermost = not (any (isPrefix p) otherPaths)
        , redexIsInnermost = not (any (p `isPrefix`) otherPaths)
        }) rawRedexes
      where otherPaths = map (\(p,_,_,_) -> p) rawRedexes

Strategy Selection:

selectRedex :: Strategy -> [Redex] -> Maybe Redex
selectRedex NormalOrder redexes =
  find redexIsOutermost (sortByLeftmost redexes)
selectRedex ApplicativeOrder redexes =
  find redexIsInnermost (sortByLeftmost redexes)
selectRedex CallByValue redexes =
  find (\r -> redexIsInnermost r && notUnderLambda r) (sortByLeftmost redexes)
selectRedex (Interactive n) redexes =
  if n < length redexes then Just (redexes !! n) else Nothing

Divergence Detection:

checkDivergence :: Term -> Map Term Int -> Int -> Maybe (Int, Int)
checkDivergence term seenTerms currentStep =
  case Map.lookup term seenTerms of
    Just prevStep -> Just (prevStep, currentStep)  -- Found cycle
    Nothing -> Nothing

Visualization Formatting:

formatStep :: ReductionStep -> String
formatStep step = unlines
  [ formatTermWithHighlight (stepBefore step) (redexPath $ stepRedex step)
  , "  Reducing: " ++ prettyPrint (redexTerm $ stepRedex step)
  , "  Substitution: " ++ fst (stepSubstitution step) ++ " := " ++
      prettyPrint (snd $ stepSubstitution step)
  , "  Result: " ++ prettyPrint (stepAfter step)
  ]

Implementation Guide

Phase 1: Path and Position Infrastructure (Days 1-2)

Milestone: Navigate and address any subterm.

Define the Path data type
Implement isPrefix :: Path -> Path -> Bool
Implement pathDepth :: Path -> Int
Implement getSubterm :: Path -> Term -> Maybe Term
Implement replaceSubterm :: Path -> Term -> Term -> Term
Test navigation thoroughly

Hint Layer 1: A path is like a list of directions; implement common list operations Hint Layer 2: isPrefix p1 p2 checks if following p1 is a prefix of following p2 Hint Layer 3: getSubterm should return Nothing for invalid paths Hint Layer 4: Use pattern matching to navigate; recursively descend following the path

Phase 2: Redex Finding (Days 3-4)

Milestone: Find and classify all redexes in any term.

Implement basic findRedexes :: Term -> [(Path, Term)]
Add classification: outermost/innermost
Add ordering: leftmost-first
Build the full Redex record type
Test with complex nested terms

Hint Layer 1: A redex matches the pattern App (Lam x body) arg Hint Layer 2: Traverse the whole term; collect matches with their paths Hint Layer 3: Outermost = no other redex path is a prefix of this one Hint Layer 4: Leftmost can be determined by comparing paths lexicographically

Phase 3: Single-Step Reduction (Day 5)

Milestone: Reduce at any specified position.

Implement reduceAt :: Path -> Term -> Term
Build ReductionStep record with before/after/substitution
Test single steps at various positions
Verify substitution is capture-avoiding

Hint Layer 1: Use the subst function from Project 1 Hint Layer 2: Navigate to the redex position, then apply substitution Hint Layer 3: Record the variable name and argument for visualization Hint Layer 4: Edge case: what if the path is invalid? Return unchanged or error?

Phase 4: Strategy Implementation (Days 6-7)

Milestone: Automatic reduction with multiple strategies.

Implement normalOrderStep :: Term -> Maybe ReductionStep
Implement applicativeOrderStep :: Term -> Maybe ReductionStep
Implement callByValueStep :: Term -> Maybe ReductionStep
Implement runStrategy :: Strategy -> Int -> Term -> ReductionResult
Test: verify different strategies on key examples

Hint Layer 1: Strategy = select which redex from the list Hint Layer 2: Normal order: first outermost; Applicative: first innermost Hint Layer 3: Call-by-value: innermost, but not under lambda Hint Layer 4: Test with (\x. \y. y) omega to verify normal finds NF, applicative diverges

Phase 5: Divergence Detection (Day 8)

Milestone: Detect and report infinite loops.

Implement term hashing or comparison
Track seen terms with step numbers
Detect cycles and report indices
Implement step limit fallback
Test with omega and variations

Hint Layer 1: Simplest: keep a list of seen terms, check membership Hint Layer 2: More efficient: use a Set or Map with term as key Hint Layer 3: Alpha-equivalence: convert to de Bruijn for comparison Hint Layer 4: Report the cycle: “Term at step 5 equals term at step 1”

Phase 6: Visualization and Formatting (Days 9-10)

Milestone: Pretty output with highlighted redexes.

Implement formatTermWithHighlight :: Term -> Path -> String
Implement formatReductionTrace :: [ReductionStep] -> String
Add color codes for terminal (optional)
Implement comparison mode display
Add AST tree display

Hint Layer 1: Highlight by wrapping the redex in brackets: [redex] Hint Layer 2: Include position info: @ root.left.right Hint Layer 3: For tree display, use ASCII art with / and \ connectors Hint Layer 4: Consider using a library like brick for terminal UI

Phase 7: Interactive REPL (Days 11-14)

Milestone: Full interactive visualizer.

Implement command parsing
Implement state management (current term, history, strategy)
Add undo (:back command)
Implement comparison mode
Add help and error handling
Polish and test

Hint Layer 1: Use haskeline for readline support Hint Layer 2: State is a record; commands return new state Hint Layer 3: For undo, keep history as a list; pop to go back Hint Layer 4: Comparison mode: run both strategies independently, interleave output

Testing Strategy

Unit Tests

Path Tests:

testPathPrefix = isPrefix Here (GoLeft Here) `shouldBe` True
testPathNotPrefix = isPrefix (GoLeft Here) (GoRight Here) `shouldBe` False
testGetSubterm = getSubterm (GoLeft Here) (App f a) `shouldBe` Just f

Redex Finding Tests:

testFindRedexSimple =
  findRedexes (App (Lam "x" (Var "x")) (Var "y"))
  `shouldHaveLength` 1

testFindRedexNested =
  let term = App (App (Lam "x" (Lam "y" (Var "x")))
                       (App (Lam "z" (Var "z")) (Var "a")))
                 (Var "b")
  in findRedexes term `shouldHaveLength` 2

testClassifyOutermost =
  let redexes = findRedexes nestedTerm
  in filter redexIsOutermost redexes `shouldHaveLength` 1

Strategy Tests:

testNormalOrderFindsNF =
  let omega = App (Lam "x" (App (Var "x") (Var "x")))
                  (Lam "x" (App (Var "x") (Var "x")))
      term = App (Lam "x" (Lam "y" (Var "y"))) omega
  in case runStrategy NormalOrder 100 term of
       NormalForm t _ -> t `shouldBe` Lam "y" (Var "y")
       _ -> expectationFailure "Should find normal form"

testApplicativeOrderDiverges =
  let term = ... -- same as above
  in case runStrategy ApplicativeOrder 100 term of
       Diverges _ _ -> pure ()
       StepLimitReached _ _ -> pure ()  -- also acceptable
       NormalForm _ _ -> expectationFailure "Should diverge"

Divergence Detection Tests:

testDetectsOmegaLoop =
  let omega = App (Lam "x" (App (Var "x") (Var "x")))
                  (Lam "x" (App (Var "x") (Var "x")))
  in case runStrategy NormalOrder 10 omega of
       Diverges _ (Just (1, 2)) -> pure ()  -- Found cycle
       Diverges _ Nothing -> pure ()  -- Hit limit, acceptable
       _ -> expectationFailure "Should detect divergence"

Property-Based Tests

-- Church-Rosser: both strategies reach same normal form (if they terminate)
prop_churchRosser :: Term -> Property
prop_churchRosser term =
  case (runStrategy NormalOrder 1000 term,
        runStrategy ApplicativeOrder 1000 term) of
    (NormalForm n1 _, NormalForm n2 _) -> alphaEquiv n1 n2
    _ -> True  -- Divergence is okay

-- Step count: normal order never takes more steps than applicative (to NF)
prop_normalOrderOptimal :: Term -> Property
prop_normalOrderOptimal term =
  case (runStrategy NormalOrder 1000 term,
        runStrategy ApplicativeOrder 1000 term) of
    (NormalForm _ h1, NormalForm _ h2) -> length h1 <= length h2
    _ -> True

Integration Tests

testInteractiveSession = do
  state <- initState "(\\ x. x) y"
  state' <- runCommand state ":step"
  currentTerm state' `shouldBe` Var "y"

testComparisonMode = do
  output <- runCommand initState ":compare (\\x. \\y. y) omega"
  output `shouldContain` "Normal Order: \\y. y"
  output `shouldContain` "Applicative Order: DIVERGES"

Common Pitfalls

1. Wrong Leftmost/Outermost Classification

Symptom: Normal order reduces the wrong redex

Cause: Confusing “leftmost” in tree structure vs. string representation

Fix: Leftmost means “appearing first in a left-to-right pre-order traversal.” Implement path comparison correctly.

2. Missing Redexes in Nested Lambdas

Symptom: Redexes inside lambda bodies not found

Cause: Not traversing into Lam bodies

Fix: findRedexes (Lam x body) should recurse into body with GoBody path

3. Divergence Detection False Positives

Symptom: Reports divergence for terms that reach normal form

Cause: Comparing terms structurally when they are alpha-equivalent

Fix: Normalize to de Bruijn indices before comparison, or use alpha-aware equality

4. History Grows Without Bound

Symptom: Memory exhaustion on long reductions

Cause: Keeping all history forever

Fix: Limit history size; use a bounded queue or ring buffer

5. Visualization Misaligns

Symptom: Highlighted redex does not match actual redex

Cause: Pretty printer and redex finder disagree on term structure

Fix: Use the same traversal logic; highlight by path, not by string matching

6. Applicative Order Goes Too Deep

Symptom: Applicative order reduces inside lambda bodies when it should not (for CBV)

Cause: Confusing applicative order (full reduction) with call-by-value (WHNF)

Fix: Call-by-value stops at lambda; applicative order continues. Implement separately.

Extensions and Challenges

Extension 1: Web Interface

Build a web UI using Elm, PureScript, or Haskell with GHCJS:

Clickable redexes
Animated substitution
Side-by-side strategy comparison
Shareable URLs for terms

Extension 2: Parallel Reduction

Implement parallel reduction (reducing multiple non-overlapping redexes at once):

Identify independent redexes
Show parallel reduction steps
Compare efficiency with sequential

Extension 3: Reduction Graphs

Instead of showing linear traces, build and visualize the reduction graph:

Nodes are terms
Edges are reduction steps
Multiple paths visible simultaneously
Show where paths merge (Church-Rosser)

Extension 4: Cost Metrics

Add metrics to reduction:

Count beta-reductions
Estimate memory (size of terms)
Time complexity analysis
Compare strategy efficiency empirically

Extension 5: De Bruijn Mode

Add a toggle to show terms in de Bruijn representation:

Simpler comparison
No alpha-renaming visible
Different aesthetic

Extension 6: Custom Strategy Builder

Let users define their own reduction strategies:

Priority rules for redex selection
Hybrid strategies
Randomized reduction

Real-World Connections

GHC Core and STG

GHC (Glasgow Haskell Compiler) uses intermediate languages closely related to lambda calculus:

Core: A typed lambda calculus, reduced by inlining and simplification
STG: Spineless Tagless G-machine, explicit about evaluation

Understanding reduction strategies helps understand how GHC optimizes code.

Call-by-Need in Haskell

Haskell’s evaluation is call-by-need: normal order + memoization. When you write:

let x = expensiveComputation in x + x

Haskell evaluates expensiveComputation once, not twice. Your visualizer can demonstrate the difference.

Debugging Lazy Evaluation

Haskell’s laziness can cause space leaks. Understanding reduction order helps debug them. Tools like ghc-vis visualize Haskell’s runtime reduction similarly to your visualizer.

Term Rewriting Systems

Lambda calculus reduction is a special case of term rewriting. Your visualizer techniques apply to:

Algebraic specification languages (Maude, OBJ)
Theorem provers (rewriting tactics)
Domain-specific languages with custom reduction rules

Partial Evaluation

Partial evaluators reduce programs given partial inputs. The visualization techniques you build help understand:

What parts of a program can be reduced at compile time
How specialization works

Interview Questions

After completing this project, you should be able to answer:

What is a redex? Give an example with multiple redexes and identify which is outermost.
Explain the difference between normal order and applicative order reduction. When does the choice matter for termination?
State the Church-Rosser theorem. What does it guarantee about normal forms?
Give an example of a term that has a normal form under normal order but diverges under applicative order. Explain why.
How would you detect that a lambda term is diverging during reduction?
How does Haskell’s evaluation strategy relate to normal order? What optimization does call-by-need add?
Explain why normal order is “optimal” according to the Standardization Theorem.

Self-Assessment Checklist

You have mastered this project when you can:

Resources

Primary References

Resource	Use For	Specific Chapters
“Types and Programming Languages” by Pierce	Reduction strategies, Church-Rosser	Chapters 5, 12
“Lambda Calculus and Combinators” by Hindley & Seldin	Standardization theorem	Chapter 11
“Purely Functional Data Structures” by Okasaki	Efficient history (for undo)	Chapter 5

Papers

Paper	Description
“The Lambda Calculus: Its Syntax and Semantics” by Barendregt	The definitive reference
“Lazy Evaluation and Strictness Analysis”	How strategies affect performance
“Call-by-Name, Call-by-Value, and the Lambda Calculus” by Plotkin	Classic paper on strategies

Tools and Visualizers

Tool	Description
Lambda Calculator	Compare with your visualizer
Lambda Viewer	See different visualization approaches
PLT Redex	Racket-based semantics modeling

Videos

Video	Description
“Lambda Calculus Reduction” by Computerphile	Visual introduction
“Lazy Evaluation” by NICTA	How Haskell evaluates
“GHC Core” talks by Simon Peyton Jones	Real-world application

Libraries for Implementation

Library	Use For
`haskeline`	REPL line editing
`brick`	Terminal UI
`ansi-terminal`	Colored output
`containers`	Efficient Map/Set for term tracking

“The Church-Rosser theorem assures us that we may make our computational choices freely - all roads that reach an answer reach the same answer.” - J. Roger Hindley