Jäger (2002): Some notes on the formal properties of bidirectional optimality theory

Jäger asks when Blutner's weak bidirection is well defined. The paper's Definition 1 is Blutner's mutual recursion between the Q- and the I-principle (BidirectionalOT.IsWeakSolution), which it calls z-optimality after the zigzag of its evaluation; Lemma 1 shows by the recursion theorem that a well-founded harmony ordering makes the solution unique. Definition 3 is the paper's own x-optimality: a pair is x-optimal iff it lies in the generator and no x-optimal pair blocks it along either axis, the fixed point of BidirectionalOT.unblockedSet. Theorem 2 shows that for a transitive well-founded ordering the x-optimality relation is unique and coincides with z-optimality. The worked example opening the paper's transducer construction shows that bidirectional optimality predicts iconicity.

This file proves Lemma 1 and Theorem 2 under the paper's hypotheses: the harmonies of the generator are well-founded, and the ordering is transitive because it is a preorder. The paper's Lemma 1 gives existence and uniqueness together by the recursion theorem; here existence is the substrate's hypothesis-free BidirectionalOT.exists_isWeakSolution and only uniqueness needs the descent. The first part of Theorem 2 uses minimality alone; the second part uses transitivity, as the paper does, where a form-axis blocker of a blocker is turned into a blocker.

Main statements

• isWeakSolution_unique: the weak version has at most one solution.
• existsUnique_isFixedPt: x-optimality is unique, and it is the substrate's superoptimalSet.
• inter_eq_superoptimalSet: the pairs satisfying both principles of a weak solution are exactly the x-optimal pairs.

TODO

• The paper's second part, bidirectional optimization by finite-state transducers, is formalized only in its opening example.

References

• [Jag02]
• [Blu00]

Lemma 1: uniqueness of the weak solution

theorem Jaeger2002.isWeakSolution_unique {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] {pairs : Set (F × M)} {f : F × M → α} (h : (f '' pairs).IsWF) {Q I Q' I' : Set (F × M)} (hQI : BidirectionalOT.IsWeakSolution pairs f Q I) (hQI' : BidirectionalOT.IsWeakSolution pairs f Q' I') : Q = Q' ∧ I = I'

When the harmonies of the generator are well-founded the weak version has at most one solution (Lemma 1). A minimal pair on which two solutions disagree would have a blocker on which they also disagree.

Theorem 2: x-optimality is unique and is z-optimality

theorem Jaeger2002.existsUnique_isFixedPt {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] {pairs : Set (F × M)} {f : F × M → α} (h : (f '' pairs).IsWF) : ∃! S : Set (F × M), Function.IsFixedPt (BidirectionalOT.unblockedSet pairs f) S

When the harmonies of the generator are well-founded there is exactly one x-optimality relation, the substrate's superoptimalSet (Theorem 2, first part).

theorem Jaeger2002.inter_eq_superoptimalSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] {pairs : Set (F × M)} {f : F × M → α} (h : (f '' pairs).IsWF) {Q I : Set (F × M)} (hQI : BidirectionalOT.IsWeakSolution pairs f Q I) : Q ∩ I = BidirectionalOT.superoptimalSet pairs f

The pairs satisfying both principles of a weak solution are the x-optimal pairs (Theorem 2, second part).

Iconicity

The worked example opening the paper's transducer construction: three inputs and three outputs ordered by cost, with the constraint "be small" on each side.

theorem Jaeger2002.superoptimalSet_eq_diagonal {α : Type u_3} [Preorder α] {g : Fin 3 × Fin 3 → α} (hg : StrictMono g) : BidirectionalOT.superoptimalSet Set.univ g = Set.diagonal (Fin 3)

With "be small" on inputs and on outputs, the bidirectionally optimal pairs are the diagonal: cheap inputs go with cheap outputs and expensive inputs with expensive outputs. This holds for the paper's ordering, the product order (strictMono_id), and for every other harmony strictly monotone in cost.