SKY Combinator Multiway Formalization
A complete Lean 4 formalization of multiway reduction semantics for SKY combinators (S, K, Y), together with a topos-theoretic gluing layer where Grothendieck closure operators form nuclei on sieve lattices. The fixed points of this nucleus—the closed sieves—form a Heyting algebra that canonically identifies equivalent computational states.
Click to expand
Multiway graph showing branching reduction paths for SKY combinators. Each node represents a term state, edges are labeled with reduction rules (S, K, Y) and redex paths.
Technical Contributions
Complete Labeled Edge Enumeration
stepEdgesList enumerates all one-step reductions from a term, each labeled with a rule tag (S, K, or Y) and a redex path.stepEdgesList_complete proves every valid reduction appears in the enumeration.
Sieves Form a Frame
For any object X in a category C, Sieve X carries a complete lattice structure. We establish this is a frame (complete Heyting algebra) with implication S => T := U {U | U n S <= T}.
Grothendieck Closure as Nucleus
Given a Grothendieck topology J, the closure operator J.close is inflationary, idempotent, and preserves binary meets. The fixed points form a sublocale inheriting frame/Heyting algebra structure.
Fixed-Point Impossibility
Constructive proof that no total fixed-point operator Y : (a -> a) -> a can exist when a = Bool, since Bool.not has no fixed point. Y-combinator re-entry requires non-termination or partiality.
-Dno_sorry -DwarningAsError=true
Verified via mathics/wolframscript
Lean -> LambdaIR -> MiniC -> C
| LEAN DECLARATION | CONTENT |
|---|---|
| stepEdgesList_complete | Every one-step reduction enumerated with correct labeling |
| Sieve.instFrame | Sieves form a frame (complete Heyting algebra) |
| sieveNucleus | Grothendieck closure is a nucleus on the sieve frame |
| closedSieve_instHeyting | Closed sieves inherit Heyting algebra structure |
| heyting_trichotomy | Classification of Heyting behavior under nuclei |
| no_total_fixpoint_Bool | No total Y operator exists on Bool |
Topos-Theoretic Gluing
Multiway computation, as formalized in the Wolfram Physics Project, models non-deterministic rewriting where all possible reduction paths are explored simultaneously. The resulting multiway graph encodes the complete branching structure of computation from a given initial term.
A fundamental challenge is identifying when different paths lead to equivalent outcomes—a question naturally addressed by sheaf-theoretic gluing. We view the SKY term type as a thin category via the reachability preorder, then equip this with the dense Grothendieck topology J.
The closure operator J.close acts as a nucleus in the sense of locale theory. Its fixed points form a sublocale inheriting frame structure. In computational terms, this identifies terms that are mutually reachable—they collapse to the same "glued" entity.