Blutner (2000): Some aspects of optimality in natural language interpretation

Blutner evaluates form-meaning pairs from the speaker's and the hearer's side at once (Pragmatics/Bidirectional.lean). His schematic tableaux pit an unmarked against a marked form and a stereotypical against a marked situation, under a constraint F against marked forms and a constraint C against marked situations. The results below hold for every harmony strictly monotone in the two markedness orders, so for either ranking of F and C, which the paper leaves open. Strong bidirection blocks the marked form in every interpretation and yields Horn's division of pragmatic labour only when the generator stipulates it; weak bidirection derives it.

For presupposition projection, AvoidA counts accommodated markers and BeStrong prefers stronger outcomes. Ranked in that order they select global accommodation when no binder is available, binding when the antecedent supplies one, and, where global accommodation is unavailable, the stronger local reading over the higher intermediate site that van der Sandt's and Geurts's preference would choose. The Q-principle blocks accommodation when a non-triggering alternative expresses the same outcome.

Main statements

• strong_total_blocking: strong bidirection blocks the marked form in every interpretation on any generator in which both forms can express the stereotypical situation.
• marked_marked_mem_strongOptimalSet_iff: strong bidirection pairs the marked form with the marked situation only if the generator excludes both mixed pairs.
• weak_division_of_labour: weak bidirection pairs the unmarked form with the stereotypical situation and the marked form with the marked one.
• strength_local_height_intermediate: without global accommodation, BeStrong selects the local reading where the higher-site preference selects the intermediate one.

Implementation notes

• The markedness orders on forms and situations are pulled back from the violations of F and C.
• BeStrong compares outcomes by entailment, as sets of worlds, so the harmony of a resolution is its AvoidA count followed lexicographically by its outcome.
• The quantified sentences of the paper's (19) and (20) are read through the conditional schema for one individual; global accommodation is left out of their generator because it would leave the bound marker free.

TODO

• The generalization (23), that a trigger does not accommodate iff it has a simple non-triggering alternative, as a theorem over generators in which AvoidA ranks first.

References

• [Blu00]
• [Hor84]
• [vdS92]
• [Geu95]
• [AL98]

Total blocking and the division of pragmatic labour

The schematic tableaux (7), (9), (10) and (12): an unmarked and a marked form, such as kill and cause to die, and a stereotypical and a marked situation.

inductive Blutner2000.Form : Type

The unmarked and the marked form.

• unmarked : Form
• marked : Form

@[instance_reducible]

instance Blutner2000.instDecidableEqForm : DecidableEq Form

Equations

• Blutner2000.instDecidableEqForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Blutner2000.instFintypeForm : Fintype Form

Equations

• Blutner2000.instFintypeForm = { elems := { val := ↑Blutner2000.Form.enumList, nodup := Blutner2000.Form.enumList_nodup }, complete := Blutner2000.instFintypeForm._proof_1 }

@[instance_reducible]

instance Blutner2000.instReprForm : Repr Form

Equations

• Blutner2000.instReprForm = { reprPrec := Blutner2000.instReprForm.repr }

def Blutner2000.instReprForm.repr : Form → ℕ → Std.Format

Equations

• Blutner2000.instReprForm.repr Blutner2000.Form.unmarked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Blutner2000.Form.unmarked")).group prec✝
• Blutner2000.instReprForm.repr Blutner2000.Form.marked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Blutner2000.Form.marked")).group prec✝

inductive Blutner2000.Situation : Type

The stereotypical and the marked situation.

• stereotypical : Situation
• marked : Situation

@[instance_reducible]

instance Blutner2000.instDecidableEqSituation : DecidableEq Situation

Equations

• Blutner2000.instDecidableEqSituation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Blutner2000.instFintypeSituation : Fintype Situation

Equations

• Blutner2000.instFintypeSituation = { elems := { val := ↑Blutner2000.Situation.enumList, nodup := Blutner2000.Situation.enumList_nodup }, complete := Blutner2000.instFintypeSituation._proof_1 }

@[instance_reducible]

instance Blutner2000.instReprSituation : Repr Situation

Equations

• Blutner2000.instReprSituation = { reprPrec := Blutner2000.instReprSituation.repr }

def Blutner2000.instReprSituation.repr : Situation → ℕ → Std.Format

Equations

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

def Blutner2000.Form.markedness : Form → ℕ

