Structurally-Defined Alternatives

@cite{katzir-2007}

Katzir, R. (2007). Structurally-defined alternatives. Linguistics and Philosophy, 30(6), 669–690.

Scalar alternatives are not stipulated via Horn scales but generated structurally. The alternatives to a sentence φ are all parse trees obtainable from φ by three operations — deletion, contraction, and substitution — using items from the substitution source L(φ).

Key Definitions

• Substitution source (def 41): L(φ) = lexicon ∪ subtrees(φ)
• Structural complexity (def 19): ψ ≲ φ iff φ can be transformed to ψ by deletion, contraction, and substitution with items from L(φ). Also: φ ∼ ψ (equal complexity) and ψ < φ (strictly less complex).
• Structural alternatives (def 20): A_str(φ) := {ψ : ψ ≲ φ}
• Conversational principle (def 21): do not assert φ if ∃ φ' ∈ A_str(φ) with ⟦φ'⟧ ⊂ ⟦φ⟧ and φ' weakly assertable

The Symmetry Problem

The naïve conversational principle says: don't assert φ if there is a stronger alternative φ'. The symmetry problem (Kroch 1972; von Fintel & Heim class notes; see p. 673) is that for any stronger φ', there exists a symmetric alternative φ'' = φ ∧ ¬φ' which is also stronger, licensing the opposite inference.

Katzir's solution: restrict alternatives to those obtainable by structural operations. For φ = "John ate some of the cake":

• φ' = "John ate all of the cake" ∈ A_str(φ) — by substituting the Det leaf "some" with "all" (both in the lexicon, same category)
• φ'' = "John ate some but not all" ∉ A_str(φ) — requires ConjP/NegP structure not available in L(φ)

Connection to Linglib

• Horn scales subsumed: Lexical substitution of same-category items is a special case of structural alternatives (§8)
• Fills truthmaker gap: AlternativeSensitive.lean's IsTruthmaker requires ALT_S computed via structural alternative generation
• Economy connection: @cite{katzir-singh-2015}'s complexity ordering in KatzirSingh2015.lean is based on structural complexity (def 19)

inductive StructuralAlternatives.SynCat : Type

Syntactic categories for parse tree nodes. Terminal categories (Det, N, V, ...) label leaves; phrasal categories (NP, VP, S, ...) label internal nodes.

• S : SynCat
• NP : SynCat
• VP : SynCat
• Det : SynCat
• N : SynCat
• V : SynCat
• Adj : SynCat
• Adv : SynCat
• PP : SynCat
• P : SynCat
• CP : SynCat
• C : SynCat
• DP : SynCat
• Deg : SynCat
• Conj : SynCat
• ConjP : SynCat
• Neg : SynCat
• NegP : SynCat

instance StructuralAlternatives.instDecidableEqSynCat : DecidableEq SynCat

Equations

• StructuralAlternatives.instDecidableEqSynCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance StructuralAlternatives.instBEqSynCat : BEq SynCat

Equations

• StructuralAlternatives.instBEqSynCat = { beq := StructuralAlternatives.instBEqSynCat.beq }

def StructuralAlternatives.instBEqSynCat.beq : SynCat → SynCat → Bool

Equations

• StructuralAlternatives.instBEqSynCat.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def StructuralAlternatives.instReprSynCat.repr : SynCat → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance StructuralAlternatives.instReprSynCat : Repr SynCat

Equations

• StructuralAlternatives.instReprSynCat = { reprPrec := StructuralAlternatives.instReprSynCat.repr }

instance StructuralAlternatives.instInhabitedSynCat : Inhabited SynCat

Equations

• StructuralAlternatives.instInhabitedSynCat = { default := StructuralAlternatives.instInhabitedSynCat.default }

def StructuralAlternatives.instInhabitedSynCat.default : SynCat

Equations

• StructuralAlternatives.instInhabitedSynCat.default = StructuralAlternatives.SynCat.S

inductive StructuralAlternatives.ParseTree (W : Type) : Type

Parse tree with syntactic category labels. Leaves carry a word of type W; internal nodes carry a list of children. This is the structure that Katzir's operations act on.

• leaf {W : Type} (cat : SynCat) (word : W) : ParseTree W
• node {W : Type} (cat : SynCat) (children : List (ParseTree W)) : ParseTree W

