Correspondence Theory

A correspondence between two strings ([McCP95] (10)) is a relation ℛ between their positions, and a faithfulness constraint is a condition on ℛ: MAX reads its domain, DEP its range, IDENT the segments at corresponding positions. Correspondence Role α carries one string per role (form) and the relation edge r₁ r₂ for every ordered pair of roles, so the input–output, base–reduplicant and output–output ([Ben97]) relations of one candidate are cells of a single diagram. The relation is directed, as ℛ is; "correspondents of one another" is the derived property IsSymmetric.

The constraints of Appendix A are families Correspondence Role α → Role → Role → ℕ counting offending elements; a named constraint is a partial application (MAX-IO is (·.maxViol .input .output)), and each cardinal family vanishes iff the relation has the matching order-theoretic property (maxViol_eq_zero_iff, …). Positions are Fin-indexed, so every pair of edge is in range by type. The position-relation encoding follows [PVH17] and [PP02] (base–reduplicant relations: [DH20b]).

Main definitions

• Correspondence — role-indexed strings with a directed relation between the positions of each ordered pair of roles.
• Correspondence.maxViol, depViol, identViol, identViolFeature, contigIViol, contigOViol, anchorLViol, anchorRViol, linearityViol, uniformityViol, integrityViol — the constraint families of Appendix A; maxViolOn, depViolOn are their segment-class restrictions (MAX-V, DEP-C, …), and maxViolAt, depViolAt their restrictions to positions (positional faithfulness).
• Correspondence.ofPairs, diagram, parallel, identity, reduplication — constructors: from index pairs, the diagonal on a role predicate, and the binary and input–base–reduplicant diagonal diagrams.
• Correspondence.IsSymmetric, IsFaithful — symmetry of the relation; freedom from the five order-relevant violations on an edge.
• Correspondence.IsFaithfulness, IsMarkedness — the structural faithfulness/markedness split for constraints over correspondences.

Main results

• Correspondence.isFaithful_iff_exists_orderIso — an edge is faithful iff it is the graph of an order isomorphism between the two position orders.
• Correspondence.diagram_isSymmetric — a diagonal diagram over a symmetric role predicate is symmetric.
• Correspondence.isMarkedness_iff_exists_comap — a markedness constraint is exactly a constraint on strings pulled back along the output form.

References

• J. J. McCarthy and A. Prince, Faithfulness and Reduplicative Identity (1995)
• L. Benua, Transderivational Identity: Phonological Relations between Words (1997)
• A. Payne, M. H. Vu and J. Heinz, A Formal Analysis of Correspondence Theory (2017)
• C. Potts and G. K. Pullum, Model Theory and the Content of OT Constraints (2002)
• H. Dolatian and J. Heinz, Computing and Classifying Reduplication with 2-Way Finite-State Transducers (2020)

