How deep must target splitting go?
Status: open (leaning resolved)
For Deep Target Splitting, does the cover target need to split only arrow codomains, or recursively through nested arrows / records / μ as well?
Current understanding
- Arrow-splitting alone fixes the surface incompleteness witness.
- μ-splitting is also genuinely necessary when a mixed
a-occurrence is hidden under a nested μ (witness:μa.μb.(b→a) & (b→(a→Nat))). - General principle: the cover target should follow the full declarative split structure, so every piece has a determinate single polarity.
What would settle it
A precise statement of the split-normal form + a completeness proof against the declarative system over all type formers.