Hermes Agent
6e2914b06e
Converted with pandoc 3.7 (markdown → org), all 17 files: - README, references, 15 tutorial units - Internal file links updated from .md to .org - Source code blocks (#+begin_src lean) preserved - Tables, math notation, links intact For the Emacs workflow.
92 lines
3.3 KiB
Org Mode
92 lines
3.3 KiB
Org Mode
* Unit 9 --- Substitution and α-Equivalence
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: unit-9-substitution-and-α-equivalence
|
||
:END:
|
||
*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]]
|
||
|
||
** Goals
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: goals
|
||
:END:
|
||
- Implement =subst= (substitution) for de Bruijn terms
|
||
- Implement =lift= (index shifting) --- the key operation that avoids capture
|
||
- Prove fundamental substitution lemmas
|
||
|
||
** Sources
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: sources
|
||
:END:
|
||
- syndikos/lean4-stlc =Syntax.lean= and =Reduction.lean=
|
||
- chenson2018/LeanScratch: https://github.com/chenson2018/LeanScratch
|
||
- PLFA Part 2: https://plfa.github.io/
|
||
|
||
** Exercises
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: exercises
|
||
:END:
|
||
#+begin_src lean
|
||
open DBTerm -- from Unit 8
|
||
|
||
-- 9.1 — Lift: shift all *free* variables above a cutoff by k
|
||
-- Lift is the engine that makes substitution work under binders.
|
||
-- When we go under a λ, existing de Bruijn indices need to shift by 1
|
||
-- because a new binder appears.
|
||
def lift (t : DBTerm) (cutoff k : Nat) : DBTerm :=
|
||
match t with
|
||
| var n => if n < cutoff then var n else var (n + k)
|
||
| lam body => lam (lift body (cutoff + 1) k)
|
||
| app f a => app (lift f cutoff k) (lift a cutoff k)
|
||
|
||
-- Verify: lifting the identity function
|
||
-- lift (λ. 0) 0 1 should produce λ. 0 (bound variables inside λ are untouched)
|
||
#eval lift idDB 0 1
|
||
|
||
-- 9.2 — Substitution: replace variable `idx` with `s` in term `t`
|
||
-- This is capture-avoiding substitution via de Bruijn arithmetic.
|
||
-- Under a λ, the target index shifts by 1 and the replacement gets lifted.
|
||
def subst (t : DBTerm) (idx : Nat) (s : DBTerm) : DBTerm :=
|
||
match t with
|
||
| var n =>
|
||
if n < idx then var n
|
||
else if n == idx then s -- found the variable to replace
|
||
else var (n - 1) -- shift remaining vars down
|
||
| lam body => lam (subst body (idx + 1) (lift s 0 1))
|
||
| app f a => app (subst f idx s) (subst a idx s)
|
||
|
||
-- Test: substitute λ. 0 for variable 0 in (λ. 0) -- should be identity
|
||
-- Actually: [0 ↦ λ.0] (λ. 0) — nothing changes (0 is bound)
|
||
#eval subst (lam (var 0)) 0 (lam (var 0))
|
||
|
||
-- 9.3 — Single-step β-reduction (preview of next unit)
|
||
-- β: (λ. t) s → subst t 0 s
|
||
def betaRedex : DBTerm := app (lam (var 0)) (lam (var 0)) -- (λx. x) (λy. y) → ...y...
|
||
|
||
-- Compute the result of one β step on this term
|
||
#eval subst (var 0) 0 (lam (var 0)) -- should be lam (var 0) (= λy. y)
|
||
|
||
-- 9.4 — Lemma: Substitution under a lambda
|
||
-- If we substitute for index 0 in a term that's already shifted,
|
||
-- the lift in the body handles the shift correctly.
|
||
-- Prove this property:
|
||
lemma subst_lift_commute (t s : DBTerm) (n : Nat) :
|
||
subst (lift t 0 1) (n+1) (lift s 0 1) = lift (subst t n s) 0 1 :=
|
||
by
|
||
sorry
|
||
|
||
-- This lemma is *critical* for proving preservation/type safety later.
|
||
-- It says that shifting before and after substitution agree.
|
||
#+end_src
|
||
|
||
*** Why this matters
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: why-this-matters
|
||
:END:
|
||
Substitution is the core operation of operational semantics. Doing it right
|
||
(no variable capture) is the hardest part of formalizing lambda calculi.
|
||
de Bruijn indices make capture impossible --- the arithmetic is mechanical.
|
||
The lemmas here are boilerplate you prove once, then reuse everywhere.
|
||
|
||
--------------
|
||
|
||
← [[file:08-syntax-representation.org][Previous: Unit 8]] · Next: [[file:10-small-step-semantics.org][Unit 10 --- Small-Step Semantics]]
|