Bidirectional Optimality Theory

Bidirectional optimality theory evaluates a form-meaning pair of a generator from the speaker's and the hearer's side at once. Another pair blocks it when it is more harmonic and shares its meaning (the Q-principle, production) or its form (the I-principle, comprehension). Under strong bidirection a pair is optimal when no pair of the generator blocks it; under weak bidirection it is super-optimal when no super-optimal pair blocks it, a fixed point of the blocking step.

Main definitions

• profile: the violation profile of a ranking, compared lexicographically.
• QBlocks, IBlocks, Blocks: a set of pairs blocks a pair along the meaning axis, the form axis, or either.
• unblockedSet pairs f S: the pairs of pairs that S does not block, an antitone step; strongOptimalSet is its value at pairs.
• superoptimalSet: the greatest fixed point of the square of the step.
• IsWeakSolution: a solution of Blutner's mutual recursion of the two principles.
• unblocked, strongOptimal, superoptimal: the computable Finset forms.

Main results

• mem_superoptimalSet: when the harmonies of the generator are well-founded, a pair is super-optimal iff it lies in the generator and no super-optimal pair blocks it, and superoptimalSet is the only such set.
• strongOptimalSet_subset_superoptimalSet: optimal pairs are super-optimal.
• superoptimalSet_eq_graphOn: the division of pragmatic labour. On a generator containing the graph of an isomorphism between the markedness orders of forms and of meanings, the super-optimal pairs are that graph, under every harmony strictly monotone in markedness.
• coe_superoptimal: the Finset iteration computes superoptimalSet.

Implementation notes

• The harmony is any preorder reached through f, such as profile into the lexicographic order on List ℕ. The principles' "other pair" clause is dropped, since f q < f p already forces q ≠ p.
• The step is antitone, so its square has a greatest fixed point without further hypotheses, and the step exchanges it with the least one. The two coincide by descent along a minimal pair of their difference when the harmonies of the generator are well-founded, Jäger's hypothesis, which every finite generator meets (Set.Finite.isWF).
• The Finset form iterates the squared step from pairs with pairs.card as fuel and an early exit, so it needs no convergence hypothesis and decide stays shallow.
• Jäger's uniqueness of weak solutions and their agreement with superoptimalSet are proved in Studies/Jaeger2002.lean.

References

• [Blu00]
• [Jag02]
• [Hor84]
• [AL81]

def BidirectionalOT.profile {F : Type u_1} {M : Type u_2} (ranking : List (F × M → ℕ)) (p : F × M) : List ℕ

The violation profile of a ranking lists a pair's violations from the dominant constraint down, to be compared lexicographically.

Equations

• BidirectionalOT.profile ranking p = List.map (fun (x : F × M → ℕ) => x p) ranking

theorem BidirectionalOT.strictMono_profile {F : Type u_1} {M : Type u_2} [Preorder F] [Preorder M] {ranking : List (F × M → ℕ)} (hmono : ∀ c ∈ ranking, Monotone c) (hsep : ∀ ⦃p q : F × M⦄, p < q → ∃ c ∈ ranking, c p < c q) : StrictMono (profile ranking)

A ranking of constraints that each penalize the more marked pair gives a strictly monotone profile once every strictly less marked pair does strictly better on some constraint.

Blocking

