Docs / Phonology / OptimalityTheory / Correspondence / Basic

Correspondence theory

import Linglib.Phonology.OptimalityTheory.Correspondence.Basic · namespace OptimalityTheory

This file defines McCarthy and Prince's correspondence between strings, a relation between their positions, and the faithfulness constraints as conditions on it: MAX reads its domain, DEP its range, and IDENT the segments at corresponding positions. A correspondence carries one string per role and a relation between the positions of each ordered pair of roles, so that the input, base, and reduplicant of a reduplicative candidate form one diagram.

Main definitions

Correspondence Role α: a string for each role and 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 families MAX, DEP, IDENT, IDENT(F), I-CONTIG, O-CONTIG, L-ANCHOR, R-ANCHOR, LINEARITY, UNIFORMITY, and INTEGRITY, counting offending elements; maxViolOn and depViolOn restrict MAX and DEP to a class of segments, and maxViolAt and depViolAt to a class of positions.
Correspondence.ofPairs, diagram, parallel, identity, reduplication: constructors from index pairs, from a role predicate with the diagonal on each selected pair of roles, and the binary and input–base–reduplicant diagonal diagrams.
Correspondence.IsSymmetric, IsFaithful: symmetry of the relation, and freedom from the five order-relevant violations on an edge.
Correspondence.IsFaithfulness, IsMarkedness: a constraint that the fully faithful candidate satisfies, and one that depends only on the output string.

Main statements

Correspondence.maxViol_eq_zero_iff and its siblings: MAX, DEP, INTEGRITY, UNIFORMITY, and LINEARITY vanish iff the relation is left-total, right-total, functional, injective, and order-preserving.
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 constraint is markedness iff it is a constraint on strings pulled back along the output form.
Correspondence.identViolFeature_of_diagonal: on a diagonal edge a feature family counts the offending pairs of the two strings' List.zip, as do maxViolFeature_of_diagonal and depViolFeature_of_diagonal.
Correspondence.IsFaithfulness.not_antifaithful: the anti-faithfulness constraint of a faithfulness constraint is not faithfulness.

Implementation notes

A named constraint is a partial application of a family to a pair of roles: MAX-IO is (·.maxViol .input .output).
Positions are indexed by Fin, so that every pair in an edge is in range by type, and Correspondence.ofPairs drops index pairs out of range.
Encoding a correspondence as a binary relation on positions follows Payne, Vu, and Heinz.

References

Declarations

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

structure Correspondence L81–85

(Role : Type u_1) (α : Type u_2) :

Type (max u_1 u_2)

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

Used in Phonology/OptimalityTheory/Correspondence/Deletion, Alderete2001, Benua1997, BerentEtAl2016, Casali1997 and 7 more

A correspondence is symmetric when each relation is the converse of the reverse one.

def Correspondence.IsSymmetric L115–117

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) :

Prop

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

Built from

Used by Correspondence.diagram_isSymmetric, Correspondence.parallel_isSymmetric, Correspondence.reduplication_isSymmetric, Correspondence.ofFun_isSymmetric, Correspondence.IsSymmetric.swap, Correspondence.IsSymmetric.maxViolAt_eq, Correspondence.IsSymmetric.maxViol_eq, Correspondence.IsSymmetric.identViol_eq

Used in Phonology/OptimalityTheory/Correspondence/Deletion

Constraint families

MAX counts the positions of form r₁ without a correspondent in form r₂.

def Correspondence.maxViol L121–123

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) :

ℕ

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

Built from

Used by Correspondence.maxViol_eq_zero_iff, Correspondence.maxViolOn_true, Correspondence.maxViolAt_true, Correspondence.maxViol_swap, Correspondence.maxViol_of_diagonal, Correspondence.maxViol_eq_zero_of_diagonal, Correspondence.maxViol_identity, Correspondence.IsSymmetric.maxViol_eq, Correspondence.maxViol_eq_zero_of_graph, Correspondence.IsFaithful, Correspondence.exists_fun_mem_edge_iff, Correspondence.exists_orderEmbedding_mem_edge_iff, Correspondence.isFaithfulness_maxViol

