Documentation

Linglib.Theories.Pragmatics.Bidirectional

Bidirectional Optimality Theory #

@cite{blutner-2000} @cite{horn-1984} @cite{atlas-levinson-1981}

Bidirectional OT integrates production and comprehension optimality into a single framework. The key insight is that the Gricean maxims decompose into two opposing optimization pressures:

Q-principle (production optimality): for a given meaning τ, the optimal form A is the one that produces ⟨A, τ⟩ most harmonically. Blocking mechanism: suppresses interpretations that can be expressed more economically by an alternative form. Corresponds to the first part of Grice's Quantity maxim ("be as informative as required") and the force of diversification / auditor's economy (@cite{atlas-levinson-1981}, @cite{horn-1984}).
I-principle (comprehension optimality): for a given form A, the optimal meaning τ is the one that produces ⟨A, τ⟩ most harmonically. Interpretation mechanism: selects the most coherent/stereotypical reading. Corresponds to the second part of Grice's Quantity maxim ("do not make your contribution more informative than required"), Relation, Manner, and the force of unification / speaker's economy (@cite{atlas-levinson-1981}, @cite{horn-1984}'s R-principle).

These correspond to the speaker/hearer optimization layers in RSA (@cite{frank-goodman-2012}) and IBR (@cite{franke-2011}).

Strong vs Weak BiOT #

@cite{blutner-2000} defines two versions:

Strong (eq. 9): Q and I are independent — ⟨A, τ⟩ is optimal iff it survives BOTH Q and I evaluated against the full candidate set. Solution concept: Nash Equilibrium.
Weak (eq. 14): Q and I mutually constrain each other — competition under Q is restricted to I-surviving pairs, and vice versa. Solution concept: greatest fixed point of the blocking operator.

The weak version derives @cite{horn-1984}'s division of pragmatic labour: unmarked forms pair with unmarked (stereotypical) meanings, and marked forms pair with marked (non-stereotypical) meanings. The strong version incorrectly predicts that marked forms are blocked in ALL their interpretations.

Connection to RSA and IBR #

All three frameworks — BiOT, IBR, RSA — perform alternating speaker/hearer optimization. They differ in the optimization criterion:

Framework	Comparison	Solution
Strong BiOT	lexicographic (OT)	Nash equilibrium
Weak BiOT	lexicographic (OT)	greatest fixed point
IBR	argmax (set-level)	iterated best response
RSA	softmax (probabilistic)	Bayesian posterior

The relationship: RSA α→∞ approximates IBR, and IBR fixed points correspond to weak-BiOT super-optimal pairs for scalar games (see IBR/ScalarGames.lean).

def Theories.Pragmatics.Bidirectional.satisfiesQ {F M : Type} [BEq F] [BEq M] (gen : List (F × M)) (profile : F × M → List Nat) (p : F × M) :

Q-principle (production optimality, @cite{blutner-2000} eq. 9(Q)): ⟨A, τ⟩ satisfies Q iff no other pair with the same meaning τ but a different form A' is strictly more harmonic.

Operationally: the speaker chose A because it is the best way to express τ. If a better form A' existed, A would be blocked. This is the blocking mechanism — it suppresses interpretations that can be triggered more economically by an alternative form (@cite{horn-1984}'s Q-based implicature).

Equations

Theories.Pragmatics.Bidirectional.satisfiesQ gen profile p = !gen.any fun (q : F × M) => !q.fst == p.fst && q.snd == p.snd && Core.ConstraintEvaluation.lexLT (profile q) (profile p)

Instances For

def Theories.Pragmatics.Bidirectional.satisfiesI {F M : Type} [BEq F] [BEq M] (gen : List (F × M)) (profile : F × M → List Nat) (p : F × M) :

I-principle (comprehension optimality, @cite{blutner-2000} eq. 9(I)): ⟨A, τ⟩ satisfies I iff no other pair with the same form A but a different meaning τ' is strictly more harmonic.

Operationally: the hearer chose τ because it is the best interpretation of A. If a better meaning τ' existed, τ would be dispreferred. This is the interpretation mechanism — it selects the most coherent/stereotypical reading (@cite{horn-1984}'s R-based inference).

Equations

Theories.Pragmatics.Bidirectional.satisfiesI gen profile p = !gen.any fun (q : F × M) => q.fst == p.fst && !q.snd == p.snd && Core.ConstraintEvaluation.lexLT (profile q) (profile p)