def BidirectionalOT.QBlocks {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (f : F × M → α) (S : Set (F × M)) (p : F × M) : Prop

QBlocks f S p holds when a more harmonic pair of S expresses p's meaning.

Equations

• BidirectionalOT.QBlocks f S p = ∃ q ∈ S, q.2 = p.2 ∧ f q < f p

def BidirectionalOT.IBlocks {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (f : F × M → α) (S : Set (F × M)) (p : F × M) : Prop

IBlocks f S p holds when a more harmonic pair of S interprets p's form.

Equations

• BidirectionalOT.IBlocks f S p = ∃ q ∈ S, q.1 = p.1 ∧ f q < f p

def BidirectionalOT.Blocks {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (f : F × M → α) (S : Set (F × M)) (p : F × M) : Prop

Blocks f S p holds when a more harmonic pair of S shares p's form or meaning.

Equations

• BidirectionalOT.Blocks f S p = ∃ q ∈ S, (q.1 = p.1 ∨ q.2 = p.2) ∧ f q < f p

theorem BidirectionalOT.blocks_iff_blocked {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (f : F × M → α) (S : Set (F × M)) (p : F × M) : Blocks f S p ↔ Competition.Blocked (fun (p : F × M) => {q : F × M | q ∈ S ∧ (q.1 = p.1 ∨ q.2 = p.2)}) f p

Bidirectional blocking is competition among the pairs of S that share a form or a meaning.

theorem BidirectionalOT.blocks_iff {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (f : F × M → α) (S : Set (F × M)) (p : F × M) : Blocks f S p ↔ IBlocks f S p ∨ QBlocks f S p

theorem BidirectionalOT.QBlocks.mono {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] {f : F × M → α} {S : Set (F × M)} {p : F × M} {T : Set (F × M)} (hST : S ⊆ T) : QBlocks f S p → QBlocks f T p

theorem BidirectionalOT.IBlocks.mono {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] {f : F × M → α} {S : Set (F × M)} {p : F × M} {T : Set (F × M)} (hST : S ⊆ T) : IBlocks f S p → IBlocks f T p

theorem BidirectionalOT.Blocks.mono {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] {f : F × M → α} {S : Set (F × M)} {p : F × M} {T : Set (F × M)} (hST : S ⊆ T) : Blocks f S p → Blocks f T p

@[instance_reducible]

instance BidirectionalOT.instDecidableQBlocksCoeFinsetProdOfDecidableEq {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (f : F × M → α) (p : F × M) [DecidableLT α] (S : Finset (F × M)) [DecidableEq M] : Decidable (QBlocks f (↑S) p)

Equations

• BidirectionalOT.instDecidableQBlocksCoeFinsetProdOfDecidableEq f p S = decidable_of_iff (∃ q ∈ S, q.2 = p.2 ∧ f q < f p) ⋯

@[instance_reducible]

instance BidirectionalOT.instDecidableIBlocksCoeFinsetProdOfDecidableEq {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (f : F × M → α) (p : F × M) [DecidableLT α] (S : Finset (F × M)) [DecidableEq F] : Decidable (IBlocks f (↑S) p)

Equations

• BidirectionalOT.instDecidableIBlocksCoeFinsetProdOfDecidableEq f p S = decidable_of_iff (∃ q ∈ S, q.1 = p.1 ∧ f q < f p) ⋯

@[instance_reducible]

instance BidirectionalOT.instDecidableBlocksCoeFinsetProdOfDecidableEq {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (f : F × M → α) (p : F × M) [DecidableLT α] (S : Finset (F × M)) [DecidableEq F] [DecidableEq M] : Decidable (Blocks f (↑S) p)

Equations

• BidirectionalOT.instDecidableBlocksCoeFinsetProdOfDecidableEq f p S = decidable_of_iff (∃ q ∈ S, (q.1 = p.1 ∨ q.2 = p.2) ∧ f q < f p) ⋯

The blocking step and its fixed points

def BidirectionalOT.unblockedSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) (S : Set (F × M)) : Set (F × M)

The pairs of pairs that S does not block. Antitone in S.

Equations

• BidirectionalOT.unblockedSet pairs f S = {p : F × M | p ∈ pairs ∧ ¬BidirectionalOT.Blocks f S p}

@[simp]

theorem BidirectionalOT.mem_unblockedSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) {S : Set (F × M)} {p : F × M} : p ∈ unblockedSet pairs f S ↔ p ∈ pairs ∧ ¬Blocks f S p

theorem BidirectionalOT.unblockedSet_subset {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) {S : Set (F × M)} : unblockedSet pairs f S ⊆ pairs

theorem BidirectionalOT.unblockedSet_antitone {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) : Antitone (unblockedSet pairs f)

def BidirectionalOT.strongOptimalSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) : Set (F × M)

Strong bidirection keeps the pairs that no pair of pairs blocks.

Equations

• BidirectionalOT.strongOptimalSet pairs f = BidirectionalOT.unblockedSet pairs f pairs

def BidirectionalOT.unblockedSq {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) : Set (F × M) →o Set (F × M)

The square of the blocking step, monotone as the composite of two antitone maps.

Equations

• BidirectionalOT.unblockedSq pairs f = { toFun := BidirectionalOT.unblockedSet pairs f ∘ BidirectionalOT.unblockedSet pairs f, monotone' := ⋯ }

@[simp]

theorem BidirectionalOT.unblockedSq_apply {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) (S : Set (F × M)) : (unblockedSq pairs f) S = unblockedSet pairs f (unblockedSet pairs f S)

noncomputable def BidirectionalOT.superoptimalSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) : Set (F × M)

The super-optimal pairs, the greatest fixed point of the squared blocking step. When the harmonies of the generator are well-founded it is the unique fixed point of the step itself (isFixedPt_superoptimalSet, eq_superoptimalSet_of_isFixedPt), Jäger's reformulation.

Equations

• BidirectionalOT.superoptimalSet pairs f = OrderHom.gfp (BidirectionalOT.unblockedSq pairs f)

theorem BidirectionalOT.superoptimalSet_subset {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) : superoptimalSet pairs f ⊆ pairs

theorem BidirectionalOT.strongOptimalSet_subset_superoptimalSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) : strongOptimalSet pairs f ⊆ superoptimalSet pairs f

Optimal pairs are super-optimal, since strongOptimalSet is a post-fixed point of the squared step, since the step is antitone and lands in pairs.

theorem BidirectionalOT.unblockedSet_superoptimalSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) : unblockedSet pairs f (superoptimalSet pairs f) = OrderHom.lfp (unblockedSq pairs f)

The step exchanges the greatest and least fixed points of its square.

theorem BidirectionalOT.lfp_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) : OrderHom.lfp (unblockedSq pairs f) = superoptimalSet pairs f

When the harmonies of the generator are well-founded, the least and greatest fixed points of the squared step coincide, since a minimal pair of their difference would be blocked by a still smaller one.

theorem BidirectionalOT.isFixedPt_superoptimalSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) (h : (f '' pairs).IsWF) : Function.IsFixedPt (unblockedSet pairs f) (superoptimalSet pairs f)

theorem BidirectionalOT.mem_superoptimalSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) {p : F × M} (h : (f '' pairs).IsWF) : p ∈ superoptimalSet pairs f ↔ p ∈ pairs ∧ ¬Blocks f (superoptimalSet pairs f) p