instance StructuralAlternatives.instReprParseTree {W✝ : Type} [Repr W✝] : Repr (ParseTree W✝)

Equations

• StructuralAlternatives.instReprParseTree = { reprPrec := StructuralAlternatives.instReprParseTree.repr }

partial def StructuralAlternatives.instReprParseTree.repr {W✝ : Type} [Repr W✝] : ParseTree W✝ → ℕ → Std.Format

def StructuralAlternatives.ParseTree.cat {W : Type} : ParseTree W → SynCat

Syntactic category of the root node.

Equations

• (StructuralAlternatives.ParseTree.leaf a a_1).cat = a
• (StructuralAlternatives.ParseTree.node a a_1).cat = a

def StructuralAlternatives.ParseTree.beq {W : Type} [BEq W] : ParseTree W → ParseTree W → Bool

Structural equality for parse trees.

Equations

• (StructuralAlternatives.ParseTree.leaf c₁ w₁).beq (StructuralAlternatives.ParseTree.leaf c₂ w₂) = (c₁ == c₂ && w₁ == w₂)
• (StructuralAlternatives.ParseTree.node c₁ cs₁).beq (StructuralAlternatives.ParseTree.node c₂ cs₂) = (c₁ == c₂ && StructuralAlternatives.ParseTree.beq.beqList cs₁ cs₂)
• x✝¹.beq x✝ = false

def StructuralAlternatives.ParseTree.beq.beqList {W : Type} [BEq W] : List (ParseTree W) → List (ParseTree W) → Bool

Equations

• StructuralAlternatives.ParseTree.beq.beqList [] [] = true
• StructuralAlternatives.ParseTree.beq.beqList (a :: as) (b :: bs) = (a.beq b && StructuralAlternatives.ParseTree.beq.beqList as bs)
• StructuralAlternatives.ParseTree.beq.beqList x✝¹ x✝ = false

instance StructuralAlternatives.ParseTree.instBEq {W : Type} [BEq W] : BEq (ParseTree W)

Equations

• StructuralAlternatives.ParseTree.instBEq = { beq := StructuralAlternatives.ParseTree.beq }

def StructuralAlternatives.ParseTree.size {W : Type} : ParseTree W → ℕ

Number of nodes in the tree.

Equations

• (StructuralAlternatives.ParseTree.leaf a a_1).size = 1
• (StructuralAlternatives.ParseTree.node a a_1).size = 1 + StructuralAlternatives.ParseTree.size.sizeList a_1

def StructuralAlternatives.ParseTree.size.sizeList {W : Type} : List (ParseTree W) → ℕ

Equations

• StructuralAlternatives.ParseTree.size.sizeList [] = 0
• StructuralAlternatives.ParseTree.size.sizeList (t :: ts) = t.size + StructuralAlternatives.ParseTree.size.sizeList ts

def StructuralAlternatives.ParseTree.subtrees {W : Type} : ParseTree W → List (ParseTree W)

All subtrees including self (pre-order).

Equations

• (StructuralAlternatives.ParseTree.leaf cat word).subtrees = [StructuralAlternatives.ParseTree.leaf cat word]
• (StructuralAlternatives.ParseTree.node cat cs).subtrees = StructuralAlternatives.ParseTree.node cat cs :: StructuralAlternatives.ParseTree.subtrees.subtreesList cs

def StructuralAlternatives.ParseTree.subtrees.subtreesList {W : Type} : List (ParseTree W) → List (ParseTree W)

Equations

• StructuralAlternatives.ParseTree.subtrees.subtreesList [] = []
• StructuralAlternatives.ParseTree.subtrees.subtreesList (t :: ts) = t.subtrees ++ StructuralAlternatives.ParseTree.subtrees.subtreesList ts

def StructuralAlternatives.ParseTree.containsCat {W : Type} (c : SynCat) : ParseTree W → Bool

Whether a category appears anywhere in the tree.

Equations

• StructuralAlternatives.ParseTree.containsCat c (StructuralAlternatives.ParseTree.leaf a a_1) = (c == a)
• StructuralAlternatives.ParseTree.containsCat c (StructuralAlternatives.ParseTree.node a a_1) = (c == a || StructuralAlternatives.ParseTree.containsCat.containsCatList c a_1)

def StructuralAlternatives.ParseTree.containsCat.containsCatList {W : Type} (c : SynCat) : List (ParseTree W) → Bool

