{"id":"86b558c9-253b-4bf5-a910-665ad537694a","arxiv_id":"2507.10482","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Subtyping with union, intersection, negation, and monotone type constructors under assumptions is decidable in O(n^2(1+m)) time, and every type has a quadratic-time computable minimal normal form.","lead":"The paper gives algorithms that decide subtyping in polynomial time for types built from unions, intersections, negations, and type constructors with covariant or contravariant parameters. A generalist reader might care because this could make type checkers in languages like Scala and TypeScript faster and more predictable while supporting expressive type features.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Normalization theorem rests on unproven completeness of β: Lemma 6.12 asserts OL+ 0/1 equivalence coincides with BL+ 0/1 for β-normalized terms, but its disjunctive case is dismissed 'by definition of β' without proof.","rationale":"The paper's central algorithmic claim (Theorem 4.1) is well-supported: the sequent calculus is sound and complete, the partial cut-elimination proof is claimed formalized in Rocq, and the Horn-clause reduction yields the stated O(n^2(1+|A|)) bound. The weaker point is Section 6's normalization theorem, exactly as the reader identified. I agree that Lemma 6.13 is the load-bearing step, but I would locate the true gap one level deeper: Lemma 6.12's unproven completeness. The step 'if ⊢CF+δ S_L,S_L then S∼OL+0' is actually valid by soundness; the fragile inference is the subsequent 'hence S∼BL+0' via Lemma 6.12. That lemma asserts a conservativity property for β-normalized terms that is not established and may fail because free ortholattices fail the orthomodular quasi-identity. The proof merely says 'by definition of β' for the disjunctive case, which is an assertion of completeness, not a proof. Since Section 6 is explicitly not fully formalized in Rocq, this gap is unverified. A concrete computational search or a formalization attempt would settle whether the concern lands. The reader's CONDITIONAL verdict is appropriate: the normalization claim should be accepted only after Lemma 6.12 is either proven or repaired.","tokens_in":26110,"tokens_out":28948,"duration_ms":295431,"concrete_test":"Enumerate β-normalized terms over two generators x,y (and their negations x′,y′) up to size, say, 12, using β's recursive definition. For each term, decide OL+-equivalence to 0/1 via the Section 5 Horn-clause algorithm, and BL+-equivalence to 0/1 via its BL+ analogue (the same algorithm without negation rules). If any S satisfies S∼OL+0 but not S∼BL+0, or S∼OL+1 but not S∼BL+1, then Lemma 6.12 is refuted and Theorem 6.15 is unsound. Alternatively, attempt a machine-checked proof of Lemma 6.12 in Rocq; if the proof cannot be completed, the normalization result lacks support.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 6.15 (quadratic-time minimal normalization for OL+) depends on Lemma 6.13 and its corollary, which in turn rely on Lemma 6.12. Lemma 6.12 claims that for terms in the range of β, S∼OL+0/1 iff S∼BL+0/1. Its proof's critical case says: 'If S=φ1∨φ2∼OL+1 then S=1 by definition of β.' This asserts the completeness of the β disjunction rule without a derivation. In ortholattices, φ1∨φ2=1 is equivalent to ¬φ1∧¬φ2=0, which does not generally imply δ(¬φ1)≤BL+φ1∨φ2, because δ(¬φ1)≤BL+φ1∨φ2 is a bounded-lattice inequality and free ortholattices are not orthomodular. If there exist β-normalized φ1,φ2 with φ1∨φ2∼OL+1 but neither δ(¬φ1)≤BL+φ1∨φ2 nor δ(¬φ2)≤BL+φ1∨φ2, then Lemma 6.12 fails. In that case the normalization map in Theorem 6.15 (δ, β, ζ, η) would not be well-defined on OL+ equivalence classes, and the minimal-canonical-form claim would collapse. The paper notes that not all results in Section 6 were formalized in Rocq, so this load-bearing inference is unverified.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes orthologic with monotone and antimonotone function symbols (OL+) as a foundation for subtyping with intersection, union, and negation types plus type constructors. It presents a sequent calculus SC+ for OL+ with axioms, proves soundness and completeness, and states a partial cut-elimination theorem (Theorem 4.7) that is formalized in Rocq. From cut elimination it derives an O(n^2(1+|A|)) decision procedure for the entailment problem by reducing proof search to propositional Horn clauses (Theorems 4.1 and 5.1). It then develops a normal-form theory for bounded lattices with monotone functions (BL+), gives a quadratic-time normalization algorithm for BL+ (Theorem 6.8), and extends it to OL+ through the maps delta, beta, zeta, and eta (Theorems 6.12, 6.13, and 6.15), claiming a unique minimal-size canonical form. The paper explicitly states that not all results in Section 6 are formalized in Rocq.","tokens_in":26426,"tokens_out":11375,"duration_ms":130580,"significance":"If the results hold, this is a valuable contribution: it offers a rare combination of expressiveness (negation, union/intersection, variance, and subtyping assumptions) with polynomial-time subtyping and normalization, and it ships a Rocq formalization of the central cut-elimination and completeness theorems, together with a clean reduction of proof search to Horn clauses. The paper is also careful about scope, explicitly acknowledging limitations such as the lack of support for recursive type definitions with parameters. The main weakness is that the normalization half of the paper rests on Lemma 6.12, whose proof contains an unsubstantiated step, and the paper notes that Section 6 was not fully formalized. Until that step is proved, the minimal-canonical-form claim should be treated as conditional, so the paper requires revision before the normalization contribution can be accepted.","major_comments":[{"comment":"The proof of the disjunctive case states, \"If S = phi1 \\/ phi2 ~OL+ 1 then S = 1 by definition of beta,\" but gives no derivation. For this step to be valid, phi1 \\/ phi2 ~OL+ 1 must imply that at least one of the two bounded-lattice inequalities checked by Algorithm 4 holds, namely delta(neg phi1) <=BL+ phi1 \\/ phi2 or delta(neg phi2) <=BL+ phi1 \\/ phi2. This implication is not a formal consequence of the ortholattice laws: in an ortholattice, phi1 \\/ phi2 = 1 is equivalent to neg phi1 /\\ neg phi2 = 0, and the latter does not by itself yield a bounded-lattice inequality in the free BL+, which has no complementation structure. The paper gives no argument that beta-normalized terms exclude possible failure cases. Because Lemma 6.12 is used in the Replace case of Lemma 6.13, this gap is load-bearing for the whole normalization development.","section":"Section 6.1, Lemma 6.12"},{"comment":"The Replace case of Lemma 6.13 contains the inference \"if |- CF+_delta S_L, S_L holds, then S ~OL+ 0; hence, by Lemma 6.12, S ~BL+ 0.\" This is the only bridge between OL+ equivalence and BL+ equivalence in the normalization construction, and it is used in Theorem 6.15 to conclude that beta(delta(S)) ~BL+ beta(delta(T)) whenever S ~OL+ T. That conclusion is exactly what makes eta(zeta(beta(delta(S)))) well-defined on OL+ equivalence classes. The paper notes that not all results in Section 6 were formalized in Rocq, so there is no machine-checked fallback for this step. If Lemma 6.12 cannot be repaired, Theorem 6.15 and the minimal-canonical-form claim collapse; as written, the proof is incomplete.","section":"Section 6, Lemma 6.13 and Theorem 6.15"},{"comment":"In the proof of Theorem 6.6, in the join case with S = x, the text says \"x <=BL+ T1 \\/ ... \\/ Tn and hence necessarily forall i, x <=BL+ Ti.\" This is incorrect as stated for free lattices: a generator below a join is below at least one joinand, not necessarily below all of them. The subsequent contradiction relies on the interaction between this step and the dual inequality T1 \\/ ... \\/ Tn <=BL+ x. If \"forall\" is a typo for \"exists,\" the argument needs to be restated carefully; if not, the proof of this case is invalid. Since Theorem 6.6 is the basis for the BL+ normal-form characterization and hence for Theorem 6.8, this needs correction.","section":"Section 6, Theorem 6.6"}],"minor_comments":[{"comment":"The abstract states the complexity as O(n^2(1+m)) while Theorem 4.1 states O(n^2(1+|A|)); the relationship between m and |A| (number of axioms vs. total size of axioms) should be clarified, and the missing closing parenthesis in Theorem 4.1 should be fixed.","section":"Abstract and Theorem 4.1"},{"comment":"The pseudocode uses a special value \"None\" in sequents, but the formal system of Section 4 has only two annotated terms and no None constructor; lines 20 and 24 should be explained or the pseudocode should be aligned with the formal system. Lines 32-33 say \"analogous\" and should be spelled out.","section":"Algorithm 1"},{"comment":"The sentence \"Define OL+ (resp BL+) as the algebraic signature of OL+ (resp BL+) extended with ...\" is grammatically unclear and should be rephrased.","section":"Section 6, Definition 6.9"},{"comment":"References [24] and [25] appear to be the same work (Henglein and Rehof, Constraint Automata and the Complexity of Recursive Subtype Entailment) and should be merged or distinguished.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The subtyping algorithm and its formalization appear to be strong; the main obstacle to acceptance is the unproved bridge between OL+ and BL+ in the normalization section. I would not reject the paper on the current evidence, but the authors must either provide a complete proof of Lemma 6.12 and its use in Lemma 6.13, or weaken the normalization claims accordingly."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The subtyping result is the real contribution and it looks solid. The O(n^2(1+m)) decision procedure for ortholattices with (anti)monotone function symbols extends the authors' earlier orthologic program in the natural direction, and the reduction to Horn clauses is a genuinely cleaner formulation than the memoization approach they cite. The partial cut elimination is stated to be formalized in Rocq, which is real evidence. The reader's conditional verdict is about right.\n\nWhere I part company with a fully positive read is Section 6. The normalization section is not machine-checked, and the paper openly says so. The stress-test note about Lemma 6.12 lands: the disjunctive case 'S = 1 by definition of beta' is doing more work than the paper accounts for. Lemma 6.13 then leans on that to equate OL+ and BL+ provability on the range of beta, and Theorem 6.15's quadratic minimal normal form depends on the whole chain. If that step fails, the minimal canonical form claim collapses, even if the procedure still gives a useful but non-minimal normal form. The paper would be stronger if this section were either formalized or honestly downgraded to a conjecture with minimality separated out.\n\nThe citation pattern is fine. The reliance on their own prior orthologic results is legitimate because those are formalized. No invented entities. The absence of a public artifact with a commit hash is a minor but real annoyance: the formalization claim is not verifiable from the paper alone.\n\nWho is this for: people building intersection/union/negation type systems who want polynomial algorithms, and verification researchers already using ortholattices. It deserves a serious referee. I would send it to a PL venue with a strong proof-theory PC and focus the referee on Section 6. The normalization weakness should not sink the subtyping contribution, but the minimal-form claim should not be accepted as-is.","headline":"Solid formally verified subtyping algorithm for ortholattices with constructors; the normalization half is a sketched proof that needs a careful referee before the minimal-form claim is trusted.","tokens_in":26957,"tokens_out":1501,"would_cite":true,"duration_ms":19526,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that subtyping with union, intersection, and negation types under assumptions is decidable in quadratic time and that every type has a quadratic-time normal form that is the smallest equivalent type.","keywords":["orthologic","ortholattices","subtyping","union types","intersection types","negation types","type constructors","normalization"],"falsifier":"Enumerate small terms in the range of the $\\beta$ reduction and check whether $\\vdash_{CF+_\\delta} S_L,S_L$ holds exactly when $S\\sim_{BL+}0$; a mismatch for any single term would refute Lemma 6.13 and hence Theorem 6.15.","tokens_in":25866,"feed_emoji":"🧩","tokens_out":9433,"duration_ms":94188,"temperature":0.7,"pith_summary":"The paper proposes using orthologic, the logic of ortholattices, as a foundation for type systems with intersection, union, and negation types, where negation behaves like a complement but distributivity is not assumed. Its central claim is that adding (anti)monotone type constructors and user-supplied subtyping assumptions preserves the efficient behavior of pure orthologic: subtyping entailment is decidable in $O(n^2(1+m))$ time, where $m$ is the number of assumptions, and every type can be normalized in quadratic time to the unique smallest equivalent type. If this holds, type checkers could gain complete and predictable reasoning about union and intersection types without the exponential blow-ups caused by distributivity in current languages.","feed_headline":"Quadratic-time subtyping for union, intersection, and negation types","feed_subtitle":"Subtype checks under assumptions and minimal type normalization, both in quadratic time.","key_machinery":"The load-bearing mechanism is partial cut elimination for the sequent calculus SC+ (Theorem 4.7), which removes all uses of transitivity except those involving axioms and gives a subformula property: any derivable inequality $S \\leq T$ has a proof built only from subterms of $S$, $T$, and the axioms. This turns proof search into a finite closure problem expressed as a set of Horn clauses with at most three literals each, solvable in linear time. The second mechanism is the syntactic characterization of minimal terms in BL+ (Theorem 6.6), which says a disjunction of normal terms is minimal exactly when its disjuncts form an antichain and no conjunct inside a disjunct is below the whole disjunction; the transformations $\\zeta$, $\\eta$, $\\delta$, and $\\beta$ enforce these conditions while preserving equivalence, and their composition yields the OL+ normal form.","core_discovery":"The paper establishes that the entailment problem for OL+, the class of ortholattices with monotonic, antimonotonic, and invariant function symbols, is decidable in polynomial time even in the presence of axioms. It gives a sequent calculus SC+ that is sound and complete for OL+ with axioms, proves partial cut elimination (Theorem 4.7) so that every provable sequent has a proof using only subterms of the goal and the axioms, and then reduces proof search to a polynomial-size set of propositional Horn clauses, yielding the $O(n^2(1+|A|))$ decision procedure of Theorem 4.1. For normalization, it characterizes the minimal forms of BL+, bounded lattices with monotone functions, by Whitman-style conditions (Theorem 6.6), constructs a quadratic-time normal form function for BL+, and lifts it to OL+ by pushing negations onto literals and function symbols, obtaining a quadratic-time function that maps each term to the unique smallest term in its equivalence class (Theorem 6.15).","pith_inferences":["The Horn-clause encoding suggests that subtyping queries under a fixed axiom set can be solved incrementally, with new clauses added as constraints are learned, which may yield further speedups in compilers.","The minimal normal form could serve as a canonical key for hash-consing types, making equivalence tests constant-time within a compilation session.","The partial cut elimination result may transfer to other substructural or non-classical logics with monotone operators, where similar Horn-clause encodings would give polynomial decision procedures.","An empirical test on the benchmark families described in the paper (for example the alternating union-intersection types that make current compilers slow) would show whether the predicted quadratic behavior replaces the observed exponential growth."],"forward_implications":["Subtyping in a language with intersection, union, and negation types, covariant and contravariant type constructors, and subtyping constraints can be decided in $O(n^2(1+m))$ time instead of exponential time.","Type simplifiers can use the normalization function to replace every type by the unique smallest equivalent type in quadratic time, never increasing the size of the representation.","Because the semantics is the free ortholattice with monotone functions, any subtyping judgment the algorithm accepts remains valid if new types or constructors are added later, an open-world property.","Record types, nominal subtyping declarations, and constrained polymorphism can be encoded as axioms, so the decision procedure applies to these features directly.","The system deliberately omits distributivity and constructor conjunctivity, matching languages whose type lattices are non-distributive and avoiding unsound laws found in some compilers."],"supporting_citations":[{"why":"Supplies the orthologic-with-axioms proof system and cut-elimination argument that OL+ extends, plus the polynomial entailment algorithm for the base case.","marker":"[21]"},{"why":"Provides the verified and optimized orthologic proof search whose proof-producing approach the normalization section invokes to check computed normal forms.","marker":"[22]"},{"why":"Gives the linear-time algorithm for propositional Horn clause entailment used to make the $O(n^2(1+|A|))$ proof search bound.","marker":"[12]"},{"why":"Whitman's characterization of free lattices is the foundation of the CF+_BL proof system and the normal-form conditions.","marker":"[48]"},{"why":"The monograph on free lattices supplies the Whitman-style theory that the minimal-form characterization generalizes.","marker":"[14]"},{"why":"The prior normalization algorithms for lattices are the base that the $\\zeta$ and $\\eta$ procedures extend to BL+ and OL+.","marker":"[16]"},{"why":"Bruns's construction of free ortholattices is the starting point for the ortholattice normalization theory.","marker":"[3]"}],"fun_headline_variants":["Quadratic subtyping and normalization for orthologic types","Subtyping under assumptions in quadratic time for orthologic types","Orthologic type systems: quadratic subtyping and type simplification","Quadratic-time algorithms for subtyping and type normalization","Orthologic types: subtyping and normalization in quadratic time"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The normalization theorem rests on the unformalized step in Lemma 6.13: if a term $S$ in the negation-normal fragment admits the derivation $S_L,S_L$, then $S$ is equivalent to bottom already in BL+; if that inference fails, the quadratic minimal-normal-form result for OL+ collapses.","fun_headline_variants_meta":{"raw":{"variants":["Quadratic subtyping and normalization for orthologic types","Subtyping under assumptions in quadratic time for orthologic types","Orthologic type systems: quadratic subtyping and type simplification","Quadratic-time algorithms for subtyping and type normalization","Orthologic types: subtyping and normalization in quadratic time"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000308,"raw_usage":{"total_tokens":1712,"prompt_tokens":850,"completion_tokens":862,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":466,"completion_tokens_details":{"reasoning_tokens":778}},"tokens_in":466,"tokens_out":862,"duration_ms":8537,"temperature":1.0,"reasoning_tokens":778,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T17:30:35.539619+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Enumerate small terms in the range of the $\\beta$ reduction and check whether $\\vdash_{CF+_\\delta} S_L,S_L$ holds exactly when $S\\sim_{BL+}0$; a mismatch for any single term would refute Lemma 6.13 and hence Theorem 6.15.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the verified and optimized orthologic proof search whose proof-producing approach the normalization section invokes to check computed normal forms."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Whitman's characterization of free lattices is the foundation of the CF+_BL proof system and the normal-form conditions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The prior normalization algorithms for lattices are the base that the $\\zeta$ and $\\eta$ procedures extend to BL+ and OL+."}],"review_version":1}