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. Substrate: strongOptimal (Finset, computable) + IsStrongOptimal (Set-valued Prop).
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. Substrate: superoptimal (Finset, computable) + superoptimalSet (Set-valued, anchored in mathlib's OrderHom.gfp).

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 (marked) meanings. The strong version incorrectly predicts that marked forms are blocked in ALL their interpretations.

The structural meta-theorem strong ⊂ weak (@cite{blutner-2000} p. 12) lives in Core/Constraint/Evaluation/Superoptimal.lean as isStrongOptimal_imp_mem_superoptimalSet (Set-valued, coinductive proof against OrderHom.gfp) and its Finset corollary strongOptimal_subset_superoptimal.

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

These are List-Bool versions of the per-pair Q and I checks, used by consumer studies (e.g. Blutner2000.lean's accommodation_blocked_is_Q) that want to check Q or I in isolation rather than the conjunction. The relationship to the substrate's Set-valued Blocks predicate:

`¬ Blocks profile S p ↔ (no Q-blocker in S for p) ∧ (no I-blocker in S for p)`

where Q-blocker = same meaning, different form; I-blocker = same form,
different meaning. So `satisfiesQ` and `satisfiesI` together pin down the
`¬ Blocks` condition that defines `IsStrongOptimal` and (via the gfp)
`superoptimalSet`.