Trinh & Haida 2015: Constraining the Derivation of Alternatives

[TH15]

Trinh, T. & Haida, A. (2015). Constraining the derivation of alternatives. Natural Language Semantics, 23(4), 249–270.

Core Contribution

The Atomicity constraint (def 32): expressions in the substitution source are syntactically atomic — their internal structure is inaccessible to structural operations. This refines [FK11] / [Kat07] to correctly distinguish:

• Symmetry-breaking cases (§3.2.2): "Bill ran and didn't smoke. John ran." → John smoked. Atomicity blocks "ran ∧ smoked" from F(S), so A = {run, run ∧ ¬smoke} satisfies Conditions on A (27), and EXH derives ¬(run ∧ ¬smoke).

• Symmetry-preserving cases (§3.2.3): "Bill ate exactly three. John ate three." → ✗John ate exactly three. Atomicity is vacuous; Conditions on A (27c) force "four" into A, creating symmetry.

Key Definitions

• inBooleanClosure: p is determined by a set of propositions (27c)
• isValidDomain: Conditions on A (27) for EXH domains
• ATree / ATStructOp: parse trees with AT-marking; structural operations that cannot enter AT-marked nodes
• structuralAlternativesAT: F_AT(S) ⊆ F(S)

Relation to the Excluder.preFilter combinator

Atomicity is a restriction on the formal-alternative source F, the [FK11] F (not C) side of the asymmetry. Semantics/Exhaustification/Combinators.lean packages F-side restrictions as the abstract combinator Excluder.preFilter, with the algebraic non-monotonicity theorem preFilter_can_create_implicature. The Trinh–Haida construction is a linguistically-motivated two-layer F-side restriction (Atomicity + Conditions on A), so it doesn't reduce to a single preFilter call: innocent.exh on full F_AT(run) remains vacuous; the strengthening to ran ∧ smoked requires the further domain-choice step A = {ran, ranNotSmoked}. The Symmetric/Atomic formalization here is therefore complementary to (not subsumed by) the abstract combinator: Combinators.lean proves the asymmetry exists in the algebra; this file shows the linguistic substance the asymmetry licenses.

def TrinhHaida2015.inBooleanClosure {W : Type} (domain : List W) (alts : List (W → Bool)) (p : W → Bool) : Bool

A proposition p is in the Boolean closure of alts: p is determined by the truth values of elements of alts. Whenever two worlds agree on all elements of alts, they agree on p. Used in Condition (27c).

Equations

• TrinhHaida2015.inBooleanClosure domain alts p = domain.all fun (w₁ : W) => domain.all fun (w₂ : W) => (!alts.all fun (a : W → Bool) => a w₁ == a w₂) || p w₁ == p w₂

def TrinhHaida2015.propEqOn {W : Type} (domain : List W) (p q : W → Bool) : Bool

Extensional equality on a finite domain.

Equations

• TrinhHaida2015.propEqOn domain p q = domain.all fun (w : W) => p w == q w

def TrinhHaida2015.propMemOn {W : Type} (domain : List W) (p : W → Bool) (alts : List (W → Bool)) : Bool

Extensional membership via propEqOn.

Equations

• TrinhHaida2015.propMemOn domain p alts = alts.any fun (a : W → Bool) => TrinhHaida2015.propEqOn domain p a

def TrinhHaida2015.isValidDomain {W : Type} (domain : List W) (formalAlts : List (W → Bool)) (prejacent : W → Bool) (domainOfEXH : List (W → Bool)) : Bool

Conditions on A (27): A is a valid domain of EXH for prejacent S given formal alternatives formalAlts = F(S).

(27a) A ⊆ F(S) (27b) S ∈ A (27c) No S' in F(S) \ A is in the Boolean closure of A

Equations

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

inductive TrinhHaida2015.ATree (W : Type) : Type

Parse tree with optional AT-marking. AT-marked nodes (atNode) preserve content for semantic interpretation but are inaccessible to structural operations — implementing the Atomicity constraint (def 32): "Expressions in the substitution source are syntactically atomic."

• leaf {W : Type} (cat : Syntax.Cat) (word : W) : ATree W
• node {W : Type} (cat : Syntax.Cat) (children : List (ATree W)) : ATree W
• atNode {W : Type} (cat : Syntax.Cat) (content : Syntax.Tree Syntax.Cat W) : ATree W

def TrinhHaida2015.ATree.cat {W : Type} : ATree W → Syntax.Cat

Equations

• (TrinhHaida2015.ATree.leaf c word).cat = c
• (TrinhHaida2015.ATree.node c children).cat = c
• (TrinhHaida2015.ATree.atNode c content).cat = c