Equations

• One or more equations did not get rendered due to their size.
• StructuralAlternatives.ParseTree.containsCat.containsCatList c [] = false

def StructuralAlternatives.ParseTree.leafSubst {W : Type} [BEq W] (target replacement : W) (c : SynCat) : ParseTree W → ParseTree W

Substitute all leaves of category c carrying word target with replacement. This is the most common structural operation: replacing one scalar item with another of the same category.

Equations

• One or more equations did not get rendered due to their size.

def StructuralAlternatives.ParseTree.leafSubst.leafSubstList {W : Type} [BEq W] (target replacement : W) (c : SynCat) : List (ParseTree W) → List (ParseTree W)

Equations

• One or more equations did not get rendered due to their size.
• StructuralAlternatives.ParseTree.leafSubst.leafSubstList target replacement c [] = []

def StructuralAlternatives.substitutionSource {W : Type} (lexicon : List (ParseTree W)) (φ : ParseTree W) : List (ParseTree W)

The substitution source for φ (def 41, final version): the union of the lexicon of the language with the set of all subtrees of φ. The revised definition (adding subtrees) is needed to handle Matsumoto's examples (§5) where a complex sub-constituent of φ serves as a substitution source for a simpler constituent elsewhere in φ.

The initial definition (def 18) used only the lexicon; def 41 adds subtrees of φ to derive the inference in examples like: "It was warm yesterday, and it is a little bit more than warm today" where "a little bit more than warm" (a subtree of φ) substitutes for "warm" in the left conjunct.

Equations

• StructuralAlternatives.substitutionSource lexicon φ = lexicon ++ φ.subtrees

inductive StructuralAlternatives.StructOp {W : Type} (source : List (ParseTree W)) : ParseTree W → ParseTree W → Prop

One structural operation on parse trees (p. 678). StructOp source φ ψ means ψ is obtained from φ by one application of deletion, contraction, or substitution with items from source.

The three operations:

• Deletion: remove a subtree (a child from a node)
• Contraction: remove an edge and identify endpoints (replace a node with one of its same-category children)
• Substitution: replace any constituent with a same-category item from the substitution source L(φ)

• subst {W : Type} {source : List (ParseTree W)} {φ ψ : ParseTree W} (h_cat : ψ.cat = φ.cat) (h_src : ψ ∈ source) : StructOp source φ ψ

  Substitute: replace tree with a same-category item from source.

• delete {W : Type} {source : List (ParseTree W)} {cat : SynCat} {cs : List (ParseTree W)} (i : Fin cs.length) : StructOp source (ParseTree.node cat cs) (ParseTree.node cat (cs.eraseIdx ↑i))

  Delete: remove the i-th child from a node.

• contract {W : Type} {source : List (ParseTree W)} {cat : SynCat} {cs : List (ParseTree W)} {child : ParseTree W} (h_mem : child ∈ cs) (h_cat : child.cat = cat) : StructOp source (ParseTree.node cat cs) child

  Contract: replace a node with one of its same-category children.

• inChild {W : Type} {source : List (ParseTree W)} {cat : SynCat} {cs : List (ParseTree W)} (i : Fin cs.length) {ψ_child : ParseTree W} (h_step : StructOp source (cs.get i) ψ_child) : StructOp source (ParseTree.node cat cs) (ParseTree.node cat (cs.set (↑i) ψ_child))

  Recursive: apply an operation inside one child of a node.

def StructuralAlternatives.atMostAsComplex {W : Type} (source : List (ParseTree W)) (ψ φ : ParseTree W) : Prop

Structural complexity ordering (def 19): ψ ≲ φ iff φ can be transformed into ψ by a finite chain of structural operations using items from source.

Formally: the reflexive-transitive closure of StructOp source.

Equations

• StructuralAlternatives.atMostAsComplex source ψ φ = Relation.ReflTransGen (StructuralAlternatives.StructOp source) φ ψ

def StructuralAlternatives.equalComplexity {W : Type} (source : List (ParseTree W)) (φ ψ : ParseTree W) : Prop

Equal complexity (def 19): φ ∼ ψ iff φ ≲ ψ ∧ ψ ≲ φ.

Equations

• StructuralAlternatives.equalComplexity source φ ψ = (StructuralAlternatives.atMostAsComplex source φ ψ ∧ StructuralAlternatives.atMostAsComplex source ψ φ)