structure OptimalityTheory.Correspondence (Role : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

A correspondence diagram consists of a string for each role and, for each ordered pair of roles, a directed relation between their positions.

• form : Role → List α
• edge (r₁ r₂ : Role) : Finset (Fin (self.form r₁).length × Fin (self.form r₂).length)

inductive OptimalityTheory.BinaryRole : Type

The roles of a binary correspondence are its two strings, as in Correspondence.parallel and Correspondence.identity.

• lhs : BinaryRole
• rhs : BinaryRole

@[instance_reducible]

instance OptimalityTheory.instDecidableEqBinaryRole : DecidableEq BinaryRole

Equations

• OptimalityTheory.instDecidableEqBinaryRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def OptimalityTheory.instReprBinaryRole.repr : BinaryRole → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance OptimalityTheory.instReprBinaryRole : Repr BinaryRole

Equations

• OptimalityTheory.instReprBinaryRole = { reprPrec := OptimalityTheory.instReprBinaryRole.repr }

inductive OptimalityTheory.ReduplicationRole : Type

The roles of the basic model of reduplication are the input, the base and the reduplicant.

• input : ReduplicationRole
• base : ReduplicationRole
• reduplicant : ReduplicationRole

@[instance_reducible]

instance OptimalityTheory.instDecidableEqReduplicationRole : DecidableEq ReduplicationRole

Equations

• OptimalityTheory.instDecidableEqReduplicationRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def OptimalityTheory.instReprReduplicationRole.repr : ReduplicationRole → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance OptimalityTheory.instReprReduplicationRole : Repr ReduplicationRole

Equations

• OptimalityTheory.instReprReduplicationRole = { reprPrec := OptimalityTheory.instReprReduplicationRole.repr }

def OptimalityTheory.Correspondence.IsSymmetric {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) : Prop

Correspondence is symmetric when each relation is the converse of the reverse one.

Equations

• c.IsSymmetric = ∀ (r₁ r₂ : Role), c.edge r₂ r₁ = Finset.image Prod.swap (c.edge r₁ r₂)

Constraint families

def OptimalityTheory.Correspondence.maxViol {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

MAX (A.1) counts the positions of form r₁ without a correspondent in form r₂.

Equations

• c.maxViol r₁ r₂ = (Finset.univ \ Finset.image Prod.fst (c.edge r₁ r₂)).card

def OptimalityTheory.Correspondence.depViol {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

DEP (A.2) counts the positions of form r₂ without a correspondent in form r₁.

Equations

• c.depViol r₁ r₂ = (Finset.univ \ Finset.image Prod.snd (c.edge r₁ r₂)).card

def OptimalityTheory.Correspondence.maxViolOn {Role : Type u_1} {α : Type u_2} (P : α → Prop) [DecidablePred P] (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

MAX (A.1) restricted to the positions of form r₁ whose segment satisfies P — the segment-class instances MAX-V, MAX-C.

Equations

• OptimalityTheory.Correspondence.maxViolOn P c r₁ r₂ = ({i : Fin (c.form r₁).length | P (c.form r₁)[i]} \ Finset.image Prod.fst (c.edge r₁ r₂)).card

def OptimalityTheory.Correspondence.depViolOn {Role : Type u_1} {α : Type u_2} (P : α → Prop) [DecidablePred P] (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

DEP (A.2) restricted to the positions of form r₂ whose segment satisfies P — the segment-class instances DEP-V, DEP-C.

Equations

• OptimalityTheory.Correspondence.depViolOn P c r₁ r₂ = ({j : Fin (c.form r₂).length | P (c.form r₂)[j]} \ Finset.image Prod.snd (c.edge r₁ r₂)).card

def OptimalityTheory.Correspondence.maxViolAt {Role : Type u_1} {α : Type u_2} (P : ℕ → Prop) [DecidablePred P] (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

MAX restricted to the positions of form r₁ that satisfy P, the positional faithfulness constraints that protect a segment by where it stands, not by what it is.

Equations

• OptimalityTheory.Correspondence.maxViolAt P c r₁ r₂ = ({i : Fin (c.form r₁).length | P ↑i} \ Finset.image Prod.fst (c.edge r₁ r₂)).card

def OptimalityTheory.Correspondence.depViolAt {Role : Type u_1} {α : Type u_2} (P : ℕ → Prop) [DecidablePred P] (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

DEP restricted to the positions of form r₂ that satisfy P.

Equations

• OptimalityTheory.Correspondence.depViolAt P c r₁ r₂ = ({j : Fin (c.form r₂).length | P ↑j} \ Finset.image Prod.snd (c.edge r₁ r₂)).card

def OptimalityTheory.Correspondence.identViol {Role : Type u_1} {α : Type u_2} [DecidableEq α] (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

IDENT (A.3) on whole segments counts the corresponding pairs whose segments differ.

Equations

• c.identViol r₁ r₂ = {p ∈ c.edge r₁ r₂ | (c.form r₁)[p.1] ≠ (c.form r₂)[p.2]}.card

def OptimalityTheory.Correspondence.identViolFeature {Role : Type u_1} {α : Type u_2} {F : Type u_3} [DecidableEq F] (proj : α → F) (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

IDENT(F) (A.3) for the feature proj counts the corresponding pairs that differ under proj.

Equations

• OptimalityTheory.Correspondence.identViolFeature proj c r₁ r₂ = {p ∈ c.edge r₁ r₂ | proj (c.form r₁)[p.1] ≠ proj (c.form r₂)[p.2]}.card

def OptimalityTheory.Correspondence.maxViolFeature {Role : Type u_1} {α : Type u_2} (P : α → Prop) [DecidablePred P] (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

MAX of a privative property along a segmental correspondence counts the corresponding pairs whose first member has P and whose second lacks it, the autosegment being lost.

Equations

• OptimalityTheory.Correspondence.maxViolFeature P c r₁ r₂ = {p ∈ c.edge r₁ r₂ | P (c.form r₁)[p.1] ∧ ¬P (c.form r₂)[p.2]}.card

def OptimalityTheory.Correspondence.depViolFeature {Role : Type u_1} {α : Type u_2} (P : α → Prop) [DecidablePred P] (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

DEP of a privative property along a segmental correspondence counts the corresponding pairs whose second member has P and whose first lacks it, the autosegment being inserted.

Equations

• OptimalityTheory.Correspondence.depViolFeature P c r₁ r₂ = {p ∈ c.edge r₁ r₂ | ¬P (c.form r₁)[p.1] ∧ P (c.form r₂)[p.2]}.card

theorem OptimalityTheory.Correspondence.maxViolFeature_pos_iff {Role : Type u_1} {α : Type u_2} (P : α → Prop) [DecidablePred P] (c : Correspondence Role α) (r₁ r₂ : Role) : 0 < maxViolFeature P c r₁ r₂ ↔ ∃ p ∈ c.edge r₁ r₂, P (c.form r₁)[p.1] ∧ ¬P (c.form r₂)[p.2]

maxViolFeature is positive exactly when some correspondent loses P.

def OptimalityTheory.Correspondence.contigIViol {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

I-CONTIG, "No Skipping" (A.4a): whether the domain of the relation is a contiguous substring of form r₁.

Equations

• c.contigIViol r₁ r₂ = if List.IsChain (fun (a b : ℕ) => b = a + 1) ((Finset.image Fin.val (Finset.image Prod.fst (c.edge r₁ r₂))).sort fun (x1 x2 : ℕ) => x1 ≤ x2) then 0 else 1

def OptimalityTheory.Correspondence.contigOViol {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

O-CONTIG, "No Intrusion" (A.4b): whether the range of the relation is a contiguous substring of form r₂.

Equations

• c.contigOViol r₁ r₂ = if List.IsChain (fun (a b : ℕ) => b = a + 1) ((Finset.image Fin.val (Finset.image Prod.snd (c.edge r₁ r₂))).sort fun (x1 x2 : ℕ) => x1 ≤ x2) then 0 else 1

def OptimalityTheory.Correspondence.anchorLViol {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

L-ANCHOR (A.5): whether the leftmost positions correspond; vacuous when either string is empty.

Equations

• c.anchorLViol r₁ r₂ = if h : 0 < (c.form r₁).length ∧ 0 < (c.form r₂).length then if (⟨0, ⋯⟩, ⟨0, ⋯⟩) ∈ c.edge r₁ r₂ then 0 else 1 else 0

def OptimalityTheory.Correspondence.anchorRViol {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

R-ANCHOR (A.5): whether the rightmost positions correspond; vacuous when either string is empty.

Equations

• c.anchorRViol r₁ r₂ = if h : 0 < (c.form r₁).length ∧ 0 < (c.form r₂).length then if (⟨(c.form r₁).length - 1, ⋯⟩, ⟨(c.form r₂).length - 1, ⋯⟩) ∈ c.edge r₁ r₂ then 0 else 1 else 0

def OptimalityTheory.Correspondence.linearityViol {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

LINEARITY, "No Metathesis" (A.6), counts the pairs of correspondences (i₁, j₁), (i₂, j₂) with i₁ < i₂ but j₂ < j₁.

Equations

• c.linearityViol r₁ r₂ = {pq ∈ c.edge r₁ r₂ ×ˢ c.edge r₁ r₂ | pq.1.1 < pq.2.1 ∧ pq.2.2 < pq.1.2}.card

def OptimalityTheory.Correspondence.uniformityViol {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

UNIFORMITY, "No Coalescence" (A.7), counts the positions of form r₂ with more than one correspondent in form r₁.

Equations

• c.uniformityViol r₁ r₂ = {j : Fin (c.form r₂).length | 1 < {p ∈ c.edge r₁ r₂ | p.2 = j}.card}.card

def OptimalityTheory.Correspondence.integrityViol {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : ℕ

INTEGRITY, "No Breaking" (A.8), counts the positions of form r₁ with more than one correspondent in form r₂.

Equations

• c.integrityViol r₁ r₂ = {i : Fin (c.form r₁).length | 1 < {p ∈ c.edge r₁ r₂ | p.1 = i}.card}.card

Vanishing characterizations

Each cardinal constraint vanishes iff the relation has the corresponding order-theoretic property: left-total, right-total, functional, injective, order-preserving.

theorem OptimalityTheory.Correspondence.maxViol_eq_zero_iff {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : c.maxViol r₁ r₂ = 0 ↔ Finset.univ ⊆ Finset.image Prod.fst (c.edge r₁ r₂)

theorem OptimalityTheory.Correspondence.depViol_eq_zero_iff {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : c.depViol r₁ r₂ = 0 ↔ Finset.univ ⊆ Finset.image Prod.snd (c.edge r₁ r₂)

theorem OptimalityTheory.Correspondence.maxViolOn_true {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : maxViolOn (fun (x : α) => True) c r₁ r₂ = c.maxViol r₁ r₂

theorem OptimalityTheory.Correspondence.depViolOn_true {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : depViolOn (fun (x : α) => True) c r₁ r₂ = c.depViol r₁ r₂

theorem OptimalityTheory.Correspondence.maxViolAt_true {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : maxViolAt (fun (x : ℕ) => True) c r₁ r₂ = c.maxViol r₁ r₂

theorem OptimalityTheory.Correspondence.depViolAt_true {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : depViolAt (fun (x : ℕ) => True) c r₁ r₂ = c.depViol r₁ r₂

theorem OptimalityTheory.Correspondence.integrityViol_eq_zero_iff {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : c.integrityViol r₁ r₂ = 0 ↔ ∀ (i : Fin (c.form r₁).length), {p ∈ c.edge r₁ r₂ | p.1 = i}.card ≤ 1

theorem OptimalityTheory.Correspondence.uniformityViol_eq_zero_iff {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : c.uniformityViol r₁ r₂ = 0 ↔ ∀ (j : Fin (c.form r₂).length), {p ∈ c.edge r₁ r₂ | p.2 = j}.card ≤ 1

theorem OptimalityTheory.Correspondence.linearityViol_eq_zero_iff {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : c.linearityViol r₁ r₂ = 0 ↔ ∀ p ∈ c.edge r₁ r₂, ∀ q ∈ c.edge r₁ r₂, p.1 < q.1 → ¬q.2 < p.2

Constructors

def OptimalityTheory.Correspondence.diagonalPairs (k : ℕ) : List (ℕ × ℕ)

The index pairs (0, 0), …, (k - 1, k - 1) of a parallel correspondence.

Equations

• OptimalityTheory.Correspondence.diagonalPairs k = List.map (fun (i : ℕ) => (i, i)) (List.range k)

def OptimalityTheory.Correspondence.edgeOfPairs (m n : ℕ) (l : List (ℕ × ℕ)) : Finset (Fin m × Fin n)

The relation on positions given by index pairs; pairs out of range are dropped.

Equations

• OptimalityTheory.Correspondence.edgeOfPairs m n l = (List.filterMap (fun (p : ℕ × ℕ) => if h : p.1 < m ∧ p.2 < n then some (⟨p.1, ⋯⟩, ⟨p.2, ⋯⟩) else none) l).toFinset

@[simp]

theorem OptimalityTheory.Correspondence.mem_edgeOfPairs {m n : ℕ} {l : List (ℕ × ℕ)} {p : Fin m × Fin n} : p ∈ edgeOfPairs m n l ↔ (↑p.1, ↑p.2) ∈ l

def OptimalityTheory.Correspondence.ofPairs {Role : Type u_1} {α : Type u_2} (form : Role → List α) (pairs : Role → Role → List (ℕ × ℕ)) : Correspondence Role α

ofPairs form pairs is the correspondence whose relation edge r₁ r₂ reads the index pairs pairs r₁ r₂ into the two position types.

Equations

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

@[simp]

theorem OptimalityTheory.Correspondence.ofPairs_form {Role : Type u_1} {α : Type u_2} (form : Role → List α) (pairs : Role → Role → List (ℕ × ℕ)) (r : Role) : (ofPairs form pairs).form r = form r

@[simp]

theorem OptimalityTheory.Correspondence.ofPairs_edge {Role : Type u_1} {α : Type u_2} (r₁ r₂ : Role) (form : Role → List α) (pairs : Role → Role → List (ℕ × ℕ)) : (ofPairs form pairs).edge r₁ r₂ = edgeOfPairs ((ofPairs form pairs).form r₁).length ((ofPairs form pairs).form r₂).length (pairs r₁ r₂)

def OptimalityTheory.Correspondence.diagonal (m n : ℕ) : Finset (Fin m × Fin n)

The diagonal (0, 0), (1, 1), … of Fin m × Fin n, one pair per index of the shorter string.

Equations

• OptimalityTheory.Correspondence.diagonal m n = Finset.image (fun (i : Fin (min m n)) => (Fin.castLE ⋯ i, Fin.castLE ⋯ i)) Finset.univ

@[simp]

theorem OptimalityTheory.Correspondence.mem_diagonal {m n : ℕ} (a : Fin m) (b : Fin n) : (a, b) ∈ diagonal m n ↔ ↑a = ↑b

theorem OptimalityTheory.Correspondence.card_diagonal (m n : ℕ) : (diagonal m n).card = min m n

theorem OptimalityTheory.Correspondence.image_swap_diagonal (m n : ℕ) : Finset.image Prod.swap (diagonal m n) = diagonal n m

def OptimalityTheory.Correspondence.diagram {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] : Correspondence Role α

The diagonal correspondence on every pair of roles satisfying hasEdge, empty elsewhere.

Equations

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

@[simp]

theorem OptimalityTheory.Correspondence.diagram_form {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] (r : Role) : (diagram form hasEdge).form r = form r

theorem OptimalityTheory.Correspondence.diagram_edge {Role : Type u_1} {α : Type u_2} (r₁ r₂ : Role) (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] : (diagram form hasEdge).edge r₁ r₂ = if hasEdge r₁ r₂ then diagonal (form r₁).length (form r₂).length else ∅

theorem OptimalityTheory.Correspondence.diagram_edge_pos {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] {r₁ r₂ : Role} (h : hasEdge r₁ r₂) : (diagram form hasEdge).edge r₁ r₂ = diagonal (form r₁).length (form r₂).length

theorem OptimalityTheory.Correspondence.diagram_edge_neg {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] {r₁ r₂ : Role} (h : ¬hasEdge r₁ r₂) : (diagram form hasEdge).edge r₁ r₂ = ∅

theorem OptimalityTheory.Correspondence.diagram_isSymmetric {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] (hsymm : ∀ {r₁ r₂ : Role}, hasEdge r₁ r₂ → hasEdge r₂ r₁) : (diagram form hasEdge).IsSymmetric

def OptimalityTheory.Correspondence.parallel {α : Type u_2} (s₁ s₂ : List α) : Correspondence BinaryRole α

The diagonal correspondence between two strings, truncated to the shorter.

Equations

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

def OptimalityTheory.Correspondence.identity {α : Type u_2} (s : List α) : Correspondence BinaryRole α

identity s is the fully faithful candidate, the diagonal correspondence of a string with itself.

Equations

• OptimalityTheory.Correspondence.identity s = OptimalityTheory.Correspondence.parallel s s

def OptimalityTheory.Correspondence.reduplication {α : Type u_2} (input base reduplicant : List α) : Correspondence ReduplicationRole α

The input–base–reduplicant diagram with diagonal correspondence between each pair of distinct roles.

Equations

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

theorem OptimalityTheory.Correspondence.parallel_isSymmetric {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).IsSymmetric

theorem OptimalityTheory.Correspondence.reduplication_isSymmetric {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).IsSymmetric

@[simp]

theorem OptimalityTheory.Correspondence.parallel_form_lhs {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).form BinaryRole.lhs = s₁

@[simp]

theorem OptimalityTheory.Correspondence.parallel_form_rhs {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).form BinaryRole.rhs = s₂

@[simp]

theorem OptimalityTheory.Correspondence.parallel_edge_diag {α : Type u_2} (s₁ s₂ : List α) (r : BinaryRole) : (parallel s₁ s₂).edge r r = ∅

@[simp]

theorem OptimalityTheory.Correspondence.parallel_edge_lhs_rhs {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).edge BinaryRole.lhs BinaryRole.rhs = diagonal s₁.length s₂.length

@[simp]

theorem OptimalityTheory.Correspondence.parallel_edge_rhs_lhs {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).edge BinaryRole.rhs BinaryRole.lhs = diagonal s₂.length s₁.length

@[simp]

theorem OptimalityTheory.Correspondence.reduplication_form_input {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).form ReduplicationRole.input = input

@[simp]

theorem OptimalityTheory.Correspondence.reduplication_form_base {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).form ReduplicationRole.base = base

@[simp]

theorem OptimalityTheory.Correspondence.reduplication_form_reduplicant {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).form ReduplicationRole.reduplicant = reduplicant

theorem OptimalityTheory.Correspondence.reduplication_edge {α : Type u_2} (input base reduplicant : List α) {r₁ r₂ : ReduplicationRole} (h : r₁ ≠ r₂) : (reduplication input base reduplicant).edge r₁ r₂ = diagonal ((reduplication input base reduplicant).form r₁).length ((reduplication input base reduplicant).form r₂).length

Faithfulness on the diagonal

MAX, DEP and IDENT vanish on a diagonal edge between equal strings — the fully faithful candidate, and total reduplication read on its base–reduplicant edge.

theorem OptimalityTheory.Correspondence.card_image_fst_diagonal (m n : ℕ) : (Finset.image Prod.fst (diagonal m n)).card = min m n

theorem OptimalityTheory.Correspondence.card_image_snd_diagonal (m n : ℕ) : (Finset.image Prod.snd (diagonal m n)).card = min m n

theorem OptimalityTheory.Correspondence.maxViol_of_diagonal {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) (hedge : c.edge r₁ r₂ = diagonal (c.form r₁).length (c.form r₂).length) : c.maxViol r₁ r₂ = (c.form r₁).length - (c.form r₂).length

On a diagonal edge MAX counts the truncated tail of the first string.

theorem OptimalityTheory.Correspondence.depViol_of_diagonal {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) (hedge : c.edge r₁ r₂ = diagonal (c.form r₁).length (c.form r₂).length) : c.depViol r₁ r₂ = (c.form r₂).length - (c.form r₁).length

On a diagonal edge DEP counts the tail of the second string beyond the first.

theorem OptimalityTheory.Correspondence.maxViol_eq_zero_of_diagonal {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) (hform : c.form r₁ = c.form r₂) (hedge : c.edge r₁ r₂ = diagonal (c.form r₁).length (c.form r₂).length) : c.maxViol r₁ r₂ = 0

theorem OptimalityTheory.Correspondence.depViol_eq_zero_of_diagonal {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) (hform : c.form r₁ = c.form r₂) (hedge : c.edge r₁ r₂ = diagonal (c.form r₁).length (c.form r₂).length) : c.depViol r₁ r₂ = 0

theorem OptimalityTheory.Correspondence.identViolFeature_eq_zero_of_diagonal {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) {F : Type u_3} [DecidableEq F] (proj : α → F) (hform : c.form r₁ = c.form r₂) (hedge : c.edge r₁ r₂ = diagonal (c.form r₁).length (c.form r₂).length) : identViolFeature proj c r₁ r₂ = 0

theorem OptimalityTheory.Correspondence.identViol_eq_zero_of_diagonal {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) [DecidableEq α] (hform : c.form r₁ = c.form r₂) (hedge : c.edge r₁ r₂ = diagonal (c.form r₁).length (c.form r₂).length) : c.identViol r₁ r₂ = 0

@[simp]

theorem OptimalityTheory.Correspondence.maxViol_identity {α : Type u_2} (s : List α) : (identity s).maxViol BinaryRole.lhs BinaryRole.rhs = 0

@[simp]

theorem OptimalityTheory.Correspondence.depViol_identity {α : Type u_2} (s : List α) : (identity s).depViol BinaryRole.lhs BinaryRole.rhs = 0

@[simp]

theorem OptimalityTheory.Correspondence.identViol_identity {α : Type u_2} [DecidableEq α] (s : List α) : (identity s).identViol BinaryRole.lhs BinaryRole.rhs = 0

@[simp]

theorem OptimalityTheory.Correspondence.identViolFeature_identity {α : Type u_2} {F : Type u_3} [DecidableEq F] (proj : α → F) (s : List α) : identViolFeature proj (identity s) BinaryRole.lhs BinaryRole.rhs = 0

Faithfulness as order isomorphism

structure OptimalityTheory.Correspondence.IsFaithful {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : Prop

An edge is faithful when it has no MAX, DEP, INTEGRITY, UNIFORMITY or LINEARITY violation — exactly the hypotheses under which it is the graph of an order isomorphism.

• max : c.maxViol r₁ r₂ = 0
• dep : c.depViol r₁ r₂ = 0
• integrity : c.integrityViol r₁ r₂ = 0
• uniformity : c.uniformityViol r₁ r₂ = 0
• linearity : c.linearityViol r₁ r₂ = 0

theorem OptimalityTheory.Correspondence.exists_fun_mem_edge_iff {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) (hmax : c.maxViol r₁ r₂ = 0) (hint : c.integrityViol r₁ r₂ = 0) : ∃ (f : Fin (c.form r₁).length → Fin (c.form r₂).length), ∀ (i : Fin (c.form r₁).length) (j : Fin (c.form r₂).length), (i, j) ∈ c.edge r₁ r₂ ↔ f i = j

Without MAX or INTEGRITY violations the edge is the graph of a function.

theorem OptimalityTheory.Correspondence.isFaithful_iff_exists_orderIso {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) : c.IsFaithful r₁ r₂ ↔ ∃ (e : Fin (c.form r₁).length ≃o Fin (c.form r₂).length), ∀ (i : Fin (c.form r₁).length) (j : Fin (c.form r₂).length), (i, j) ∈ c.edge r₁ r₂ ↔ e i = j

theorem OptimalityTheory.Correspondence.length_eq_of_isFaithful {Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) (h : c.IsFaithful r₁ r₂) : (c.form r₁).length = (c.form r₂).length

A faithful edge joins strings of equal length.

Faithfulness and markedness constraints

A constraint over correspondences is faithfulness when the fully faithful candidate satisfies it, and markedness when it reads only the output string. The split is structural, and non-vacuous: *STRUC is markedness and fires on identity s.

def OptimalityTheory.Correspondence.IsFaithfulness {α : Type u_2} (k : Constraint (Correspondence BinaryRole α)) : Prop

A constraint over binary correspondences is faithfulness when the fully faithful candidate identity s satisfies it.

Equations

• OptimalityTheory.Correspondence.IsFaithfulness k = ∀ (s : List α), k (OptimalityTheory.Correspondence.identity s) = 0

def OptimalityTheory.Correspondence.IsMarkedness {Role : Type u_1} {α : Type u_2} (out : Role) (k : Constraint (Correspondence Role α)) : Prop

A constraint is markedness for the role out when it depends only on form out.

Equations

• OptimalityTheory.Correspondence.IsMarkedness out k = Function.FactorsThrough k fun (x : OptimalityTheory.Correspondence Role α) => x.form out

theorem OptimalityTheory.Correspondence.isMarkedness_comap {Role : Type u_1} {α : Type u_2} (out : Role) (m : Constraint (List α)) : IsMarkedness out (Constraint.comap (fun (x : Correspondence Role α) => x.form out) m)

A constraint on strings pulled back along the output form is markedness.

theorem OptimalityTheory.Correspondence.isMarkedness_iff_exists_comap {Role : Type u_1} {α : Type u_2} (out : Role) (k : Constraint (Correspondence Role α)) : IsMarkedness out k ↔ ∃ (m : Constraint (List α)), k = Constraint.comap (fun (x : Correspondence Role α) => x.form out) m

A constraint is markedness for the role out exactly when it is a constraint on strings pulled back along form out.

theorem OptimalityTheory.Correspondence.isFaithfulness_maxViol {α : Type u_2} : IsFaithfulness fun (x : Correspondence BinaryRole α) => x.maxViol BinaryRole.lhs BinaryRole.rhs

theorem OptimalityTheory.Correspondence.isFaithfulness_depViol {α : Type u_2} : IsFaithfulness fun (x : Correspondence BinaryRole α) => x.depViol BinaryRole.lhs BinaryRole.rhs

theorem OptimalityTheory.Correspondence.isFaithfulness_identViol {α : Type u_2} [DecidableEq α] : IsFaithfulness fun (x : Correspondence BinaryRole α) => x.identViol BinaryRole.lhs BinaryRole.rhs

theorem OptimalityTheory.Correspondence.exists_isMarkedness_not_isFaithfulness {α : Type u_2} [Inhabited α] : ∃ (k : Constraint (Correspondence BinaryRole α)), IsMarkedness BinaryRole.rhs k ∧ ¬IsFaithfulness k