def TrinhHaida2015.ATree.expand {W : Type} : ATree W → Syntax.Tree Syntax.Cat W

Expand to Tree Cat by unsealing AT-marked nodes.

Equations

• (TrinhHaida2015.ATree.leaf c word).expand = Syntax.Tree.terminal c word
• (TrinhHaida2015.ATree.node c children).expand = Syntax.Tree.node c (TrinhHaida2015.ATree.expand.expandList children)
• (TrinhHaida2015.ATree.atNode c content).expand = content

def TrinhHaida2015.ATree.expand.expandList {W : Type} : List (ATree W) → List (Syntax.Tree Syntax.Cat W)

Equations

• TrinhHaida2015.ATree.expand.expandList [] = []
• TrinhHaida2015.ATree.expand.expandList (t :: ts) = t.expand :: TrinhHaida2015.ATree.expand.expandList ts

def TrinhHaida2015.ATree.lift {W : Type} : Syntax.Tree Syntax.Cat W → ATree W

Lift a Tree Cat to ATree (no AT-marking). Traces and binders are wrapped as opaque AT-marked nodes, since they are LF-specific structure inaccessible to PF-level operations.

Equations

• TrinhHaida2015.ATree.lift (Syntax.Tree.terminal c w) = TrinhHaida2015.ATree.leaf c w
• TrinhHaida2015.ATree.lift (Syntax.Tree.node c cs) = TrinhHaida2015.ATree.node c (TrinhHaida2015.ATree.lift.liftList cs)
• TrinhHaida2015.ATree.lift (Syntax.Tree.trace n c) = TrinhHaida2015.ATree.atNode c (Syntax.Tree.trace n c)
• TrinhHaida2015.ATree.lift (Syntax.Tree.bind n c body) = TrinhHaida2015.ATree.atNode c (Syntax.Tree.bind n c body)

def TrinhHaida2015.ATree.lift.liftList {W : Type} : List (Syntax.Tree Syntax.Cat W) → List (ATree W)

Equations

• TrinhHaida2015.ATree.lift.liftList [] = []
• TrinhHaida2015.ATree.lift.liftList (t :: ts) = TrinhHaida2015.ATree.lift t :: TrinhHaida2015.ATree.lift.liftList ts

inductive TrinhHaida2015.ATStructOp {W : Type} (source : List (ATree W)) : ATree W → ATree W → Prop

Structural operation respecting Atomicity. Like StructOp but inChild can only descend into .node, NOT .atNode. AT-marked material is opaque to further syntactic manipulation.

• subst {W : Type} {source : List (ATree W)} {φ ψ : ATree W} (h_cat : ψ.cat = φ.cat) (h_src : ψ ∈ source) : ATStructOp source φ ψ
• delete {W : Type} {source : List (ATree W)} {cat : Syntax.Cat} {cs : List (ATree W)} (i : Fin cs.length) : ATStructOp source (ATree.node cat cs) (ATree.node cat (cs.eraseIdx ↑i))
• contract {W : Type} {source : List (ATree W)} {cat : Syntax.Cat} {cs : List (ATree W)} {child : ATree W} (h_mem : child ∈ cs) (h_cat : child.cat = cat) : ATStructOp source (ATree.node cat cs) child
• inChild {W : Type} {source : List (ATree W)} {cat : Syntax.Cat} {cs : List (ATree W)} (i : Fin cs.length) {ψ_child : ATree W} (h_step : ATStructOp source (cs.get i) ψ_child) : ATStructOp source (ATree.node cat cs) (ATree.node cat (cs.set (↑i) ψ_child))

def TrinhHaida2015.atReachable {W : Type} (source : List (ATree W)) (ψ φ : ATree W) : Prop

AT-constrained reachability (reflexive-transitive closure).

Equations

• TrinhHaida2015.atReachable source ψ φ = Relation.ReflTransGen (TrinhHaida2015.ATStructOp source) φ ψ

def TrinhHaida2015.atomicSubstitutionSource {W : Type} (lexicon : List (Syntax.Tree Syntax.Cat W)) (φ : Syntax.Tree Syntax.Cat W) (context : List (Syntax.Tree Syntax.Cat W)) : List (ATree W)

The substitution source with Atomicity: lexical items + subtrees of S are lifted (transparent); contextual constituents are wrapped in atNode (opaque).

Equations

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

