A Lean 4 formalization of a small combinatory calculus, its observational quotient, and structure-preserving morphisms from closed dialects (lambda, TRS, bytecode, HF sets) into that quotient.
Open Dialect Explorer →The substrate is the term algebra ITerm with operators norm, konst, comp, and dup, plus application. Reduction laws include identity \(\text{norm} \cdot x \to x\) and constant \(\text{konst} \cdot x \cdot y \to x\). BasisCompleteness.lean derives the distributive combinator \(S\) from this basis and checks its reduction behaviour.
The Invariant Layer is the quotient of the ISK fragment by operational joinability (OperEq). Two terms are identified when they join under multi-step reduction. This is the observational equivalence used throughout the stack; terminality is stated relative to a fixed category of Kernel views, not as a claim about all models of computation.
Lambda calculus, term rewriting, stack bytecode, and HF-set interpretations are modelled as Kernel structures: a carrier, a view map, observational equivalence, and a decode back to the calculus. morphism_uniqueness states that morphisms into the canonical ISAR presentation are unique up to OperEq — terminality in that category.
The informal word Plex nods to Douglas T. Ross's 1961 plex tract (data plus topology pointers). Here it is only historical colour: the formal objects are ITerm, OperEq, and Kernel.
In Futamura.lean, we formally define substitution (subst) and partial evaluation (specialize) over variables and terms, and prove the correctness of the three Futamura projections:
Given a program \(t\), a static environment mapping static inputs, and a dynamic environment mapping dynamic inputs, specialization produces a new program. We prove (futamura_first) that running the specialized program with the dynamic inputs yields the same result as running the original program with the complete environment:
$$\text{subst}(\text{specialize}(t, env_{\text{static}}), env_{\text{dynamic}}) = \text{subst}(t, env)$$
If we specialize a correct partial evaluator with respect to an interpreter, we generate a compiler. We prove (futamura_second) that applying this compiler to a program source yields a specialized executable program that behaves identically to the interpreter running that program:
$$\text{specialize}(\text{specializer}, \text{interpreter}) = \text{compiler}$$
If we specialize the partial evaluator with respect to itself, we generate a compiler generator (often called cogen). We prove (futamura_third) that applying cogen to any interpreter yields a compiler for that interpreter:
$$\text{specialize}(\text{specializer}, \text{specializer}) = \text{cogen}$$
Verified dialect views share the same encode → substrate → quotient → decode shape:
| Aspect | Operational / quotient side | Syntactic rewrite side |
|---|---|---|
| Primitive structure | ITerm, reduction, OperEq classes |
Terms, rules, graphs under a chosen view |
| Evaluation dynamics | Joinability / complete development | Symbolic rewrite steps |
| Normal form | Unique NF when it exists (isar_fragment_unique_normal_forms) |
No applicable rewrite rule |
| Confluence | Parallel reduction / Tait–Martin-Löf development | Critical-pair style reasoning on the fragment |
| Terminality | Terminal object in the stated Kernel category |
Not a property of “systems in general” |
The IK-fragment is in the same ballpark as untyped combinatory logic / lambda: homogeneous code-data, SKI embeddable, confluent on the verified fragment. Full ISAR adds an explicit observational quotient and a category of dialect views with a uniqueness theorem for morphisms into that quotient. This does not claim that lambda calculus lacks models, quotients, or universal encodings — those are classical (Böhm trees, \(D_\infty\), Morris congruence, Abramsky applicative bisimilarity, Church encodings, SECD/Krivine, TRS translations).
Combinatory core with confluence and unique normal forms on the encoded fragment; lambda compiles in with simulation theorems.
Given the Kernel interface, morphisms into ISAR_Kernel are unique up to OperEq (morphism_uniqueness). Strength of the claim tracks strength of that interface.
Verification uses Lean 4 (CIC). The object language may diverge; Lean reasons over inductive step relations rather than executing unbounded reductions. Terminality is uniqueness of morphisms into a chosen presentation up to observational equivalence — standard category theory — and does not by itself imply that every matrix model of a theory is isomorphic to every other.
Below is the verified code index. Click any file to view its proof script on GitHub:
| Lean / doc file | Role in the stack | Primary verified theorem |
|---|---|---|
| BasisCompleteness.lean | Completeness of structural carriers | completeness_of_basis (derives \(S\) from \(I, K, W, C, B\)) |
| InvariantLayer.lean | Formal operational quotient space | Quotient Setoid formulation and canonical representative equivalence |
| ISAR.lean | Symbolic calculus rewriting | Confluence, determinism, and IStepBasis simulation |
| KernelCategory.lean | Universal category of semantic views | morphism_uniqueness (proving terminality of ISAR Kernel) |
| LambdaFragment.lean | Lambda compiler adequacy | Compositional homomorphic compilation and Closed Term Separation |
| ZFCInterpretation.lean | Hereditarily Finite Set view interpreter | Relative interpretation of set theory constructors onto ISAR |
| TRSView.lean | Term Rewriting System isomorphism | Isomorphism between symbolic tree terms and the operational substrate |
| BytecodeView.lean | Bytecode execution view | Compilation and execution equivalence over VM stack operations |
| IotaView.lean | Barker Iota view | Isomorphism between Barker iota trees and the operational substrate |
| Futamura.lean | Futamura projections verification | First Futamura projection proof (specializer soundness) |
| ISARMatrices.lean | Geometric matrix gauge transformations | Similarity matrix conjugation \(P \cdot K_1 \cdot P^{-1} = K_2\) |
| ReverseRosetta.lean | Operational boundary limits | closure_preserved_under_reachability (closed) & open_requires_anchor |
| applications.md | Substrate and partial evaluation documentation | Core definitions and correspondence table |