Tony's Wiki

Deep Target Splitting

2 min read

Deep Target Splitting

The proposed fix (2026-05-31) for incompleteness of the algorithmic μ-rule: let the cover’s target decomposition push intersection-splits down into arrow codomains and under μ, following the declarative dist-mu structure, so every covered piece has a determinate single polarity.

Why it is safe: splitting is free for soundness

By dist-mu forward, reassembling split pieces is always sound. So you never need positivity to stay sound — positivity only decides whether a split preserves completeness. → make the split/keep-whole choice non-deterministic and let the cover search resolve it.

What splitting fixes

  • Arrow-splitting alone fixes the surface witness: normalize Int→(T1&T2) ≡ (Int→T1)&(Int→T2) → two homogeneous leaves:
    • Int→T1 covered by μ(Int→A1), covariant → CLIMB ✓
    • Int→T2 covered by μ(Int→A2), contravariant → RIGID ✓
  • μ-splitting is also genuinely necessary when the mixed a-occurrence is hidden under a nested μ. E.g. μa.μb.(b→a) & (b→(a→Nat)): outer a is covariant in b→a, contravariant in b→(a→Nat); the whole μb… is one cont-leaf, so the single entry carries one a-flavor — mixed-a failure recurs. Distributing the μb separates the polarities: (μb.b→a) & (μb.b→(a→Nat)).

The positivity problem dissolves

There is no stable syntactic positivity (μa.(a→Int)&(Top→Int) ≡ μa.Top→Int looks negative but splits fine; μa.(a→Int)&(Int→Int) genuinely doesn’t). Because splitting is always sound, you don’t classify — you search:

Design 1 (recommended): non-deterministic deep splitting. At each & under an arrow or μ, the cover may either split (dist-arrow ≡ / dist-mu forward) or keep the node whole (defer to the recursive ISub-μ check). Both branches sound; accept if any decomposition yields a valid cover.

  • Positive μ → split branch succeeds (homogeneous pieces).
  • Genuinely negative μ → keep-whole branch (RIGID, deferred inner check) fires, correct precisely because the negative μ wasn’t distributing anyway.
  • Decidable: splits are on strictly smaller types; μ-recursion decreases on the nominal-unfolding (msize) measure → finite search.

Open

How deep must target splitting go · A posteriori soundness condition for deep splitting

Distributivity Subtyping Laws · Split-Cover and Polarity Certificates · Incompleteness of the Algorithmic Mu-Rule · Size-Stratified Mutual Transitivity

Sources

2026-05-31

Graph View

Backlinks