def TrinhHaida2015.structuralAlternativesAT {W : Type} (lex : List (Syntax.Tree Syntax.Cat W)) (φ : Syntax.Tree Syntax.Cat W) (context : List (Syntax.Tree Syntax.Cat W)) : Set (Syntax.Tree Syntax.Cat W)

F_AT(S): formal alternatives derivable under Atomicity. S' ∈ F_AT(S) iff ∃ ATree t reachable from lift(S) via AT-constrained operations with t.expand = S'.

Equations

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

Symmetry Breaking

(34) Bill went for a run and didn't smoke. John (only) went for a run. Inference: ¬[John went for a run and didn't smoke] → John smoked.

Atomicity blocks "ran ∧ smoked" from F(S) because deriving it requires modifying the interior of the AT-marked contextual constituent "ran ∧ ¬smoked" (removing the NegP). This leaves A = {run, run ∧ ¬smoke} as a valid domain satisfying (27c), and EXH(A)(run) = run ∧ smoke.

inductive TrinhHaida2015.AW : Type

Four activity worlds (run and smoke are independent).

• rs : AW
• rns : AW
• s : AW
• ns : AW

@[implicit_reducible]

instance TrinhHaida2015.instDecidableEqAW : DecidableEq AW

Equations

• TrinhHaida2015.instDecidableEqAW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TrinhHaida2015.instReprAW.repr : AW → ℕ → Std.Format

Equations

• TrinhHaida2015.instReprAW.repr TrinhHaida2015.AW.rs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TrinhHaida2015.AW.rs")).group prec✝
• TrinhHaida2015.instReprAW.repr TrinhHaida2015.AW.rns prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TrinhHaida2015.AW.rns")).group prec✝
• TrinhHaida2015.instReprAW.repr TrinhHaida2015.AW.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TrinhHaida2015.AW.s")).group prec✝
• TrinhHaida2015.instReprAW.repr TrinhHaida2015.AW.ns prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TrinhHaida2015.AW.ns")).group prec✝

@[implicit_reducible]

instance TrinhHaida2015.instReprAW : Repr AW

Equations

• TrinhHaida2015.instReprAW = { reprPrec := TrinhHaida2015.instReprAW.repr }

@[implicit_reducible]

instance TrinhHaida2015.instFintypeAW : Fintype AW

Equations

• TrinhHaida2015.instFintypeAW = { elems := { val := ↑TrinhHaida2015.AW.enumList, nodup := TrinhHaida2015.AW.enumList_nodup }, complete := TrinhHaida2015.instFintypeAW._proof_1 }

theorem TrinhHaida2015.run_valid_domain : isValidDomain TrinhHaida2015.awDomain✝ TrinhHaida2015.fATrun✝ TrinhHaida2015.ran✝ TrinhHaida2015.domainA✝ = true

A satisfies all three Conditions on A (27). Crucially, (27c) holds: neither "smoke" nor "¬smoke" is in BC({run, run ∧ ¬smoke}) because the 4-world domain distinguishes them from all Boolean combinations.

theorem TrinhHaida2015.run_exh_correct : Exhaustification.innocent.exh (Exhaustification.altsFromPreds TrinhHaida2015.domainA✝) (Exhaustification.predToFinset TrinhHaida2015.ran✝) = Exhaustification.predToFinset fun (w : AW) => TrinhHaida2015.ran✝ w && TrinhHaida2015.smoked✝ w

EXH(A)(run) = run ∧ smoke: the correct empirical inference. exhIE negates "run ∧ ¬smoke" (the only non-weaker alternative in A), deriving that John smoked.

theorem TrinhHaida2015.without_atomicity_vacuous : Exhaustification.innocent.exh (Exhaustification.altsFromPreds [TrinhHaida2015.ran✝, TrinhHaida2015.smoked✝, TrinhHaida2015.didntSmoke✝, TrinhHaida2015.ranNotSmoked✝, TrinhHaida2015.ranAndSmoked✝]) (Exhaustification.predToFinset TrinhHaida2015.ran✝) = Exhaustification.predToFinset TrinhHaida2015.ran✝

Symmetry Preserving

(41) Bill ate exactly three cookies. John (only) ate three cookies. *Inference: ¬[John ate exactly three cookies]

Atomicity is vacuous here (alternatives are derived by simple lexical substitution). The non-attested inference is blocked by Conditions on A (27c): "four" ∈ BC({three, exactly_three}), so excluding "four" from A is impossible, but including it creates symmetry.

inductive TrinhHaida2015.CW : Type

Three cookie worlds: ate exactly 3, 4, or 5.

• w3 : CW
• w4 : CW
• w5 : CW

@[implicit_reducible]

