Exercise Solutions (Hidden)

Exercise Solutions (Hidden)#

Each solution is inside a dropdown so you can reveal it when needed. The code blocks are runnable snippets (copy into a code cell if you want to execute them directly in this notebook).

Most snippets assume the corresponding chapter’s definitions are already in scope (e.g., Var, Lam, add, mul, Z). If you want a fully standalone run, copy the setup cells from that chapter first.

Reading guide

A line marked Formal proof is a general mathematical argument.
A line marked Finite check is only computational validation on a bounded range.

Exercise 1 (Lambda Basics)#

Exercise 2 (Substitution and Reduction)#

Solution (general proof + code)

Context We use capture-avoiding substitution and beta-reduction.

Substitution rules (capture-avoiding)

\(x[x:=u]=u\)
\(y[x:=u]=y\), for \(y\neq x\)
\((t\,u)[x:=v]=t[x:=v]\,u[x:=v]\)
\((\lambda y.\,t)[x:=v]=\lambda y.\,t\) if \(y=x\)
\((\lambda y.\,t)[x:=v]=\lambda y.\,t[x:=v]\) if \(y\neq x\) and \(y\notin FV(v)\)
If \(y\in FV(v)\), alpha-rename first to avoid capture.

Beta-reduction of \((\lambda x.\,x)\,((\lambda y.\,y)\,z)\)

\((\lambda x.\,x)\,((\lambda y.\,y)\,z)\)
\(\to ((\lambda y.\,y)\,z)\)
\(\to z\)

Normal-order vs applicative-order Let \(\Omega=(\lambda x.\,x\,x)(\lambda x.\,x\,x)\). Then:

Normal order: \((\lambda x.\,y)\,\Omega \to y\), terminates.
Applicative order: tries to reduce \(\Omega\) first, which diverges.

Why binder renaming is needed in subst(\lambda y. x, x := y) The replacement term \(y\) has free variable \(y\). If we substitute into \(\lambda y.\,x\) without renaming, we’d get \(\lambda y.\,y\) where that \(y\) is now bound. Correct capture avoidance renames the binder first:

\[ (\lambda y.\,x)[x:=y] \equiv (\lambda y0.\,x)[x:=y] = \lambda y0.\,y. \]

Weak-head vs full normalization Full normalization reduces under lambdas, so:

\[\lambda x. ((\lambda y. y)\,x) \to \lambda x. x.\]

Weak-head normalization stops at the outer lambda and leaves the body unreduced.

Code (using the Chapter 2 reducer)

# Reduce to z
z = Var("z")
term = App(Lam("x", Var("x")), App(Lam("y", Var("y")), z))
normalize(beta_step_normal, term)  # z

# Normalizes under normal order but diverges under applicative order
omega = App(Lam("x", App(Var("x"), Var("x"))), Lam("x", App(Var("x"), Var("x"))))
term = App(Lam("x", Var("y")), omega)

normalize(beta_step_normal, term)       # y
normalize(beta_step_applicative, term)  # diverges

# Substitution that requires alpha-renaming to avoid capture
term = Lam("y", Var("x"))
out = subst(term, "x", Var("y"))
show(out)  # (lambda y0. y)

# Weak-head normal form: do not reduce under Lam
def beta_step_normal_weak(t: Term):
    if is_redex(t):
        return subst(t.fn.body, t.fn.param, t.arg), True
    if isinstance(t, App):
        new_fn, changed = beta_step_normal_weak(t.fn)
        if changed:
            return App(new_fn, t.arg), True
        new_arg, changed = beta_step_normal_weak(t.arg)
        if changed:
            return App(t.fn, new_arg), True
        return t, False
    # Crucial: do not descend into Lam
    return t, False

t = Lam("x", App(Lam("y", Var("y")), Var("x")))
show(normalize(beta_step_normal, t))       # (lambda x. x)
show(normalize(beta_step_normal_weak, t))  # (lambda x. ((lambda y. y) x))

Exercise 3 (Church Booleans)#

Exercise 4 (Propositional Logic)#

Exercise 5 (Church Numerals)#

Expanded step-by-step example (symbolic rewrite) We document the associativity step for add using the symbolic lambda-calculus engine from Chapter 8.

