Lean formalization of the untyped lambda calculus using De Bruijn indices
- De Bruijn representation of lambda terms
- λβ equivalence relation
- Basic combinators, boolean encodings, and Church numerals
- Proof of the first recursion theorem proven with both Y and θ combinators
- Lambda calculus self-encoder and interpreter with injectivity and correctness proofs
| File | Contents |
|---|---|
VLambda/DBTerm.lean |
Syntax of lambda terms (DBTerm) and λβ equivalence relation (LB_eq) |
VLambda/ShiftLemmas.lean |
Useful lemmas about shift and shift_down (used for β-substitution) |
VLambda/Comb.lean |
Combinators |
VLambda/Church.lean |
Church numerals |
VLambda/RecThm.lean |
First recursion theorem |
VLambda/SelfEval.lean |
Self-encoding and evaluation |