instance TrinhHaida2015.instDecidableEqCW : DecidableEq CW

Equations

• TrinhHaida2015.instDecidableEqCW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TrinhHaida2015.instReprCW.repr : CW → ℕ → Std.Format

Equations

• TrinhHaida2015.instReprCW.repr TrinhHaida2015.CW.w3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TrinhHaida2015.CW.w3")).group prec✝
• TrinhHaida2015.instReprCW.repr TrinhHaida2015.CW.w4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TrinhHaida2015.CW.w4")).group prec✝
• TrinhHaida2015.instReprCW.repr TrinhHaida2015.CW.w5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TrinhHaida2015.CW.w5")).group prec✝

@[implicit_reducible]

instance TrinhHaida2015.instReprCW : Repr CW

Equations

• TrinhHaida2015.instReprCW = { reprPrec := TrinhHaida2015.instReprCW.repr }

@[implicit_reducible]

instance TrinhHaida2015.instFintypeCW : Fintype CW

Equations

• TrinhHaida2015.instFintypeCW = { elems := { val := ↑TrinhHaida2015.CW.enumList, nodup := TrinhHaida2015.CW.enumList_nodup }, complete := TrinhHaida2015.instFintypeCW._proof_1 }

theorem TrinhHaida2015.four_in_bc : inBooleanClosure TrinhHaida2015.cwDomain✝ [TrinhHaida2015.three✝, TrinhHaida2015.exactlyThree✝] TrinhHaida2015.four✝ = true

"four" is in BC({three, exactly_three}): worlds agreeing on both "three" (always true) and "exactly_three" always agree on "four", because four ≡ three ∧ ¬exactly_three on this domain.

theorem TrinhHaida2015.restricted_domain_invalid : isValidDomain TrinhHaida2015.cwDomain✝ TrinhHaida2015.fCookies✝ TrinhHaida2015.three✝ [TrinhHaida2015.three✝, TrinhHaida2015.exactlyThree✝] = false

A = {three, exactly_three} violates (27c): "four" is excluded from A but is in BC(A).

theorem TrinhHaida2015.full_domain_valid : isValidDomain TrinhHaida2015.cwDomain✝ TrinhHaida2015.fCookies✝ TrinhHaida2015.three✝ TrinhHaida2015.fCookies✝ = true

A = F(S) = {three, exactly_three, four} satisfies (27).

theorem TrinhHaida2015.cookies_symmetric : Alternatives.Symmetric.isSymmetric TrinhHaida2015.cwDomain✝ TrinhHaida2015.three✝ TrinhHaida2015.exactlyThree✝ TrinhHaida2015.four✝ = true

"exactly_three" and "four" are symmetric alternatives of "three": they partition its denotation.

theorem TrinhHaida2015.cookies_exh_vacuous : Exhaustification.innocent.exh (Exhaustification.altsFromPreds TrinhHaida2015.fCookies✝) (Exhaustification.predToFinset TrinhHaida2015.three✝) = Exhaustification.predToFinset TrinhHaida2015.three✝

With A = F(S) (the only valid domain), exhIE is vacuous: the symmetric alternatives make exhaustification identity.

Switching Problem Constraints

For structures where a weak scalar item embeds a strong one (e.g., [some[all]]), Atomicity alone is insufficient. The paper adds three constraints on the derivation of formal alternatives:

(60a) Only non-AT-marked expressions are replaceable. (60b) The most deeply embedded replaceable expression must be replaced first (bottom-up). (60c) No replacement may yield a sentence logically weaker than the prejacent.

These constraints prevent "some" and "all" from switching places under negation while still allowing the correct indirect implicature derivation. (60a) is already captured by ATStructOp (no inChild into atNode). (60b) and (60c) are additional derivation-order and semantic monotonicity constraints:

def TrinhHaida2015.bottomUpOrdering (pos maxReplaceable : ℕ) : Prop

(60b) Bottom-up ordering: the replacement position must be at least as deeply embedded as any other replaceable position. Modeled as a property of a derivation step at position pos in a tree of depth maxDepth.

Equations

• TrinhHaida2015.bottomUpOrdering pos maxReplaceable = (pos ≥ maxReplaceable)

def TrinhHaida2015.nonWeakeningStep {W : Type} (domain : List W) (before after : W → Bool) : Bool

(60c) Semantic monotonicity: the result of a replacement step must not be logically weaker than the input (on the domain).

Equations

• TrinhHaida2015.nonWeakeningStep domain before after = ((!domain.any fun (w : W) => before w && !after w) || domain.any fun (w : W) => after w && !before w)