Instances For

theorem Theories.Pragmatics.Bidirectional.strongOptimal_eq_both {F M : Type} [BEq F] [BEq M] (pairs : List (F × M)) (profile : F × M → List Nat) :

Core.ConstraintEvaluation.strongOptimal pairs profile = List.filter (fun (p : F × M) => satisfiesQ pairs profile p && satisfiesI pairs profile p) pairs

Strong-optimal = satisfies BOTH Q and I against the full candidate set. This is equivalent to strongOptimal in ConstraintEvaluation.

@cite{horn-1984}'s division of pragmatic labour: "unmarked forms tend to be used for unmarked situations and marked forms for marked situations." This emerges naturally from weak BiOT but NOT from strong BiOT. The example below formalizes @cite{blutner-2000}'s tableau (15).

Classic examples:
- kill (unmarked) / cause to die (marked): kill ↔ stereotypical
  causation (direct), cause to die ↔ non-stereotypical (indirect)
- pork (unmarked) / pig-meat (marked, blocked): pork ↔ meat reading,
  pig ↔ animal reading — *pig-meat is totally blocked because pork
  exists
- him (unmarked) / himself (marked): himself ↔ coreferential,
  him ↔ disjoint reference

inductive Theories.Pragmatics.Bidirectional.HornForm :

Forms in Horn's division example.

unmarked : HornForm
marked : HornForm

Instances For

instance Theories.Pragmatics.Bidirectional.instDecidableEqHornForm :

DecidableEq HornForm

Equations

Theories.Pragmatics.Bidirectional.instDecidableEqHornForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Theories.Pragmatics.Bidirectional.instBEqHornForm :

Equations

Theories.Pragmatics.Bidirectional.instBEqHornForm = { beq := Theories.Pragmatics.Bidirectional.instBEqHornForm.beq }

def Theories.Pragmatics.Bidirectional.instBEqHornForm.beq :

HornForm → HornForm → Bool

Equations

Theories.Pragmatics.Bidirectional.instBEqHornForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Theories.Pragmatics.Bidirectional.instReprHornForm :

Equations

Theories.Pragmatics.Bidirectional.instReprHornForm = { reprPrec := Theories.Pragmatics.Bidirectional.instReprHornForm.repr }

def Theories.Pragmatics.Bidirectional.instReprHornForm.repr :

HornForm → Nat → Std.Format

Equations

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

Instances For

inductive Theories.Pragmatics.Bidirectional.HornMeaning :

Meanings in Horn's division example.

stereotypical : HornMeaning
nonStereotypical : HornMeaning

Instances For

instance Theories.Pragmatics.Bidirectional.instDecidableEqHornMeaning :

DecidableEq HornMeaning

Equations

Theories.Pragmatics.Bidirectional.instDecidableEqHornMeaning x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Theories.Pragmatics.Bidirectional.instBEqHornMeaning :

BEq HornMeaning

Equations

Theories.Pragmatics.Bidirectional.instBEqHornMeaning = { beq := Theories.Pragmatics.Bidirectional.instBEqHornMeaning.beq }

def Theories.Pragmatics.Bidirectional.instBEqHornMeaning.beq :

HornMeaning → HornMeaning → Bool

Equations

Theories.Pragmatics.Bidirectional.instBEqHornMeaning.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Theories.Pragmatics.Bidirectional.instReprHornMeaning.repr :

HornMeaning → Nat → Std.Format

Equations

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

Instances For

instance Theories.Pragmatics.Bidirectional.instReprHornMeaning :

Repr HornMeaning

Equations

Theories.Pragmatics.Bidirectional.instReprHornMeaning = { reprPrec := Theories.Pragmatics.Bidirectional.instReprHornMeaning.repr }

def Theories.Pragmatics.Bidirectional.hornPairs :

List (HornForm × HornMeaning)

All form-meaning pairs (forms are semantically equivalent).

Equations

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

Instances For

def Theories.Pragmatics.Bidirectional.hornProfile :

HornForm × HornMeaning → List Nat

Constraint profile: [F-violations, C-violations]. F penalizes marked forms; C penalizes non-stereotypical meanings.

Equations

Instances For

theorem Theories.Pragmatics.Bidirectional.horn_weak_biot :