Used in Phonology/OptimalityTheory/Correspondence/Deletion, Alderete2001, Casali1997, Pater2001, Storme2026

DEP counts the positions of form r₂ without a correspondent in form r₁.

def Correspondence.depViol L125–127

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) :

ℕ

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

Built from

Used by Correspondence.depViol_eq_zero_iff, Correspondence.depViolOn_true, Correspondence.depViolAt_true, Correspondence.depViol_of_diagonal, Correspondence.depViol_eq_zero_of_diagonal, Correspondence.depViol_identity, Correspondence.IsSymmetric.maxViol_eq, Correspondence.IsFaithful, Correspondence.isFaithfulness_depViol

Used in Phonology/OptimalityTheory/Correspondence/Deletion, Storme2026

MAX restricted to the positions of form r₁ whose segment satisfies P, as in MAX-V and MAX-C.

def Correspondence.maxViolOn L129–134

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

ℕ

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

Built from

Used by Correspondence.maxViolOn_true

Used in McCarthy2005

DEP restricted to the positions of form r₂ whose segment satisfies P, as in DEP-V and DEP-C.

def Correspondence.depViolOn L136–141

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

ℕ

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

Built from

Used by Correspondence.depViolOn_true

Used in McCarthy2005

MAX restricted to the positions of form r₁ that satisfy P, which is the form of a positional faithfulness constraint.

def Correspondence.maxViolAt L143–147

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

ℕ

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

Built from

Used by Correspondence.maxViolAt_true, Correspondence.IsSymmetric.maxViolAt_eq

Used in Phonology/OptimalityTheory/Correspondence/Deletion, Phonology/OptimalityTheory/PositionalFaithfulness, Casali1997, Vago2017

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

def Correspondence.depViolAt L149–152

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

ℕ

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

Built from

Used by Correspondence.depViolAt_true, Correspondence.depViolAt_swap, Correspondence.IsSymmetric.maxViolAt_eq, Correspondence.depViolAt_of_graph

Used in Phonology/OptimalityTheory/Correspondence/Deletion

IDENT on whole segments counts the corresponding pairs whose segments differ.

def Correspondence.identViol L154–156

{Role : Type u_1} {α : Type u_2} [DecidableEq α] (c : Correspondence Role α) (r₁ r₂ : Role) :

ℕ

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

Built from

Used by Correspondence.identViol_swap, Correspondence.identViol_eq_zero_of_diagonal, Correspondence.identViol_identity, Correspondence.IsSymmetric.identViol_eq, Correspondence.identViol_eq_zero_iff_of_graph, Correspondence.isFaithfulness_identViol

Used in Phonology/OptimalityTheory/Correspondence/Deletion

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

def Correspondence.identViolFeature L158–161

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

ℕ

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

Built from

Used by Correspondence.identViolFeature_eq_zero_of_diagonal, Correspondence.identViolFeature_identity, Correspondence.identViolFeature_of_diagonal

Used in Alderete2001, Benua1997, McCarthy2005

L163–167

L169–173

L175–179

I-CONTIG is violated once unless the domain of the relation is a contiguous substring of form r₁.

def Correspondence.contigIViol L181–185

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) :

ℕ

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

Built from

O-CONTIG is violated once unless the range of the relation is a contiguous substring of form r₂.

def Correspondence.contigOViol L187–191

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) :

ℕ

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

Built from

L-ANCHOR is violated once unless the leftmost positions correspond; it is vacuous when either string is empty.

def Correspondence.anchorLViol L193–198

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) :

ℕ

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

Built from

R-ANCHOR is violated once unless the rightmost positions correspond; it is vacuous when either string is empty.

def Correspondence.anchorRViol L200–206

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) :

ℕ

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

