Documentation

Linglib.Semantics.Alternatives.Structural

Structurally-Defined Alternatives #

[Kat07]

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 #

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":

Tree Type #

Uses the unified Tree C W from Syntax. 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 #

def Alternatives.Structural.substitutionSource {C W : Type} (lexicon : List (Syntax.Tree C W)) (φ : Syntax.Tree C W) :
List (Syntax.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
Instances For
    inductive Alternatives.Structural.StructOp {C W : Type} (source : List (Syntax.Tree C W)) :
    Syntax.Tree C WSyntax.Tree C WProp

    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.

    Instances For
      def Alternatives.Structural.atMostAsComplex {C W : Type} (source : List (Syntax.Tree C W)) (ψ φ : Syntax.Tree C W) :

      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. This is the reachability preorder underlying [Kat07]'s ≲, which suffices for A_str as a set (def 20) and for the worked examples. It is not a graded operation-count: two mutually-reachable trees need not take the same number of steps, so equalComplexity (mutual reachability) is coarser than Katzir's "equal complexity" ∼, and the strict orderings the paper uses in §4.2–§4.3 are reachability-strict, not count-strict.

      Equations
      Instances For
        def Alternatives.Structural.equalComplexity {C W : Type} (source : List (Syntax.Tree C W)) (φ ψ : Syntax.Tree C W) :

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

        Equations
        Instances For
          def Alternatives.Structural.strictlyLessComplex {C W : Type} (source : List (Syntax.Tree C W)) (ψ φ : Syntax.Tree C W) :

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

          Equations
          Instances For
            def Alternatives.Structural.structuralAlternatives {C W : Type} (lex : List (Syntax.Tree C W)) (φ : Syntax.Tree C W) :
            Set (Syntax.Tree C W)

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

            Equations
            Instances For

              The Katzir source as an Alternatives.Source. Pragmatic competition operators (violatesMP, violatesMaximize, violatesMCIs in Alternatives.Competition) accept any Source (Tree C W); pass katzirSource lex to recover the classical Katzir 2007 competition. Other sources include Alternatives.indirectFrom (Jeretič et al. 2025).

              Equations
              Instances For
                theorem Alternatives.Structural.self_is_alternative {C W : Type} (lex : List (Syntax.Tree C W)) (φ : Syntax.Tree C W) :

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

                theorem Alternatives.Structural.self_mem_katzirSource {C W : Type} (lex : List (Syntax.Tree C W)) (φ : Syntax.Tree C W) :
                φ katzirSource lex φ
                theorem Alternatives.Structural.equalComplexity.refl {C W : Type} {source : List (Syntax.Tree C W)} (φ : Syntax.Tree C W) :
                equalComplexity source φ φ
                theorem Alternatives.Structural.equalComplexity.symm {C W : Type} {source : List (Syntax.Tree C W)} {a b : Syntax.Tree C W} (h : equalComplexity source a b) :
                equalComplexity source b a
                theorem Alternatives.Structural.equalComplexity.trans {C W : Type} {source : List (Syntax.Tree C W)} {a b c : Syntax.Tree C W} (h₁ : equalComplexity source a b) (h₂ : equalComplexity source b c) :
                equalComplexity source a c
                theorem Alternatives.Structural.equalComplexity.equivalence {C W : Type} {source : List (Syntax.Tree C W)} :
                Equivalence (equalComplexity source)

                equalComplexity source is an equivalence relation — the equivalence kernel of the atMostAsComplex source preorder. Bundled so consumers can take a Setoid/quotient or feed mathlib's Equivalence API.

                theorem Alternatives.Structural.equalComplexity_terminal_subst {C W : Type} (source : List (Syntax.Tree C W)) (cat : C) (oldW newW : W) (h_old : Syntax.Tree.terminal cat oldW source) (h_new : Syntax.Tree.terminal cat newW source) :

                A single same-category terminal substitution gives equal complexity, provided BOTH terminals are in the source (so the substitution is reversible). The standard atom for any equalComplexity chain.

                Vocabulary for the worked examples.

                Instances For
                  @[implicit_reducible]
                  Equations
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Minimal lexicon: terminal items available for substitution.

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

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

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

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

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

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

                          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).

                          φ'' = "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.
                          Instances For

                            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 Alternatives.Structural.category_preservation {C W : Type} [DecidableEq C] (source : List (Syntax.Tree C W)) (c : C) (φ ψ : Syntax.Tree C W) (h_source : ssource, ¬Syntax.Tree.ContainsCat c s) (h_φ : ¬Syntax.Tree.ContainsCat c φ) (h_reach : atMostAsComplex source ψ φ) :

                            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.

                            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 exhibits the symmetry solution on the paper's canonical example: structure alone excludes the symmetric alternative, no lexical stipulation of which alternatives are "good." Scope note: [Kat07] excludes φ'' because it is strictly more complex / unreachable; the proof here uses a sufficient witness — φ'' needs a phrasal category (ConjP) absent from L(φ), and category_preservation shows the operations never introduce a novel category. The category-absence proxy coincides with Katzir's criterion whenever the symmetric alternative requires new structure (true here), but is narrower than the general strict-complexity exclusion, which atMostAsComplex (bare reachability, not graded operation-count) does not formalize. The general result is the target of Studies/FoxKatzir2011.lean.

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

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

                              φ' = "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.
                              Instances For

                                "and" alternative obtainable by one substitution step.

                                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.
                                Instances For

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

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

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

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

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