Core.ConstraintEvaluation.superoptimal hornPairs hornProfile = [(HornForm.unmarked , HornMeaning.stereotypical ), (HornForm.marked , HornMeaning.nonStereotypical )]

Weak BiOT derives Horn's division: unmarked ↔ stereotypical, marked ↔ non-stereotypical. Both pairs survive.

theorem Theories.Pragmatics.Bidirectional.horn_strong_biot :

Core.ConstraintEvaluation.strongOptimal hornPairs hornProfile = [(HornForm.unmarked , HornMeaning.stereotypical )]

Strong BiOT blocks the marked form entirely — only the unmarked pair survives. This is empirically wrong: marked forms DO get used (for marked meanings).

theorem Theories.Pragmatics.Bidirectional.weak_strictly_larger :

(Core.ConstraintEvaluation.superoptimal hornPairs hornProfile).length > (Core.ConstraintEvaluation.strongOptimal hornPairs hornProfile).length

The weak version admits strictly MORE pairs than the strong version for this case. This is the key empirical argument for weak BiOT.

When an unmarked form has a SPECIALIZED meaning (not semantically equivalent to the marked form), the marked form can be totally blocked — it loses ALL its interpretations.

Example: pork (= pig-meat) blocks *pig in the meat reading.
Unlike Horn's division, here the unmarked form doesn't compete
for the non-stereotypical meaning because Gen doesn't pair them.

inductive Theories.Pragmatics.Bidirectional.LexForm :

Forms for total blocking: a listed (lexicalized) form and a derived (productive) form.

listed : LexForm
derived : LexForm

Instances For

instance Theories.Pragmatics.Bidirectional.instDecidableEqLexForm :

DecidableEq LexForm

Equations

Theories.Pragmatics.Bidirectional.instDecidableEqLexForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Theories.Pragmatics.Bidirectional.instBEqLexForm :

Equations

Theories.Pragmatics.Bidirectional.instBEqLexForm = { beq := Theories.Pragmatics.Bidirectional.instBEqLexForm.beq }

def Theories.Pragmatics.Bidirectional.instBEqLexForm.beq :

LexForm → LexForm → Bool

Equations

Theories.Pragmatics.Bidirectional.instBEqLexForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Theories.Pragmatics.Bidirectional.instReprLexForm :

Equations

Theories.Pragmatics.Bidirectional.instReprLexForm = { reprPrec := Theories.Pragmatics.Bidirectional.instReprLexForm.repr }

def Theories.Pragmatics.Bidirectional.instReprLexForm.repr :

LexForm → Nat → Std.Format

Equations

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

Instances For

inductive Theories.Pragmatics.Bidirectional.LexMeaning :

Meanings for total blocking.

specialized : LexMeaning
general : LexMeaning

Instances For

instance Theories.Pragmatics.Bidirectional.instDecidableEqLexMeaning :

DecidableEq LexMeaning

Equations

Theories.Pragmatics.Bidirectional.instDecidableEqLexMeaning x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Theories.Pragmatics.Bidirectional.instBEqLexMeaning.beq :

LexMeaning → LexMeaning → Bool

Equations

Theories.Pragmatics.Bidirectional.instBEqLexMeaning.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Theories.Pragmatics.Bidirectional.instBEqLexMeaning :

Equations

Theories.Pragmatics.Bidirectional.instBEqLexMeaning = { beq := Theories.Pragmatics.Bidirectional.instBEqLexMeaning.beq }

instance Theories.Pragmatics.Bidirectional.instReprLexMeaning :

Repr LexMeaning

Equations

Theories.Pragmatics.Bidirectional.instReprLexMeaning = { reprPrec := Theories.Pragmatics.Bidirectional.instReprLexMeaning.repr }

def Theories.Pragmatics.Bidirectional.instReprLexMeaning.repr :

LexMeaning → Nat → Std.Format

Equations

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

Instances For

def Theories.Pragmatics.Bidirectional.totalBlockPairs :

List (LexForm × LexMeaning)

Gen for total blocking: the listed form only covers the specialized meaning; the derived form covers both meanings.

Equations

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

Instances For

def Theories.Pragmatics.Bidirectional.totalBlockProfile :

LexForm × LexMeaning → List Nat

Profile: listed form is less marked (0 F-violations); specialized meaning is less marked (0 C-violations).