Built from

LINEARITY counts the pairs of correspondences (i₁, j₁) and (i₂, j₂) with i₁ < i₂ but j₂ < j₁.

def Correspondence.linearityViol L208–211

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) :

ℕ

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

Built from

Used by Correspondence.linearityViol_eq_zero_iff, Correspondence.linearityViol_eq_zero_of_graph, Correspondence.IsFaithful, Correspondence.exists_orderEmbedding_mem_edge_iff

UNIFORMITY counts the positions of form r₂ with more than one correspondent in form r₁.

def Correspondence.uniformityViol L213–217

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) :

ℕ

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

Built from

Used by Correspondence.uniformityViol_eq_zero_iff, Correspondence.uniformityViol_eq_zero_of_graph, Correspondence.IsFaithful, Correspondence.exists_orderEmbedding_mem_edge_iff

Used in Pater2001

INTEGRITY counts the positions of form r₁ with more than one correspondent in form r₂.

def Correspondence.integrityViol L219–223

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) :

ℕ

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

Built from

Used by Correspondence.integrityViol_eq_zero_iff, Correspondence.integrityViol_eq_zero_of_graph, Correspondence.IsFaithful, Correspondence.exists_fun_mem_edge_iff, Correspondence.exists_orderEmbedding_mem_edge_iff

Vanishing characterizations

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

theorem Correspondence.maxViol_eq_zero_iff L232–234

{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₂)

Built from ,

Constructors

L270–271

L273–276

L278–281

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

def Correspondence.ofPairs L283–288

{Role : Type u_1} {α : Type u_2} (form : Role → List α) (pairs : Role → Role → List (ℕ × ℕ)) :

Correspondence Role α

The definition is too large to print here; read it in the source.

Built from

Used by Correspondence.ofPairs_form, Correspondence.ofPairs_edge

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

def Correspondence.diagram L318–323

{Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] :

Correspondence Role α

The definition is too large to print here; read it in the source.

Built from

Used by Correspondence.diagram_form, Correspondence.diagram_edge, Correspondence.diagram_edge_pos, Correspondence.diagram_edge_neg, Correspondence.diagram_isSymmetric

theorem Correspondence.diagram_isSymmetric L342–348

{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

Built from ,

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

def Correspondence.parallel L352–354

{α : Type u_2} (s₁ s₂ : List α) :

Correspondence BinaryRole α

The definition is too large to print here; read it in the source.

Built from ,

Used by Correspondence.identity, Correspondence.parallel_isSymmetric, Correspondence.parallel_form_lhs, Correspondence.parallel_form_rhs, Correspondence.parallel_edge_diag, Correspondence.parallel_edge_lhs_rhs, Correspondence.parallel_edge_rhs_lhs

Used in Benua1997, Pater2001, Stojkovic2026

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

def Correspondence.identity L356–358

{α : Type u_2} (s : List α) :

Correspondence BinaryRole α

Correspondence.identity s = Correspondence.parallel s s

Built from , ,

Used by Correspondence.maxViol_identity, Correspondence.depViol_identity, Correspondence.identViol_identity, Correspondence.identViolFeature_identity, Correspondence.IsFaithfulness

Used in Pater2001, Storme2026

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

def Correspondence.reduplication L360–363

{α : Type u_2} (input base reduplicant : List α) :

Correspondence ReduplicationRole α

The definition is too large to print here; read it in the source.

Built from ,

Used by Correspondence.reduplication_isSymmetric, Correspondence.reduplication_form_input, Correspondence.reduplication_form_base, Correspondence.reduplication_form_reduplicant, Correspondence.reduplication_edge

Used in BerentEtAl2016, McCarthyPrince1995

Faithfulness on the diagonal

MAX, DEP, and IDENT vanish on a diagonal edge between equal strings, as on the fully faithful candidate identity s.

Diagonal edges as zips

On a diagonal edge the i-th positions of the two strings correspond, so a feature family counts the offending pairs of their List.zip.

L530–548

theorem Correspondence.maxViolFeature_of_diagonal L550–554

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) (P : α → Prop) [DecidablePred P] (hedge : c.edge r₁ r₂ = diagonal (c.form r₁).length (c.form r₂).length) :