def StructuralAlternatives.strictlyLessComplex {W : Type} (source : List (ParseTree W)) (ψ φ : ParseTree W) : Prop

Strictly less complex (def 19): ψ < φ iff ψ ≲ φ ∧ ¬(φ ≲ ψ).

Equations

• StructuralAlternatives.strictlyLessComplex source ψ φ = (StructuralAlternatives.atMostAsComplex source ψ φ ∧ ¬StructuralAlternatives.atMostAsComplex source φ ψ)

def StructuralAlternatives.structuralAlternatives {W : Type} (lex : List (ParseTree W)) (φ : ParseTree W) : Set (ParseTree W)

Structural alternatives (def 20): A_str(φ) := {ψ : ψ ≲ φ}, where ≲ uses L(φ) = lexicon ∪ subtrees(φ).

Equations

• StructuralAlternatives.structuralAlternatives lex φ = {ψ : StructuralAlternatives.ParseTree W | StructuralAlternatives.atMostAsComplex (StructuralAlternatives.substitutionSource lex φ) ψ φ}

theorem StructuralAlternatives.self_is_alternative {W : Type} (lex : List (ParseTree W)) (φ : ParseTree W) : φ ∈ structuralAlternatives lex φ

φ is always a structural alternative to itself (reflexivity of ≲).

inductive StructuralAlternatives.ExWord : Type

Vocabulary for the worked examples.

• john : ExWord
• ate : ExWord
• some_ : ExWord
• all_ : ExWord
• cake : ExWord
• apple : ExWord
• pear : ExWord
• or_ : ExWord
• and_ : ExWord
• tall : ExWord
• man : ExWord
• but_ : ExWord
• not_ : ExWord

instance StructuralAlternatives.instDecidableEqExWord : DecidableEq ExWord

Equations

• StructuralAlternatives.instDecidableEqExWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance StructuralAlternatives.instBEqExWord : BEq ExWord

Equations

• StructuralAlternatives.instBEqExWord = { beq := StructuralAlternatives.instBEqExWord.beq }

def StructuralAlternatives.instBEqExWord.beq : ExWord → ExWord → Bool

Equations

• StructuralAlternatives.instBEqExWord.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance StructuralAlternatives.instReprExWord : Repr ExWord

Equations

• StructuralAlternatives.instReprExWord = { reprPrec := StructuralAlternatives.instReprExWord.repr }

def StructuralAlternatives.instReprExWord.repr : ExWord → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def StructuralAlternatives.exLexicon : List (ParseTree ExWord)

Minimal lexicon: terminal items available for substitution.

Equations

• One or more equations did not get rendered due to their size.

def StructuralAlternatives.someSentence : ParseTree ExWord

φ = "John ate some cake" (simplified parse tree).

Equations

• One or more equations did not get rendered due to their size.

def StructuralAlternatives.allSentence : ParseTree ExWord

φ' = "John ate all cake" — the scalar alternative.

Equations

• One or more equations did not get rendered due to their size.

theorem StructuralAlternatives.leafSubst_some_all : ParseTree.leafSubst ExWord.some_ ExWord.all_ SynCat.Det someSentence = allSentence

Leaf substitution of "some" → "all" produces the expected tree.

theorem StructuralAlternatives.all_is_alternative_to_some : allSentence ∈ structuralAlternatives exLexicon someSentence

φ' is a structural alternative to φ: substitute Det leaf "some" with "all" from the lexicon (both Det, same category).

This is the paper's ex. (25): φ = "John ate some of the cake", φ' = "John ate all of the cake". Since "all" and "some" are both in the lexicon and both Det, substitution yields φ' ∼ φ, so φ' ∈ A_str(φ).

theorem StructuralAlternatives.some_all_equal_complexity : equalComplexity (substitutionSource exLexicon someSentence) someSentence allSentence

Equal complexity: "some" ↔ "all" by mutual substitution (same number of operations in each direction). φ' ∼ φ in the sense of def 19: both φ ≲ φ' and φ' ≲ φ hold (each obtained from the other by one leaf substitution).

def StructuralAlternatives.someButNotAllSentence : ParseTree ExWord

φ'' = "John ate some but not all cake" — the symmetric alternative that the naïve principle cannot exclude.