Goal

\[ \mathrm{add}(\mathrm{add}\;a\;b)(S\,c) = \mathrm{add}\;a\;(\mathrm{add}\;b\;(S\,c)). \]

Step 1 (Definition and Lemma 1)

\[ \mathrm{add}(\mathrm{add}\;a\;b)(S\,c) = S(\mathrm{add}(\mathrm{add}\;a\;b)\;c). \]

Step 2 (Apply IH)

\[ S(\mathrm{add}(\mathrm{add}\;a\;b)\;c) = S(\mathrm{add}\;a\;(\mathrm{add}\;b\;c)). \]

Step 3 (Lemma 1, reversed)

\[ S(\mathrm{add}\;a\;(\mathrm{add}\;b\;c)) = \mathrm{add}\;a\;(\mathrm{add}\;b\;(S\,c)). \]

Exercise Solutions (Hidden)

Contents

Exercise Solutions (Hidden)#

Exercise 1 (Lambda Basics)#

Exercise 2 (Substitution and Reduction)#

Exercise 3 (Church Booleans)#

Exercise 4 (Propositional Logic)#

Exercise 5 (Church Numerals)#

Exercise 6 (Recursion and Fixpoints)#

Exercise 7 (Peano Arithmetic)#

Exercise 8 (Induction)#

Exercise 9 (Induction Proofs as Lambda Certificates)#

Exercise 10 (Tooling and Interactivity)#

Exercise 11 (Denotational Semantics)#

Exercise 12 (Normalization by Evaluation)#

Exercise 13 (Dependent Types)#

Exercise 14 (Sequent Calculus)#

Exercise 15 (Classical Logic via Control)#

Exercise 16 (System F)#

Exercise Solutions (Hidden)

Contents

Exercise Solutions (Hidden)#

Exercise 1 (Lambda Basics)#

Exercise 2 (Substitution and Reduction)#

Exercise 3 (Church Booleans)#

Exercise 4 (Propositional Logic)#

Exercise 5 (Church Numerals)#

Exercise 6 (Recursion and Fixpoints)#

Exercise 7 (Peano Arithmetic)#

Exercise 8 (Induction)#

8.1 Commutativity of addition

8.2 Associativity of addition

8.3 A symbolic beta-reduction trace

8.4 Multiplication by one

Exercise 9 (Induction Proofs as Lambda Certificates)#

9.1 Theorem 1: \(2 \mid n(n+1)\)

9.2 From Theorem 1 to \((2n+1)^2-1\) divisible by 8

9.3 Sum of odds equals a square

9.4 Symbolic rewrite trace

Exercise 10 (Tooling and Interactivity)#

10.1 Trace table for a simple reduction

10.2 Divergence via omega

10.3 REPL macros: I, K, and K I omega

10.4 Parsing variants of the identity

Exercise 11 (Denotational Semantics)#

11.1 More Kleene steps for factorial

11.2 A new functional: triangular numbers

11.3 Fuel experiments: terminating vs diverging

11.4 Denotation of (\x. x) (\y. y)

Exercise 12 (Normalization by Evaluation)#

12.1 Compose and normalize

12.2 Eta behavior

12.3 Reflect and reify directly

12.4 Ill-typed application

Exercise 13 (Dependent Types)#

13.1 Dependent identity for EqNat

13.2 Two witnesses for an existential (Σ-type)

13.3 Implication and conjunction as special cases

13.4 A failing dependent proof function

Exercise 14 (Sequent Calculus)#

14.1 K combinator shape: \(A \to (B \to A)\)

14.2 S combinator shape

14.3 Peirce’s law fails intuitionistically

14.4 Prove B from context h:A->B and a:A

Exercise 15 (Classical Logic via Control)#

15.1 Early exit from nested loops

15.2 first_satisfying

15.3 Peirce with concrete types

15.4 CPS evaluation with a nontrivial continuation

Exercise 16 (System F)#

16.1 const term and its type

16.2 Instantiate and apply

16.3 Incremental instantiation with unification

16.4 A type error

10.3 REPL macros: I, K, and `K I omega`

11.4 Denotation of `(\x. x) (\y. y)`

15.2 `first_satisfying`

16.1 `const` term and its type