6  untyped-comb and DAG Reduction

6.1 The Combinatory Architecture

The untyped-comb module handles the transformation of verified logic into an executable format, acting as the critical bridge to the WGPU Physics backend. The system structurally translates the Abstract Syntax Tree (AST) away from dependent types into a flat, variable-free combinatory representation.

#| label: comb-inductive-type

inductive Comb
  | K : Comb -- Schönfinkel's C (Konstanz) / Erasure
  | S : Comb -- Fusion / Duplication
  | I : Comb -- Identity
  | U : Comb -- Schönfinkel's Unverträglichkeit (NAND logic for SPE integration)
  | var : String -> Comb
  | app : Comb -> Comb -> Comb
  | t_inject : Comb -> Comb -- The geometric type-shifting endofunctor
  | lazy_thunk : Comb -> Comb -- Explicit Call-by-Need thunk for impredicative boundaries
  | terminal : String -> Comb -- Stabilized terminal state

This compilation model replaces hierarchical memory structures with precise routing combinators. Variables and substitution environments are removed from the operational layer, replaced entirely by the structural fusion and duplication rules dictated by the \(S\) and \(K\) execution nodes.

---

6.2 Directed Acyclic Translation & Flattening

To safely process highly entangled combinator streams on bare-metal hardware (like Interaction Nets with 32-bit pointers), the execution engine translates operations into a Directed Acyclic Graph (DAG).

The compiler executes an \(O(V+E)\) topological sort utilizing Kosaraju’s algorithm. By identifying 0-weight semantic cycles (Strongly Connected Components), the engine safely projects non-well-founded referential loops natively into flat structures, neutralizing exponential memory blowup prior to execution.

---

6.3 Topologically-Guided Lazy Reduction

Because the nf-sketches architecture evaluates an unstratified universe natively, it utilizes specific mechanical safeguards to manage execution limits structurally:

6.3.1 Dynamic T-Weaking Pipeline

The integer distances generated by the NfValidate static matrix algorithmically inform where structural friction occurs. The engine synthesizes dynamic bounds through the buildDynamicDistanceMap:

#| label: build-dynamic-distance
#| eval: false

def buildDynamicDistanceMap (w : StratificationWitness) (scope : Nat) : Comb → Option Int
  | Comb.var s =>
      if s.startsWith "_" then
        let n := (s.drop 1).toNat!
        some (getWeightFromWitness w scope (Var.bound n))
      else
        some (getWeightFromWitness w scope (Var.free s))
  | Comb.t_inject c =>
      match buildDynamicDistanceMap w scope c with
      | some w_c => some (w_c + 1)
      | none => none

By extracting the verified scope constraints (StratificationWitness), the compiler utilizes algorithmicTWeaking to natively inject Comb.t_inject wrappers into the graph exactly where bounds are violated. This geometric self-regulation ensures that unstratified arrays stabilize natively without an infinite type hierarchy.

6.3.2 MCM Bounds and Terminal States

The Minimum Cycle Mean (MCM) calculates dynamic operational limits across semantic boundaries. When evaluating saturated subsets (e.g. \(V \in V\)), the engine tracks the explicit recursion friction via explicit lazy_thunk states. When the distance map reaches a negative convergence limit, the execution is mathematically intercepted and frozen as a Comb.terminal "K_ITERATION_HALT".

Once formatted through this pipeline, the AST is perfectly pruned for WGPU parallel reduction loops where atomic Compare-And-Swap (CAS) instructions handle graph rewiring completely lock-free.