The violations of F, the constraint against marked forms.

Equations

• Blutner2000.Form.unmarked.markedness = 0
• Blutner2000.Form.marked.markedness = 1

def Blutner2000.Situation.markedness : Situation → ℕ

The violations of C, the constraint against marked situations.

Equations

• Blutner2000.Situation.stereotypical.markedness = 0
• Blutner2000.Situation.marked.markedness = 1

@[instance_reducible]

instance Blutner2000.instLinearOrderForm : LinearOrder Form

Equations

• Blutner2000.instLinearOrderForm = LinearOrder.lift' Blutner2000.Form.markedness Blutner2000.instLinearOrderForm._proof_1

@[instance_reducible]

instance Blutner2000.instLinearOrderSituation : LinearOrder Situation

Equations

• Blutner2000.instLinearOrderSituation = LinearOrder.lift' Blutner2000.Situation.markedness Blutner2000.instLinearOrderSituation._proof_1

theorem Blutner2000.strictMono_profile_markedness : StrictMono (BidirectionalOT.profile [fun (x : Form × Situation) => x.1.markedness, fun (x : Form × Situation) => x.2.markedness]) ∧ StrictMono (BidirectionalOT.profile [fun (x : Form × Situation) => x.2.markedness, fun (x : Form × Situation) => x.1.markedness])

The paper introduces no ranking between F and C, and none is needed, since the tableau under either ranking is strictly monotone in markedness, which is all the results below assume.

def Blutner2000.iconicity : Form ≃o Situation

The iconic pairing matches the unmarked form with the stereotypical situation and the marked form with the marked one, an isomorphism of the two markedness orders.

Equations

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

theorem Blutner2000.strong_total_blocking {α : Type u_1} [Preorder α] {f : Form × Situation → α} {G : Set (Form × Situation)} (hf : StrictMono f) (hu : (Form.unmarked, Situation.stereotypical) ∈ G) (hm : (Form.marked, Situation.stereotypical) ∈ G) : BidirectionalOT.strongOptimalSet G f = {(Form.unmarked, Situation.stereotypical)}

Strong bidirection blocks the marked form in every interpretation on any generator in which both forms can express the stereotypical situation, keeping only the unmarked form in its stereotypical reading. This covers the full generator (7) and the one that restricts the unmarked form to the stereotypical situation (9).

theorem Blutner2000.marked_marked_mem_strongOptimalSet_iff {α : Type u_1} [Preorder α] {f : Form × Situation → α} {G : Set (Form × Situation)} (hf : StrictMono f) : (Form.marked, Situation.marked) ∈ BidirectionalOT.strongOptimalSet G f ↔ (Form.marked, Situation.marked) ∈ G ∧ (Form.marked, Situation.stereotypical) ∉ G ∧ (Form.unmarked, Situation.marked) ∉ G

Strong bidirection pairs the marked form with the marked situation iff the generator excludes both mixed pairs: the only way to the division of labour under the strong version is to stipulate it in the generator, as in (10).

theorem Blutner2000.weak_division_of_labour {α : Type u_1} [Preorder α] {f : Form × Situation → α} (hf : StrictMono f) : BidirectionalOT.superoptimalSet Set.univ f = {(Form.unmarked, Situation.stereotypical), (Form.marked, Situation.marked)}

Weak bidirection derives the division of pragmatic labour (12), pairing the unmarked form with the stereotypical situation and the marked form with the marked one. The paper credits the general proof to Jäger; it is superoptimalSet_eq_graphOn.

theorem Blutner2000.strongOptimalSet_ssubset_superoptimalSet {α : Type u_1} [Preorder α] {f : Form × Situation → α} (hf : StrictMono f) : BidirectionalOT.strongOptimalSet Set.univ f ⊂ BidirectionalOT.superoptimalSet Set.univ f

The weak version admits the marked pair the strong version blocks.

Presupposition projection

A conditional "if p then q" whose consequent presupposes r, with the presupposition resolved locally, at the antecedent or globally (15), (16). The form is fixed, so each competition is an I-principle competition among the resolutions.

inductive Blutner2000.ProjectionSite : Type

The sites at which the presupposition can be resolved.

• local : ProjectionSite
• intermediate : ProjectionSite
• global : ProjectionSite

@[instance_reducible]