A pair is super-optimal iff it lies in the generator and no super-optimal pair blocks it, Jäger's reformulation of super-optimality.

theorem BidirectionalOT.eq_superoptimalSet_of_isFixedPt {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) {S : Set (F × M)} (h : (f '' pairs).IsWF) (hS : Function.IsFixedPt (unblockedSet pairs f) S) : S = superoptimalSet pairs f

When the harmonies of the generator are well-founded, the blocking step has no fixed point but the super-optimal set.

Blutner's mutual recursion

def BidirectionalOT.qUnblockedSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) (S : Set (F × M)) : Set (F × M)

The pairs of pairs that S does not Q-block.

Equations

• BidirectionalOT.qUnblockedSet pairs f S = {p : F × M | p ∈ pairs ∧ ¬BidirectionalOT.QBlocks f S p}

def BidirectionalOT.iUnblockedSet {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) (S : Set (F × M)) : Set (F × M)

The pairs of pairs that S does not I-block.

Equations

• BidirectionalOT.iUnblockedSet pairs f S = {p : F × M | p ∈ pairs ∧ ¬BidirectionalOT.IBlocks f S p}

theorem BidirectionalOT.qUnblockedSet_antitone {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) : Antitone (qUnblockedSet pairs f)

theorem BidirectionalOT.iUnblockedSet_antitone {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) : Antitone (iUnblockedSet pairs f)

theorem BidirectionalOT.unblockedSet_eq_inter {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) (S : Set (F × M)) : unblockedSet pairs f S = qUnblockedSet pairs f S ∩ iUnblockedSet pairs f S

def BidirectionalOT.IsWeakSolution {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) (Q I : Set (F × M)) : Prop

In the weak version of bidirection Q collects the pairs no pair of I Q-blocks and I the pairs no pair of Q I-blocks. A pair of both is super-optimal.

Equations

• BidirectionalOT.IsWeakSolution pairs f Q I = (BidirectionalOT.qUnblockedSet pairs f I = Q ∧ BidirectionalOT.iUnblockedSet pairs f Q = I)

theorem BidirectionalOT.exists_isWeakSolution {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) : ∃ (Q : Set (F × M)) (I : Set (F × M)), IsWeakSolution pairs f Q I

The mutual recursion has a solution, the greatest fixed point of the monotone composite qUnblockedSet ∘ iUnblockedSet together with its image under iUnblockedSet.

theorem BidirectionalOT.strongOptimalSet_subset_inter {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] (pairs : Set (F × M)) (f : F × M → α) {Q I : Set (F × M)} (h : IsWeakSolution pairs f Q I) : strongOptimalSet pairs f ⊆ Q ∩ I

Optimal pairs satisfy both principles of every weak solution, since a pair no pair of pairs blocks is blocked by no pair of I or of Q, both subsets of pairs.

Markedness and the division of labour