Equations

Instances For

theorem Theories.Pragmatics.Bidirectional.total_blocking_weak :

Core.ConstraintEvaluation.superoptimal totalBlockPairs totalBlockProfile = [(LexForm.listed , LexMeaning.specialized ), (LexForm.derived , LexMeaning.general )]

Total blocking: the derived form loses the specialized meaning (blocked by the listed form) but retains the general meaning. Result: listed ↔ specialized, derived ↔ general.

theorem Theories.Pragmatics.Bidirectional.total_blocking_strong :

Core.ConstraintEvaluation.strongOptimal totalBlockPairs totalBlockProfile = [(LexForm.listed , LexMeaning.specialized )]

Strong BiOT over-blocks: the derived form loses ALL interpretations because (.derived, .specialized) is I-better than (.derived, .general) under the same form. This makes strong BiOT too aggressive for partial blocking — only the listed form survives.

theorem Theories.Pragmatics.Bidirectional.total_blocking_weak_vs_strong :

(Core.ConstraintEvaluation.superoptimal totalBlockPairs totalBlockProfile).length > (Core.ConstraintEvaluation.strongOptimal totalBlockPairs totalBlockProfile).length

Weak BiOT correctly handles partial blocking — the derived form keeps the general meaning because its I-competitor (.derived, .specialized) was removed by Q-blocking from (.listed, .specialized).

theorem Theories.Pragmatics.Bidirectional.strongOptimal_satisfies_Q {F M : Type} [BEq F] [BEq M] (pairs : List (F × M)) (profile : F × M → List Nat) (p : F × M) (hp : p ∈ Core.ConstraintEvaluation.strongOptimal pairs profile) :

satisfiesQ pairs profile p = true

Every strong-optimal pair satisfies Q against the full set.

theorem Theories.Pragmatics.Bidirectional.strongOptimal_satisfies_I {F M : Type} [BEq F] [BEq M] (pairs : List (F × M)) (profile : F × M → List Nat) (p : F × M) (hp : p ∈ Core.ConstraintEvaluation.strongOptimal pairs profile) :

satisfiesI pairs profile p = true

Every strong-optimal pair satisfies I against the full set.

theorem Theories.Pragmatics.Bidirectional.strongOptimal_not_blocked {F M : Type} [BEq F] [BEq M] (pairs : List (F × M)) (profile : F × M → List Nat) (p : F × M) (hp : p ∈ Core.ConstraintEvaluation.strongOptimal pairs profile) :

Core.ConstraintEvaluation.blocked profile pairs p = false

theorem Theories.Pragmatics.Bidirectional.strong_subset_weak {F M : Type} [BEq F] [BEq M] (pairs : List (F × M)) (profile : F × M → List Nat) (p : F × M) (hp : p ∈ Core.ConstraintEvaluation.strongOptimal pairs profile) :

p ∈ Core.ConstraintEvaluation.superoptimal pairs profile

@cite{blutner-2000} p. 12: "It is simple to prove that a pair which is optimal (strong bidirection), is super-optimal (weak bidirection) as well." Strong-optimal is a subset of super-optimal.

theorem Theories.Pragmatics.Bidirectional.strong_strict_subset_weak_horn :

(Core.ConstraintEvaluation.strongOptimal hornPairs hornProfile).length < (Core.ConstraintEvaluation.superoptimal hornPairs hornProfile).length

Horn's division demonstrates strong ⊂ weak (strict inclusion): the marked pair survives weak but not strong BiOT.

theorem Theories.Pragmatics.Bidirectional.iterative_eq_strong_horn :

Core.ConstraintEvaluation.iterativeSuperoptimal hornPairs hornProfile = Core.ConstraintEvaluation.strongOptimal hornPairs hornProfile

The iterative-removal algorithm (iterativeSuperoptimal) agrees with strong BiOT for Horn's division. This shows that iterative removal over-removes: it behaves like the strong version (eq. 9), not the weak version (eq. 14).

theorem Theories.Pragmatics.Bidirectional.iterative_eq_strong_totalBlock :

Core.ConstraintEvaluation.iterativeSuperoptimal totalBlockPairs totalBlockProfile = Core.ConstraintEvaluation.strongOptimal totalBlockPairs totalBlockProfile

The iterative-removal algorithm agrees with strong BiOT for total blocking as well.