instance Blutner2000.instDecidableEqProjectionSite : DecidableEq ProjectionSite

Equations

• Blutner2000.instDecidableEqProjectionSite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Blutner2000.instFintypeProjectionSite : Fintype ProjectionSite

Equations

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

def Blutner2000.instReprProjectionSite.repr : ProjectionSite → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Blutner2000.instReprProjectionSite : Repr ProjectionSite

Equations

• Blutner2000.instReprProjectionSite = { reprPrec := Blutner2000.instReprProjectionSite.repr }

inductive Blutner2000.Atom : Type

The antecedent p, the consequent q and the presupposition r.

• p : Atom
• q : Atom
• r : Atom

@[instance_reducible]

instance Blutner2000.instDecidableEqAtom : DecidableEq Atom

Equations

• Blutner2000.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Blutner2000.instFintypeAtom : Fintype Atom

Equations

• Blutner2000.instFintypeAtom = { elems := { val := ↑Blutner2000.Atom.enumList, nodup := Blutner2000.Atom.enumList_nodup }, complete := Blutner2000.instFintypeAtom._proof_1 }

@[reducible, inline]

abbrev Blutner2000.World : Type

A world fixes the truth of the three atoms.

Equations

• Blutner2000.World = (Blutner2000.Atom → Bool)

def Blutner2000.ProjectionSite.projection : ProjectionSite → World → Prop

The proposition expressed with the presupposition resolved at the site.

Equations

• Blutner2000.ProjectionSite.global.projection = fun (w : Blutner2000.World) => w Blutner2000.Atom.r = true ∧ (w Blutner2000.Atom.p = true → w Blutner2000.Atom.q = true)
• Blutner2000.ProjectionSite.intermediate.projection = fun (w : Blutner2000.World) => w Blutner2000.Atom.r = true ∧ w Blutner2000.Atom.p = true → w Blutner2000.Atom.q = true
• Blutner2000.ProjectionSite.local.projection = fun (w : Blutner2000.World) => w Blutner2000.Atom.p = true → w Blutner2000.Atom.q = true ∧ w Blutner2000.Atom.r = true

@[instance_reducible]

instance Blutner2000.instDecidableProjection (s : ProjectionSite) (w : World) : Decidable (s.projection w)

Equations

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

def Blutner2000.ProjectionSite.outcome (worlds : Finset World) (s : ProjectionSite) : Finset World

The outcome of resolving at the site, the worlds of the context where its projection holds.

Equations

• Blutner2000.ProjectionSite.outcome worlds s = Finset.filter s.projection worlds

def Blutner2000.harmony (avoidA : ProjectionSite → ℕ) (worlds : Finset World) (p : Unit × ProjectionSite) : Lex (ℕ × Finset World)

The harmony of AvoidA ≫ BeStrong compares the number of accommodated markers, then the outcome, a stronger outcome being more harmonic.

Equations

• Blutner2000.harmony avoidA worlds p = toLex (avoidA p.2, Blutner2000.ProjectionSite.outcome worlds p.2)

@[instance_reducible]

def Blutner2000.instDecidableLTLexProdNatFinsetWorld : DecidableLT (Lex (ℕ × Finset World))

Equations

• Blutner2000.instDecidableLTLexProdNatFinsetWorld = Prod.Lex.decidable (fun (x1 x2 : ℕ) => x1 < x2) fun (x1 x2 : Finset Blutner2000.World) => x1 ⊂ x2

"If Peter has a dog, then his cat is gray" (15), (17)

No binder is available, so every site accommodates Peter's cat and BeStrong decides.

theorem Blutner2000.dog_outcome_ssubset : ProjectionSite.outcome Finset.univ ProjectionSite.global ⊂ ProjectionSite.outcome Finset.univ ProjectionSite.local ∧ ProjectionSite.outcome Finset.univ ProjectionSite.local ⊂ ProjectionSite.outcome Finset.univ ProjectionSite.intermediate

In (17) the global outcome is the strongest and the intermediate one the weakest.

theorem Blutner2000.dog_global_accommodation : BidirectionalOT.superoptimal Finset.univ (harmony (fun (x : ProjectionSite) => 1) Finset.univ) = {((), ProjectionSite.global)}

"If Peter has a cat, then his cat is gray" (16), (18)

The antecedent is the presupposition, so the intermediate site binds Peter's cat.