Under the naïve principle, φ'' is stronger than φ (⟦φ''⟧ ⊂ ⟦φ⟧) and should block assertion of φ. But it licenses the inference that John ate ALL of the cake — the opposite of the correct implicature. Katzir's structural approach excludes φ'' because it requires ConjP and NegP structure not derivable from L(φ).

Equations

• One or more equations did not get rendered due to their size.

theorem StructuralAlternatives.symmetric_has_conjp : ParseTree.containsCat SynCat.ConjP someButNotAllSentence = true

φ'' contains ConjP — a category absent from φ and L(φ).

theorem StructuralAlternatives.some_lacks_conjp : ParseTree.containsCat SynCat.ConjP someSentence = false

φ does not contain ConjP.

theorem StructuralAlternatives.source_lacks_conjp : ((substitutionSource exLexicon someSentence).all fun (t : ParseTree ExWord) => !ParseTree.containsCat SynCat.ConjP t) = true

No item in L(someSentence) contains ConjP: the lexicon consists of terminal leaves (which have no internal structure) and the subtrees of φ are {S[...], N(john), VP[...], V(ate), Det(some), N(cake)} — none contain ConjP.

theorem StructuralAlternatives.category_preservation {W : Type} (source : List (ParseTree W)) (c : SynCat) (φ ψ : ParseTree W) (h_source : ∀ (s : ParseTree W), s ∈ source → ParseTree.containsCat c s = false) (h_φ : ParseTree.containsCat c φ = false) (h_reach : atMostAsComplex source ψ φ) : ParseTree.containsCat c ψ = false

Key invariant: structural operations preserve absence of a category when that category does not appear in the substitution source.

If no item in source contains category c, and tree φ does not contain c, then no tree reachable from φ by structural operations contains c. This is because:

• Substitution can only introduce material from source (which lacks c)
• Deletion removes material (can't introduce c)
• Contraction promotes a subtree (which also lacks c by hypothesis)

Proof by induction on ReflTransGen, reducing to the single-step structOp_preserves_no_cat which case-splits on the four StructOp constructors.

theorem StructuralAlternatives.symmetry_problem_solved : ¬someButNotAllSentence ∈ structuralAlternatives exLexicon someSentence

The symmetric alternative φ'' is NOT a structural alternative to φ.

Proof sketch: L(φ) contains no item with category ConjP (source_lacks_conjp), and φ itself lacks ConjP (some_lacks_conjp), so by category_preservation every tree in A_str(φ) lacks ConjP. But φ'' contains ConjP (symmetric_has_conjp) — contradiction.

This is the paper's central result: structure alone excludes the symmetric alternative, solving the symmetry problem without lexical stipulation of which alternatives are "good."

def StructuralAlternatives.orSentence : ParseTree ExWord

φ = "John ate the apple or the pear" (ex. 26a).

Equations

• One or more equations did not get rendered due to their size.

def StructuralAlternatives.andSentence : ParseTree ExWord

φ' = "John ate the apple and the pear" (ex. 26b). Obtained by substituting Conj "or" with "and".

Equations

• One or more equations did not get rendered due to their size.

theorem StructuralAlternatives.leafSubst_or_and : ParseTree.leafSubst ExWord.or_ ExWord.and_ SynCat.Conj orSentence = andSentence

Leaf substitution of "or" → "and" produces the conjunction.

theorem StructuralAlternatives.and_is_alternative_to_or : andSentence ∈ structuralAlternatives exLexicon orSentence

"and" alternative obtainable by one substitution step.

def StructuralAlternatives.leftDisjunct : ParseTree ExWord

The left disjunct "John ate the apple" is an alternative to the disjunction — obtainable by deletion of the right disjunct and the conjunction.

This derives the effect of Sauerland's L operator (which returns the left argument of a binary connective) from structural operations alone, without stipulating L as a primitive. The paper (p. 683) notes that L and R are "somewhat stipulative" and that structural alternatives derive the same predictions.

Equations

• One or more equations did not get rendered due to their size.

theorem StructuralAlternatives.left_disjunct_is_alternative : leftDisjunct ∈ structuralAlternatives exLexicon orSentence

def StructuralAlternatives.rightDisjunct : ParseTree ExWord

The right disjunct is also an alternative (Sauerland's R operator).

Equations

• One or more equations did not get rendered due to their size.

theorem StructuralAlternatives.right_disjunct_is_alternative : rightDisjunct ∈ structuralAlternatives exLexicon orSentence

def StructuralAlternatives.tallMan : ParseTree ExWord

"A tall man" parse tree (ex. 29a).

Equations

• One or more equations did not get rendered due to their size.

def StructuralAlternatives.justMan : ParseTree ExWord

"A man" — obtained by deleting the Adj modifier (ex. 29b).

Equations

• One or more equations did not get rendered due to their size.

theorem StructuralAlternatives.deletion_produces_alternative : justMan ∈ structuralAlternatives exLexicon tallMan

Deletion produces a simpler alternative: "a man" ∈ A_str("a tall man").

Under the structural approach, any modifier can be deleted to produce an alternative. Since the modified NP entails the bare NP ("a tall man came" → "a man came"), the bare NP is a stronger alternative in upward-entailing contexts, triggering no implicature. In DE contexts, entailment reverses and deletion alternatives generate inferences (§4.3, exx. 30–32).

theorem StructuralAlternatives.deletion_reduces_size : justMan.size < tallMan.size

Deletion reduces tree size.

theorem StructuralAlternatives.horn_alternatives_are_structural {W : Type} [BEq W] (lex : List (ParseTree W)) (φ : ParseTree W) (α β : W) (c : SynCat) (_h_α_in_lex : ParseTree.leaf c α ∈ lex) (_h_β_in_lex : ParseTree.leaf c β ∈ lex) : ParseTree.leafSubst α β c φ ∈ structuralAlternatives lex φ

Horn scale alternatives are a special case of structural alternatives.

If two words α and β are on the same Horn scale (and therefore have the same syntactic category), then for any sentence tree φ containing α, the tree φ[β/α] obtained by leaf substitution is a structural alternative to φ. This is because:

1. β is in the lexicon (hence in L(φ))
2. β has the same category as α
3. Leaf substitution is a sequence of StructOp.subst steps (one per occurrence of α)

This means the scale-based approach to alternatives (listing Horn sets like ⟨some, most, all⟩) is not wrong — it is subsumed by the structural approach. Everything a Horn scale generates, structural operations generate too. But structural operations also generate alternatives that scales miss: deletion alternatives in DE contexts (§4.3), and sub-constituent alternatives for disjunction (§4.2).

TODO: Proof by induction on the tree structure, applying StructOp.subst at each matching leaf via StructOp.inChild.

def StructuralAlternatives.violatesConversationalPrinciple {W World : Type} (lex : List (ParseTree W)) (meaning : ParseTree W → World → Bool) (φ : ParseTree W) (weaklyAssertable : ParseTree W → Bool) : Prop

The neo-Gricean conversational principle with structural alternatives (def 21): do not assert φ if there is another sentence φ' ∈ A_str(φ) such that ⟦φ'⟧ ⊂ ⟦φ⟧ and φ' is weakly assertable.

This replaces the naïve principle (which considers ALL stronger alternatives) with one restricted to structurally-defined alternatives. The restriction solves the symmetry problem: φ'' = φ ∧ ¬φ' is excluded from A_str(φ) because it requires more structure than φ provides.

The at-least-as-good-as relation (def 23, p. 680) combines structural complexity (≲) with semantic entailment (⊆). This is the same relation formalized in KatzirSingh2015.lean as atLeastAsGood, where complexity is an abstract ℕ parameter — the structural complexity defined here gives that parameter its intended content.

Equations

• One or more equations did not get rendered due to their size.

def StructuralAlternatives.atLeastAsGoodAs {W World : Type} (lex : List (ParseTree W)) (meaning : ParseTree W → World → Bool) (φ ψ : ParseTree W) : Prop

At-least-as-good-as relation (def 23, p. 680): φ ≲ ψ iff φ ≲_struct ψ ∧ ⟦φ⟧ ⊆ ⟦ψ⟧.

This combines structural complexity (from def 19) with semantic entailment. It is the relation that @cite{katzir-singh-2015} use as the basis for the Answer Condition in KatzirSingh2015.lean, where it appears as Scenario.atLeastAsGood.

The key insight: in KatzirSingh2015.lean, complexity is an abstract ℕ parameter. Here, structural complexity gives that parameter its intended content — the number of structural operations needed.

Equations

• One or more equations did not get rendered due to their size.