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(φ)

Tree Type

Uses the unified Tree C W from Core.Tree. All definitions are parameterized over the category type C, so they work with UD-grounded Cat, framework-specific categories, or any C with BEq/DecidableEq.

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)

def StructuralAlternatives.substitutionSource {C W : Type} (lexicon : List (Core.Tree.Tree C W)) (φ : Core.Tree.Tree C W) : List (Core.Tree.Tree C 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 {C W : Type} (source : List (Core.Tree.Tree C W)) : Core.Tree.Tree C W → Core.Tree.Tree C 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(φ)

The inBind constructor extends Katzir's original PF-only operations to handle binding structures, allowing structural operations inside the body of a λ-binder.

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

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

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

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

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

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

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

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

• inBind {C W : Type} {source : List (Core.Tree.Tree C W)} {n : ℕ} {cat : C} {body body' : Core.Tree.Tree C W} (h_step : StructOp source body body') : StructOp source (Core.Tree.Tree.bind n cat body) (Core.Tree.Tree.bind n cat body')

  Recursive: apply an operation inside a binder body.

def StructuralAlternatives.atMostAsComplex {C W : Type} (source : List (Core.Tree.Tree C W)) (ψ φ : Core.Tree.Tree C 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 {C W : Type} (source : List (Core.Tree.Tree C W)) (φ ψ : Core.Tree.Tree C W) : Prop

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

Equations

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

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

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

Equations

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

def StructuralAlternatives.structuralAlternatives {C W : Type} (lex : List (Core.Tree.Tree C W)) (φ : Core.Tree.Tree C W) : Set (Core.Tree.Tree C W)

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

Equations

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

theorem StructuralAlternatives.self_is_alternative {C W : Type} (lex : List (Core.Tree.Tree C W)) (φ : Core.Tree.Tree C 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)

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

Equations

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

instance StructuralAlternatives.instReprExWord : Repr ExWord

Equations

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

def StructuralAlternatives.exLexicon : List (Core.Tree.Tree Core.Tree.Cat ExWord)

Minimal lexicon: terminal items available for substitution.

Equations

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

def StructuralAlternatives.someSentence : Core.Tree.Tree Core.Tree.Cat ExWord

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

Equations

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

def StructuralAlternatives.allSentence : Core.Tree.Tree Core.Tree.Cat 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 : Core.Tree.Tree.leafSubst ExWord.some_ ExWord.all_ Core.Tree.Cat.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 : Core.Tree.Tree Core.Tree.Cat 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 : Core.Tree.Tree.containsCat Core.Tree.Cat.ConjP someButNotAllSentence = true

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

theorem StructuralAlternatives.some_lacks_conjp : Core.Tree.Tree.containsCat Core.Tree.Cat.ConjP someSentence = false

φ does not contain ConjP.

theorem StructuralAlternatives.source_lacks_conjp : ((substitutionSource exLexicon someSentence).all fun (t : Core.Tree.Tree Core.Tree.Cat ExWord) => !Core.Tree.Tree.containsCat Core.Tree.Cat.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 {C W : Type} [BEq C] (source : List (Core.Tree.Tree C W)) (c : C) (φ ψ : Core.Tree.Tree C W) (h_source : ∀ (s : Core.Tree.Tree C W), s ∈ source → Core.Tree.Tree.containsCat c s = false) (h_φ : Core.Tree.Tree.containsCat c φ = false) (h_reach : atMostAsComplex source ψ φ) : Core.Tree.Tree.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 five 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 : Core.Tree.Tree Core.Tree.Cat 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 : Core.Tree.Tree Core.Tree.Cat 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 : Core.Tree.Tree.leafSubst ExWord.or_ ExWord.and_ Core.Tree.Cat.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 : Core.Tree.Tree Core.Tree.Cat 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 : Core.Tree.Tree Core.Tree.Cat 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 : Core.Tree.Tree Core.Tree.Cat ExWord

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

Equations

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

def StructuralAlternatives.justMan : Core.Tree.Tree Core.Tree.Cat ExWord

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

Equations

• StructuralAlternatives.justMan = Core.Tree.Tree.node Core.Tree.Cat.NP [Core.Tree.Tree.terminal Core.Tree.Cat.N StructuralAlternatives.ExWord.man]

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 {C W : Type} [BEq C] [LawfulBEq C] [BEq W] (lex : List (Core.Tree.Tree C W)) (φ : Core.Tree.Tree C W) (α β : W) (c : C) (_h_α_in_lex : Core.Tree.Tree.terminal c α ∈ lex) (_h_β_in_lex : Core.Tree.Tree.terminal c β ∈ lex) : Core.Tree.Tree.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).

def StructuralAlternatives.violatesConversationalPrinciple {C W World : Type} (lex : List (Core.Tree.Tree C W)) (meaning : Core.Tree.Tree C W → World → Bool) (φ : Core.Tree.Tree C W) (weaklyAssertable : Core.Tree.Tree C 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 {C W World : Type} (lex : List (Core.Tree.Tree C W)) (meaning : Core.Tree.Tree C W → World → Bool) (φ ψ : Core.Tree.Tree C 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.