def Blutner2000.catWorlds : Finset World

The worlds of the cat conditional, where the antecedent is the presupposition.

Equations

• Blutner2000.catWorlds = {w : Blutner2000.World | w Blutner2000.Atom.p = w Blutner2000.Atom.r}

def Blutner2000.catAvoidA : ProjectionSite → ℕ

Only the intermediate site binds the presupposition.

Equations

• Blutner2000.catAvoidA Blutner2000.ProjectionSite.intermediate = 0
• Blutner2000.catAvoidA x✝ = 1

theorem Blutner2000.cat_outcome : ProjectionSite.outcome catWorlds ProjectionSite.global ⊂ ProjectionSite.outcome catWorlds ProjectionSite.intermediate ∧ ProjectionSite.outcome catWorlds ProjectionSite.local = ProjectionSite.outcome catWorlds ProjectionSite.intermediate

In (18) the global outcome is stronger than the intermediate one, and the local and intermediate outcomes coincide, as the paper's footnote notes.

theorem Blutner2000.cat_intermediate_binding : BidirectionalOT.superoptimal Finset.univ (harmony catAvoidA catWorlds) = {((), ProjectionSite.intermediate)}

"Every team member will come to the match in her car" (19), (20)

Global accommodation would leave the bound marker free, so only the local and intermediate sites compete, and both accommodate. Strength selects the local reading, "every team member owns a car and will come in it", where a preference for the higher site selects the intermediate reading, "every team member who owns a car will come in it".

def Blutner2000.boundSites : Finset (Unit × ProjectionSite)

The resolutions of a presupposition with a bound marker.

Equations

• Blutner2000.boundSites = {((), Blutner2000.ProjectionSite.local), ((), Blutner2000.ProjectionSite.intermediate)}

def Blutner2000.ProjectionSite.depth : ProjectionSite → ℕ

The depth of a site below the main context, which the higher-site preference minimizes.

Equations

• Blutner2000.ProjectionSite.global.depth = 0
• Blutner2000.ProjectionSite.intermediate.depth = 1
• Blutner2000.ProjectionSite.local.depth = 2

theorem Blutner2000.strength_local_height_intermediate : BidirectionalOT.superoptimal boundSites (harmony (fun (x : ProjectionSite) => 1) Finset.univ) = {((), ProjectionSite.local)} ∧ BidirectionalOT.superoptimal boundSites (BidirectionalOT.profile [fun (x : Unit × ProjectionSite) => 1, fun (x : Unit × ProjectionSite) => x.2.depth]) = {((), ProjectionSite.intermediate)}

Accommodation blocked by the Q-principle (22)

"He had an accident. A car hit him." against "He had an accident. ??The car hit him.": from a context neutral about cars both continuations have the same outcome, but only the definite accommodates.

inductive Blutner2000.Article : Type

The presuppositional definite and its non-triggering indefinite alternative.

• definite : Article
• indefinite : Article

@[instance_reducible]

instance Blutner2000.instDecidableEqArticle : DecidableEq Article

Equations

• Blutner2000.instDecidableEqArticle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Blutner2000.instFintypeArticle : Fintype Article

Equations

• Blutner2000.instFintypeArticle = { elems := { val := ↑Blutner2000.Article.enumList, nodup := Blutner2000.Article.enumList_nodup }, complete := Blutner2000.instFintypeArticle._proof_1 }

def Blutner2000.instReprArticle.repr : Article → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Blutner2000.instReprArticle : Repr Article

Equations

• Blutner2000.instReprArticle = { reprPrec := Blutner2000.instReprArticle.repr }

def Blutner2000.accidentAvoidA : Article × Unit → ℕ

AvoidA penalizes the definite, which accommodates the car, and not the indefinite, which introduces it.

Equations

• Blutner2000.accidentAvoidA (Blutner2000.Article.definite, snd) = 1
• Blutner2000.accidentAvoidA (Blutner2000.Article.indefinite, snd) = 0

theorem Blutner2000.accommodation_blocked : BidirectionalOT.superoptimal Finset.univ accidentAvoidA = {(Article.indefinite, ())}

theorem Blutner2000.accommodation_blocked_is_Q : BidirectionalOT.QBlocks accidentAvoidA ↑Finset.univ (Article.definite, ())

The blocking is a Q-principle effect: a form with the same outcome needs no accommodation.