Nominal Inversion in Weakly Positive Subtyping with Intersection Types

This document describes a problem we are having in Path-sensitive weakly positive subtyping proof framework

Document: Summary of Nominal Inversion & Weakly Positive Subtyping (Updated)

1. Problem Context

The goal is to formalize an algorithmic subtyping system (wp / ISub) for iso-recursive types with intersections. To solve the “path divergence” problem in intersections, the wp Δ1 Δ2 A B relation introduces sets (${\Delta }_1,{\Delta }_2$) to track variables. The current roadblock is proving the nominal_inversion lemma, a critical theorem required to link the declarative nominal unfolding rule (Sub) to the algorithmic weakly positive restriction (wp).

The lemma statement is:

Theorem nominal_inversion: forall A B C D X m,
  Sub (subst_tt X (typ_rcd X C) A) (subst_tt X (typ_rcd X D) B) ->
  X `notin` fl_tt A \u fl_tt B ->
  Sub (choose m C D) (choose m D C) ->
  (Sub (choose m D C) (choose m C D) \/ 
    wp (choose m {{X}} {}) (choose m {} {{X}}) A B).

2. The Discussion & The Question

The proof consistently gets stuck in the Coq mechanization at the recursive (mu) cases. We analyzed a series of lemmas to determine if the Coq proof lacked the right induction hypothesis, or if the lemma statements themselves were mathematically false. The core question resolved was: Is there an expressive gap between the declarative Sub rule and the algorithmic wp system that structurally prevents the inversion lemma from holding?

3. The Concrete Counterexample (Why Inversion Fails)

The answer is yes. The following counterexample demonstrates why nominal_inversion is false under the current definitions.

Let $m=\text{Pos}$. Let $C=\text{nat}$ and $D=\text{top}$. (Note: $C\le D$ holds, but $D\le C$ fails). Consider the types $A$ and $B$, which contain an inner recursive binder $Z$:

• $A_0=(\text{top}\to \text{top})\wedge (X\to \text{top})\wedge (Z\to Z)$
• $B_0=(\text{top}\to \text{top})\wedge (\text{top}\to \text{top})\wedge (Z\to Z)$
• $A=\mu Z.A_0\text{and}B=\mu Z.B_0$

Step A: The Premises Hold We substitute $X\mapsto \{X:\text{nat}\}$ in $A$ and $X\mapsto \{X:\text{top}\}$ in $B$. Sub A[C] B[D] succeeds effortlessly: Sub_mu opens the types with a nominal label $Y$. The LHS $\{X:\text{nat}\}\to \text{top}$ branch is easily covered by the RHS $\text{top}\to \text{top}$ branch because $\text{top}\ge \{X:\text{nat}\}$. The inner contravariant branch $Z\to Z$ becomes $Y\to Y$, which matches itself purely via structural reflexivity (Sub_refl).

Step B: The Conclusion Fails The theorem demands either $D\le C$ (False) OR wp {X} {} A B. The wp derivation inherently crashes:

1. We cannot use wp_rec_eqv because $X$ is actively tracked (${\Delta }_1=\{X\}$) and $X\in \text{fv\_tt}(A_0)$.
2. We are forced to use wp_rec, which blindly adds the inner binder $Z$ to ${\Delta }_1$, requiring wp {X, Z} {} A_0 B_0.
3. When checking the $Z\to Z$ branch, wp_arrow flips polarities, asking for wp {} {X, Z} Z Z.
4. wp_vary requires $Z\notin {\Delta }_2$. But $Z\in \{X,Z\}$. The derivation fails.

4. The False Fix: Why We Cannot Just Drop the FV Condition

To fix the crash, one might propose dropping the syntactic free variable condition ($\forall \alpha \in \Delta ,\alpha \notin \text{fv}(T)$) from the wp_rec_eqv rule. This is mathematically unsound.

As proven by the user’s derivation, dropping the FV condition causes the algorithm to erroneously accept: $\mu a.\text{Top}\to (\mu b.b\to a)\le \mu a.\text{Int}\to (\mu b.b\to a)$

• Under Declarative Sub: This is correctly rejected. Unfolding the inner binder $b$ places it contravariantly ($b\to a$). When subtyping checks this arrow, the domain check forces a reverse check on the substituted $a$, ultimately asking to prove $\text{Top}\le \text{Int}$, which fails.
• Under a naively relaxed wp (no FV check): The algorithm would just verify that the inner $b\to a$ matches $b\to a$ structurally. Because $b$ is untracked, it matches itself. Because $a$ is tracked positively, it matches itself. The algorithm completely misses that $b$‘s contravariance acts as a multiplier that drags $a$ through a nested polarity flip.

5. The Core Theoretical Implication: Syntactic vs. Semantic Tension

This exposes the fundamental tension in algorithmic iso-recursive subtyping with intersections:

1. Soundness demands the FV check: You must statically ban tracked outer variables ($X$) from sitting inside nested contravariant recursive binders, otherwise the polarity sets ($\Delta$) fail to predict the nested reverse-checks.
2. Completeness (Intersections) breaks the FV check: Syntactic FV checks ($\alpha \notin \text{fv}(T)$) look at the whole type tree. But intersection types can “mask” or discard dead branches (like the $X\to \text{Top}$ branch in our counterexample). The syntactic check crashes the algorithm over a variable $X$ that nominal Sub safely discards.

Conclusion: The algorithmic wp system is caught in a trap. If it relies on syntactic $fv(T)$, it is sound but incomplete w.r.t nominal Sub (making the inversion lemma unprovable). If it drops $fv(T)$, it becomes complete but unsound.

---

Summary of the Path Forward: The concept of “Semantically Active Free Variables” is simply acknowledging that subtyping with intersections is a lossy operation. To fix the Coq proof, you must shift your strict polarity checks away from the raw syntax of the type, and attach them specifically to the parts of the syntax that actually survive the intersection subtyping rules.