theorem BidirectionalOT.blocks_iff_of_strictMono {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [LinearOrder F] [LinearOrder M] {f : F × M → α} {S : Set (F × M)} {p : F × M} (hf : StrictMono f) : Blocks f S p ↔ Blocks id S p

A harmony strictly monotone in the markedness of forms and of meanings blocks as markedness itself does: of two pairs sharing a form or a meaning, the less marked one is more harmonic.

theorem BidirectionalOT.unblockedSet_eq_of_strictMono {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [LinearOrder F] [LinearOrder M] (pairs : Set (F × M)) {f : F × M → α} (hf : StrictMono f) : unblockedSet pairs f = unblockedSet pairs id

theorem BidirectionalOT.superoptimalSet_eq_of_strictMono {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [LinearOrder F] [LinearOrder M] (pairs : Set (F × M)) {f : F × M → α} (hf : StrictMono f) : superoptimalSet pairs f = superoptimalSet pairs id

Weak bidirection does not depend on how a strictly monotone harmony weighs the markedness of forms against that of meanings.

theorem BidirectionalOT.superoptimalSet_eq_graphOn {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [LinearOrder F] [LinearOrder M] (pairs : Set (F × M)) {f : F × M → α} (e : F ≃o M) (hf : StrictMono f) (h : pairs.IsWF) (he : Set.graphOn (⇑e) Set.univ ⊆ pairs) : superoptimalSet pairs f = Set.graphOn (⇑e) Set.univ

On a generator well-founded in markedness and containing the graph of an isomorphism e between the markedness orders of forms and of meanings, the super-optimal pairs are exactly that graph, under every harmony strictly monotone in markedness. This is the division of pragmatic labour.

Computable forms

def BidirectionalOT.unblocked {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) (S : Finset (F × M)) : Finset (F × M)

The pairs of pairs that S does not block.

Equations

• BidirectionalOT.unblocked pairs f S = {p ∈ pairs | ¬BidirectionalOT.Blocks f (↑S) p}

@[simp]

theorem BidirectionalOT.mem_unblocked {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] {pairs : Finset (F × M)} {f : F × M → α} {S : Finset (F × M)} {p : F × M} : p ∈ unblocked pairs f S ↔ p ∈ pairs ∧ ¬Blocks f (↑S) p

@[simp]

theorem BidirectionalOT.coe_unblocked {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) {S : Finset (F × M)} : ↑(unblocked pairs f S) = unblockedSet (↑pairs) f ↑S

theorem BidirectionalOT.unblocked_subset {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) {S : Finset (F × M)} : unblocked pairs f S ⊆ pairs

theorem BidirectionalOT.unblocked_antitone {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) : Antitone (unblocked pairs f)

def BidirectionalOT.strongOptimal {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) : Finset (F × M)

Strong bidirection, computably.

Equations

• BidirectionalOT.strongOptimal pairs f = BidirectionalOT.unblocked pairs f pairs

@[simp]

theorem BidirectionalOT.mem_strongOptimal {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] {pairs : Finset (F × M)} {f : F × M → α} {p : F × M} : p ∈ strongOptimal pairs f ↔ p ∈ pairs ∧ ¬Blocks f (↑pairs) p

theorem BidirectionalOT.coe_strongOptimal {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) : ↑(strongOptimal pairs f) = strongOptimalSet (↑pairs) f

def BidirectionalOT.superoptimalAux {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) (S : Finset (F × M)) : ℕ → Finset (F × M)

The squared blocking step iterated from S until it is fixed, at most n times; the computation behind superoptimal.

Equations

• One or more equations did not get rendered due to their size.
• BidirectionalOT.superoptimalAux pairs f S 0 = S

def BidirectionalOT.superoptimal {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) : Finset (F × M)

The super-optimal pairs, computably: the squared blocking step iterated from pairs until fixed, which happens within pairs.card steps. Equality with a literal Finset is closed by decide.

Equations

• BidirectionalOT.superoptimal pairs f = BidirectionalOT.superoptimalAux pairs f pairs pairs.card

theorem BidirectionalOT.coe_superoptimal {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) : ↑(superoptimal pairs f) = superoptimalSet (↑pairs) f

theorem BidirectionalOT.mem_superoptimal {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) {p : F × M} : p ∈ superoptimal pairs f ↔ p ∈ pairs ∧ ¬Blocks f (↑(superoptimal pairs f)) p

The footnote's recursion, computably.

theorem BidirectionalOT.superoptimal_subset {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) : superoptimal pairs f ⊆ pairs

theorem BidirectionalOT.strongOptimal_subset_superoptimal {F : Type u_1} {M : Type u_2} {α : Type u_3} [Preorder α] [DecidableEq F] [DecidableEq M] [DecidableLT α] (pairs : Finset (F × M)) (f : F × M → α) : strongOptimal pairs f ⊆ superoptimal pairs f