10. Tooling and Interactivity

Working System

This chapter introduces interactive tooling built on the untyped lambda AST (Var, Lam, App) from lc_core.py. Use it to parse terms, inspect beta steps with diffs, and run a small REPL.

10. Tooling and Interactivity#

Goal. Build practical tooling around lambda-calculus terms so you can experiment quickly: parse terms, inspect beta steps with diffs, and interactively explore normal forms.

You will learn

  • How to parse lambda terms from strings and pretty-print them canonically

  • How to inspect normal-order beta-reduction step-by-step with highlighted diffs

  • How to use a small REPL for experimenting with definitions and reductions

  • What kinds of terms diverge (and how to detect this with a step limit)

  • How Thebe fits into the Jupyter Book workflow (optional)

Roadmap#

  1. Import the interactive helpers from lc_interactive.py.

  2. Use the trace table to visualize beta-reduction and what changes at each step.

  3. Use a ReductionSession widget to step forward/backward.

  4. Try the mini REPL and define basic combinators (I, K, S).

  5. (Optional) Enable Thebe for in-browser execution and understand its limitations.

from pathlib import Path
import sys

book_root = Path.cwd()
if not (book_root / "lc_interactive.py").exists():
    book_root = book_root.parent
if str(book_root) not in sys.path:
    sys.path.insert(0, str(book_root))

from IPython.display import HTML, display
from lc_interactive import (
    LambdaREPL,
    ReductionSession,
    format_trace_table,
    parse_lambda,
    pretty,
)

Interactive Reduction Visualizer (with Diffs)#

The visualizer computes a normal-order beta trace and highlights exactly what changed between each step.

expr = "((lambda x. x) ((lambda z. z) w))"

display(HTML(format_trace_table(expr, max_steps=10)))
stepbeforeafter
1(λx. x) ((λz. z) w)(λz. z) w
2(λz. z) ww

You can also inspect one step at a time with a mutable session object.

session = ReductionSession("((lambda x. lambda y. x) a) b", max_steps=10)

print(session.render_line())
print(session.next())
print(session.next())
print(session.prev())

display(HTML(session.render_diff_html()))

try:
    session.widget()
except Exception as err:
    print(f"Widget mode unavailable: {err}")

step 0/2: (λx. λy. x) a b
step 1/2: (λy. a) b
step 2/2: a
step 1/2: (λy. a) b
before (λx. λy. x) a b
after (λy. a) b
Widget mode unavailable: ipywidgets is required for widget mode

Mini REPL (Parsing + Pretty Printing)#

The REPL supports:

  • :let name = expr for bindings

  • :step expr for one beta step

  • :nf expr for normal form

  • plain expression input (same as :nf)

repl = LambdaREPL()

print(repl.eval_line(":help"))
print(repl.eval_line(":let id = lambda x. x"))
print(repl.eval_line(":let K = lambda x. lambda y. x"))
print(repl.eval_line(":step (K a) b"))
print(repl.eval_line(":nf (id (id q))"))
print(repl.eval_line(":env"))

Commands: :help, :env, :quit, :let name = expr, :step expr, :nf expr. Expressions use lambda syntax, e.g. (lambda x. x) y
id := λx. x
K := λx. λy. x
(λx. λy. x) a b -> (λy. a) b
q
K := λx. λy. x
id := λx. x

Parser + Pretty Printer#

Parser accepts lambda, \, and λ forms.

term = parse_lambda(r"\x. (x (lambda y. y))")
print(pretty(term))

λx. x (λy. y)

Note (Thebe)

The Jupyter Book config now enables Thebe (launch_buttons.thebe: true). For live Binder kernels, set repository.url in book/_config.yml to your GitHub repo URL.

Exercise

  1. Use format_trace_table to display a 6-step reduction trace for (\x. x) (\y. y) and interpret the diffs.

  2. Use ReductionSession on omega ((\x. x x) (\x. x x)). Show that it does not reach a normal form within 20 steps.

  3. In the REPL, define I := \x. x and K := \x. \y. x. Evaluate K I omega and explain why it reduces to I under normal order.

  4. Parse three syntactic variants of the identity (lambda, \, λ) and confirm pretty(parse_lambda(...)) prints the same canonical term. See solutions: Exercise 10 (Tooling and Interactivity)

Summary#

  • A parser + pretty-printer makes it easy to work with lambda terms without building ASTs by hand.

  • Normal-order beta-reduction can be explored as a step-by-step trace.

  • Diff highlighting is useful for spotting the redex and the substituted region.

  • Divergence shows up as traces that keep stepping; in practice, you work with a step limit.

  • Next: Chapter 11 explains denotational semantics, which gives a different viewpoint on divergence and recursion.

Contents