maxViolFeature P c r₁ r₂ = List.countP (fun (p : α × α) => decide (P p.1 ∧ ¬P p.2)) ((c.form r₁).zip (c.form r₂))

Built from , ,

theorem Correspondence.depViolFeature_of_diagonal L556–560

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) (P : α → Prop) [DecidablePred P] (hedge : c.edge r₁ r₂ = diagonal (c.form r₁).length (c.form r₂).length) :

depViolFeature P c r₁ r₂ = List.countP (fun (p : α × α) => decide (¬P p.1 ∧ P p.2)) ((c.form r₁).zip (c.form r₂))

Built from , ,

theorem Correspondence.identViolFeature_of_diagonal L562–567

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

identViolFeature proj c r₁ r₂ = List.countP (fun (p : α × α) => decide (proj p.1 ≠ proj p.2)) ((c.form r₁).zip (c.form r₂))

Built from , ,

L569–579

Symmetric correspondences

Read along the reverse edge of a symmetric correspondence, MAX is DEP and IDENT is unchanged.

L590–593

L595–596

L598–601

Edges that are graphs

An edge is the graph of a map f from the positions of form r₁ to those of form r₂ when each position i corresponds to f i alone. Such an edge violates neither MAX nor INTEGRITY, DEP counts the positions off the range of f, and UNIFORMITY and LINEARITY hold when f is injective and monotone.

Faithfulness as order isomorphism

An edge is faithful when it has no MAX, DEP, INTEGRITY, UNIFORMITY, or LINEARITY violation, which are exactly the conditions under which it is the graph of an order isomorphism (isFaithful_iff_exists_orderIso).

structure Correspondence.IsFaithful L659–667

{Role : Type u_1} {α : Type u_2} (c : Correspondence Role α) (r₁ r₂ : Role) :

Prop

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

Built from , , , , ,

Used by Correspondence.isFaithful_iff_exists_orderIso, Correspondence.length_eq_of_isFaithful

L669–680

L682–698

theorem Correspondence.isFaithful_iff_exists_orderIso L700–717

{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

Built from ,

L719–722

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 constraint counting the segments of the output is markedness and not faithfulness (exists_isMarkedness_not_isFaithfulness).

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

def Correspondence.IsFaithfulness L730–733

{α : Type u_2} (k : Constraint (Correspondence BinaryRole α)) :

Prop

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

Built from , ,

Used by Correspondence.isFaithfulness_maxViol, Correspondence.isFaithfulness_depViol, Correspondence.isFaithfulness_identViol, Correspondence.IsFaithfulness.not_antifaithful, Correspondence.exists_isMarkedness_not_isFaithfulness

Used in Alderete2001, RoseWalker2004

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

def Correspondence.IsMarkedness L735–737

{Role : Type u_1} {α : Type u_2} (out : Role) (k : Constraint (Correspondence Role α)) :

Prop

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

Built from

Used by Correspondence.isMarkedness_comap, Correspondence.isMarkedness_iff_exists_comap, Correspondence.exists_isMarkedness_not_isFaithfulness

Used in Alderete2001, RoseWalker2004

L739–741

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

theorem Correspondence.isMarkedness_iff_exists_comap L743–747

{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

Built from ,

L749–750

L752–753

L755–757

The anti-faithfulness constraint of a faithfulness constraint is not faithfulness, since the fully faithful candidate violates it.

theorem Correspondence.IsFaithfulness.not_antifaithful L759–763

{α : Type u_2} {k : Constraint (Correspondence BinaryRole α)} (hk : IsFaithfulness k) :

¬IsFaithfulness k.antifaithful

Built from , ,

L765–768