SKY Multiway Tree
Watch computation branch into a multiway tree. Every possible reduction path is explored simultaneously, and topos-theoretic gluing identifies when different paths converge to the same result. The Y combinator spirals infinitely, revealing why fixed points require non-termination.
3D Multiway View
Interactive
Reduction Flow
Lean 4 Verified
Each glowing sphere represents a combinator term. The root node is the initial expression; children are the results of applying reduction rules.
The S combinator: S x y z = (x z)(y z). It distributes the third argument to both inner terms.
The K combinator: K x y = x. It discards its second argument entirely.
The Y combinator: Y f = f (Y f). It unfolds infinitely, shown as a descending spiral.
When different reduction paths reach the same normal form, they are identified by the Grothendieck closure operator. The green connection shows this topos-theoretic gluing.
The tree grows downward. Each level represents one reduction step. Non-deterministic choices create multiple branches at each level.
Sieves as Heyting Algebras
The key insight from topos theory: sieves on a category form a complete Heyting algebra. When we view SKY terms as a thin category (via reachability), the Grothendieck closure operator becomes a nucleus that identifies equivalent computational states.
This isn't just mathematical elegance - it's a machine-checked proof that multiway branching respects logical structure. The Lean formalization proves that closed sieves inherit Heyting algebra structure, meaning we can reason about equivalence classes of computations using intuitionistic logic.