Correspondence Theory

@cite{mccarthy-prince-1995} @cite{benua-1997}

Correspondence Theory (@cite{mccarthy-prince-1995}) replaces the PARSE/FILL approach to faithfulness (@cite{prince-smolensky-1993}) with a relation ℛ between strings. Faithfulness constraints are structural properties of ℛ — completeness (MAX, DEP), featural identity (IDENT), order preservation (LINEARITY), contiguity (CONTIGUITY), edge alignment (ANCHOR).

@cite{benua-1997} extends correspondence from binary input-output and base-reduplicant relations to a family of relations indexed by morphological/derivational role: I-O, B-R, I-R, O-O — and, in subsequent work, sympathy candidates, basemap projections (@cite{rolle-2018}), paradigm members (@cite{mccarthy-2005}), candidate-chain steps. The unifying object is a labeled diagram of strings: a finite indexed family of forms together with binary correspondence relations between them.

The unifying type: Corr Role α

A Corr Role α is a Role-indexed family of strings of α together with a Role × Role-indexed family of correspondence relations (sets of position-pairs). Each constraint family is a function Corr Role α → Role → Role → ℕ: MAX-IO is c.maxViol .input .output; IDENT-OO is c.identViol .o₁ .o₂. The "same constraint schema generates distinct constraints for each domain" claim of @cite{mccarthy-prince-1995} becomes literally true at the type level — there is one Corr.identViol; named instances are partial applications.

Edges as Finset

Correspondence relations are sets of position pairs (@cite{mccarthy-prince-1995} Definition 10), not ordered sequences — so edge returns Finset (ℕ × ℕ) rather than List (ℕ × ℕ). INTEGRITY (one-to-many) and UNIFORMITY (many-to-one) violations are then Finset.card of suitable filters, without indexing artifacts and with no double-counting.

The binary case: Side

For two-form correspondences (M&P 1995 binary I-O, B-R, etc.), the role type is Side (.lhs | .rhs). Constructors Corr.parallel s₁ s₂ and Corr.identity s produce Corr Side α. This is the substrate used by BasemapCorrespondence (matrix vs. basemap tier) and Process.Harmony.OT (input vs. output harmony tier). Multi-role theories supply their own Role enums — see TCT.lean, Transderivational.lean, BasemapCorrespondence.lean.

Out of scope

• Composition of correspondences. @cite{mccarthy-prince-1995} explicitly has no through-correspondence; correspondence is a labeled quiver, not a category — there is no composition law to formalize here.
• Path-based evaluation (stratal cycles, candidate chains). When needed, derive via Mathlib.Combinatorics.Quiver.Path over the role quiver — see Stratal.lean and TCT.lean.

inductive Phonology.Correspondence.Side : Type

The two roles for a binary correspondence diagram. The substrate role type for Corr.parallel and Corr.identity — the latter being the @cite{mccarthy-prince-1995} input-output binary case. Multi-role theories supply their own role enums.

• lhs : Side
• rhs : Side

@[implicit_reducible]

instance Phonology.Correspondence.instDecidableEqSide : DecidableEq Side

Equations

• Phonology.Correspondence.instDecidableEqSide x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phonology.Correspondence.instReprSide : Repr Side

Equations

• Phonology.Correspondence.instReprSide = { reprPrec := Phonology.Correspondence.instReprSide.repr }

def Phonology.Correspondence.instReprSide.repr : Side → ℕ → Std.Format

Equations

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

def Phonology.Correspondence.Side.label : Side → String

Display label for a Side (used in constraint names).

Equations

• Phonology.Correspondence.Side.lhs.label = "L"
• Phonology.Correspondence.Side.rhs.label = "R"

inductive Phonology.Correspondence.RedupRole : Type

The three roles for a reduplicative correspondence diagram (@cite{mccarthy-prince-1995} §3): underlying input, base output, and reduplicant output. Substrate role type for Corr.reduplication — the canonical (I, B, R) triple of M&P 1995 reduplicative correspondence. Sibling of Side (binary), TCT.Role (BR vs OO distinction), and StratalCorr.StratalRole (chain of strata).

The 3-role pattern with .input and .base is shared with TCT.Role (whose third role is .derivative for OO-correspondence over morphologically-related words rather than within-form reduplication). The architectural distinction between BR and OO is a role-type commitment, not a substrate distinction.

• input : RedupRole
• base : RedupRole
• reduplicant : RedupRole

@[implicit_reducible]

instance Phonology.Correspondence.instDecidableEqRedupRole : DecidableEq RedupRole

Equations

• Phonology.Correspondence.instDecidableEqRedupRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phonology.Correspondence.instReprRedupRole : Repr RedupRole

Equations

• Phonology.Correspondence.instReprRedupRole = { reprPrec := Phonology.Correspondence.instReprRedupRole.repr }

def Phonology.Correspondence.instReprRedupRole.repr : RedupRole → ℕ → Std.Format

Equations

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

def Phonology.Correspondence.RedupRole.label : RedupRole → String

Display label for a RedupRole (used in constraint names: MAX-IO, MAX-BR, IDENT-BR).

Equations

• Phonology.Correspondence.RedupRole.input.label = "I"
• Phonology.Correspondence.RedupRole.base.label = "B"
• Phonology.Correspondence.RedupRole.reduplicant.label = "R"

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

A correspondence diagram: a Role-indexed family of strings of α together with a Role × Role-indexed family of binary correspondence relations. The unifying object behind I-O / B-R / I-R / O-O / OP / LC / Stratal / Antifaith / MxBM-C correspondence theories.

@cite{mccarthy-prince-1995} Definition 10 (binary case): "Given two strings S₁, S₂, correspondence is a relation ℛ from the elements of S₁ to those of S₂." Generalized to multiple typed forms following @cite{benua-1997}.

edge r₁ r₂ is the set of position pairs (i, j) such that position i of form r₁ corresponds to position j of form r₂. The relation need not be a function: one-to-many (INTEGRITY) and many-to-one (UNIFORMITY) are permitted and counted by their constraint families.

The wf field guarantees position validity: any (i, j) ∈ edge r₁ r₂ satisfies i < (form r₁).length and j < (form r₂).length.

• form : Role → List α
• edge : Role → Role → Finset (ℕ × ℕ)
• wf (r₁ r₂ : Role) (p : ℕ × ℕ) : p ∈ self.edge r₁ r₂ → p.1 < (self.form r₁).length ∧ p.2 < (self.form r₂).length

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

(A.1) MAX — every element of form r₁ has a correspondent in form r₂.

Counts positions of form r₁ with no correspondent in form r₂ under edge r₁ r₂. MAX-IO prohibits deletion; MAX-BR demands total reduplication; MAX-OO is the basemap-faithfulness constraint of @cite{benua-1997}.

Equations

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

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

(A.2) DEP — every element of form r₂ has a correspondent in form r₁.

Counts positions of form r₂ with no correspondent in form r₁ under edge r₁ r₂. DEP-IO prohibits epenthesis; DEP-BR prohibits fixed default segmentism.

Equations

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

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

(A.3) IDENT — corresponding elements are featurally identical.

Counts pairs (i, j) ∈ edge r₁ r₂ where (form r₁)[i] ≠ (form r₂)[j]. IDENT-IO penalises featural unfaithfulness; IDENT-OO is the basemap and paradigm-uniformity constraint of @cite{benua-1997}, @cite{mccarthy-2005}, and the basemap-faithfulness layer of @cite{rolle-2018}.

For a featural variant comparing forms feature-by-feature (rather than by full segment identity), see identViolFeature.

Equations

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

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

(A.3) IDENT-[F]* — featural variant of IDENT. Counts pairs (i, j) ∈ edge r₁ r₂ where projecting both elements through proj : α → F yields different values. Used by Benua-style featural OO-IDENT (@cite{benua-1997} Ch 4 Tiberian Hebrew: IDENT-[continuant]) and by harmony systems (@cite{rose-walker-2011}: IDENT-[F] for the harmony feature).

Equations

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

@[reducible, inline]

abbrev Phonology.Correspondence.Corr.IsContiguous (l : List ℕ) : Prop

A list of natural numbers is contiguous (no gaps) iff its consecutive elements differ by 1. Defined as List.IsChain (fun a b => b = a + 1) — mathlib's standard "consecutive" predicate.

Equations

• Phonology.Correspondence.Corr.IsContiguous l = List.IsChain (fun (a b : ℕ) => b = a + 1) l

@[implicit_reducible]

instance Phonology.Correspondence.Corr.instDecidableIsContiguous (l : List ℕ) : Decidable (IsContiguous l)

Equations

• Phonology.Correspondence.Corr.instDecidableIsContiguous l = l.instDecidableIsChainOfDecidableRel

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

(A.4a) I-CONTIGUITY — "No Skipping." Domain(ℛ) is a contiguous substring of form r₁. Violated by internal deletion.

Equations

• c.contigIViol r₁ r₂ = if Phonology.Correspondence.Corr.IsContiguous ((Finset.image Prod.fst (c.edge r₁ r₂)).sort fun (x1 x2 : ℕ) => x1 ≤ x2) then 0 else 1

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

(A.4b) O-CONTIGUITY — "No Intrusion." Range(ℛ) is a contiguous substring of form r₂. Violated by internal epenthesis.

Equations

• c.contigOViol r₁ r₂ = if Phonology.Correspondence.Corr.IsContiguous ((Finset.image Prod.snd (c.edge r₁ r₂)).sort fun (x1 x2 : ℕ) => x1 ≤ x2) then 0 else 1

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

(A.5a) L-ANCHOR — leftmost positions correspond. Binary 0/1. In prefixing reduplication, L-ANCHOR-BR ≫ R-ANCHOR-BR.

Equations

• c.anchorLViol r₁ r₂ = if (c.form r₁).length = 0 ∨ (c.form r₂).length = 0 then 0 else if (0, 0) ∈ c.edge r₁ r₂ then 0 else 1

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

(A.5b) R-ANCHOR — rightmost positions correspond.

Equations

• c.anchorRViol r₁ r₂ = if (c.form r₁).length = 0 ∨ (c.form r₂).length = 0 then 0 else if ((c.form r₁).length - 1, (c.form r₂).length - 1) ∈ c.edge r₁ r₂ then 0 else 1

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

(A.6) LINEARITY — "No Metathesis." Counts inversion pairs (i₁, j₁), (i₂, j₂) ∈ edge with i₁ < i₂ but j₂ < j₁.

Equations

• c.linearityViol r₁ r₂ = ∑ p ∈ c.edge r₁ r₂, {q ∈ c.edge r₁ r₂ | p.1 < q.1 ∧ q.2 < p.2}.card

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

(A.7) UNIFORMITY — "No Coalescence." Counts positions of form r₂ with multiple correspondents in form r₁.

Equations

• c.uniformityViol r₁ r₂ = {j ∈ Finset.range (c.form r₂).length | {p ∈ c.edge r₁ r₂ | p.2 = j}.card > 1}.card

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

(A.8) INTEGRITY — "No Breaking." Counts positions of form r₁ with multiple correspondents in form r₂.

Equations

• c.integrityViol r₁ r₂ = {i ∈ Finset.range (c.form r₁).length | {p ∈ c.edge r₁ r₂ | p.1 = i}.card > 1}.card

theorem Phonology.Correspondence.Corr.range_image_wf (n m₁ m₂ : ℕ) (h₁ : n ≤ m₁) (h₂ : n ≤ m₂) (p : ℕ × ℕ) : p ∈ Finset.image (fun (i : ℕ) => (i, i)) (Finset.range n) → p.1 < m₁ ∧ p.2 < m₂

Generic well-formedness lemma: parallel-pair edges of length n (0,0), (1,1), …, (n-1, n-1) are well-formed for any pair of forms of length ≥ n. The substrate wf proof every multi-role Corr constructor reduces to.

def Phonology.Correspondence.Corr.diagram {α : Type u_2} {Role : Type u_3} (form : Role → List α) (hasEdge : Role → Role → Bool) : Corr Role α

The unifying Corr constructor: build a correspondence diagram from a Role → List α form function plus a Role → Role → Bool edge predicate. Where hasEdge r₁ r₂ = true, a parallel-pair correspondence (0, 0), (1, 1), … is created, truncated to min of the two forms' lengths. Where false, no correspondence.

The substrate constructor for the major correspondence-theoretic architectures (M&P 1995 reduplication, Benua 1997 TCT, Rolle 2018 MxBM-C, stratal OT). Convenience wrappers Corr.parallel, Corr.identity, Corr.reduplication are 3-line specializations.

Symmetry: parallel-pair edges (i, i) are invariant under swap, so the (r₁, r₂) and (r₂, r₁) directions produce identical position-pair sets. Callers' hasEdge predicates are typically symmetric (e.g., · ≠ ·, adjacentStrata); the constructor does not enforce symmetry, but constraint families behave most predictably when it holds.

For non-parallel edge structures (infixation, morphologically- determined alignment, partial reduplication with skip patterns), use ParadigmUniformity.Transderivational.diagramWithEdge instead.

Equations

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

@[simp]

theorem Phonology.Correspondence.Corr.diagram_form {α : Type u_2} {Role : Type u_3} (form : Role → List α) (hasEdge : Role → Role → Bool) (r : Role) : (diagram form hasEdge).form r = form r

@[simp]

theorem Phonology.Correspondence.Corr.diagram_edge_of_true {α : Type u_2} {Role : Type u_3} (form : Role → List α) (hasEdge : Role → Role → Bool) {r₁ r₂ : Role} (h : hasEdge r₁ r₂ = true) : (diagram form hasEdge).edge r₁ r₂ = Finset.image (fun (i : ℕ) => (i, i)) (Finset.range (min (form r₁).length (form r₂).length))

@[simp]

theorem Phonology.Correspondence.Corr.diagram_edge_of_false {α : Type u_2} {Role : Type u_3} (form : Role → List α) (hasEdge : Role → Role → Bool) {r₁ r₂ : Role} (h : hasEdge r₁ r₂ = false) : (diagram form hasEdge).edge r₁ r₂ = ∅

def Phonology.Correspondence.Corr.parallel {α : Type u_2} (s₁ s₂ : List α) : Corr Side α

The parallel-pair correspondence between two strings. Forms .lhs ↦ s₁, .rhs ↦ s₂; for cross-side edges, position i of one is paired with position i of the other, ranging up to the shorter length. The substrate for Hamming-distance-style faithfulness on tier-projected forms — used by BasemapCorrespondence (matrix vs. basemap tonal tier) and Process.Harmony.OT (input vs. output harmony tier).

On unequal-length inputs, the truncation matches List.zip semantics: only positions < min s₁.length s₂.length are paired. For equal-length inputs, every position participates.

Defined as a thin wrapper around Corr.diagram.

Equations

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

def Phonology.Correspondence.Corr.identity {α : Type u_2} (s : List α) : Corr Side α

The identity correspondence on a single string. The fully-faithful candidate of @cite{mccarthy-prince-1995}: input = output, every position paired with itself.

Equations

• Phonology.Correspondence.Corr.identity s = Phonology.Correspondence.Corr.parallel s s

def Phonology.Correspondence.Corr.reduplication {α : Type u_2} (input base reduplicant : List α) : Corr RedupRole α

The reduplicative correspondence diagram: 3-role Corr RedupRole α over input + base + reduplicant forms. Cross-role edges are parallel-pair correspondences (truncated to the shorter form's length): (.input, .base) IO-correspondence, (.base, .reduplicant) BR-correspondence, (.input, .reduplicant) IR-correspondence (M&P 1995 §6 Full Model).

Defined as a thin wrapper around Corr.diagram with the off-diagonal edge predicate. The pre-Stage-2 hand-rolled version had 6 redundant reverse-direction match clauses (.image (p.2, p.1)) which are no-ops since parallel-pair edges (i, i) are symmetric under swap.

For non-parallel BR alignments (infixation, partial reduplication with morphologically-determined skip patterns), see ParadigmUniformity.Transderivational.diagramWithEdge for the explicit-edge variant.

Equations

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

@[simp]

theorem Phonology.Correspondence.Corr.reduplication_form_input {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).form RedupRole.input = input

@[simp]

theorem Phonology.Correspondence.Corr.reduplication_form_base {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).form RedupRole.base = base

@[simp]

theorem Phonology.Correspondence.Corr.reduplication_form_reduplicant {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).form RedupRole.reduplicant = reduplicant

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Phonology.Correspondence.Corr.parallel_edge_lhs_rhs {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).edge Side.lhs Side.rhs = Finset.image (fun (i : ℕ) => (i, i)) (Finset.range (min s₁.length s₂.length))

@[simp]

theorem Phonology.Correspondence.Corr.parallel_edge_rhs_lhs {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).edge Side.rhs Side.lhs = Finset.image (fun (i : ℕ) => (i, i)) (Finset.range (min s₁.length s₂.length))

theorem Phonology.Correspondence.Corr.identity_max_zero {α : Type u_2} (s : List α) : (identity s).maxViol Side.lhs Side.rhs = 0

Identity correspondence has zero MAX violations.

theorem Phonology.Correspondence.Corr.identity_dep_zero {α : Type u_2} (s : List α) : (identity s).depViol Side.lhs Side.rhs = 0

Identity correspondence has zero DEP violations.

theorem Phonology.Correspondence.Corr.identity_ident_zero {α : Type u_2} [DecidableEq α] (s : List α) : (identity s).identViol Side.lhs Side.rhs = 0

Identity correspondence has zero IDENT violations.

theorem Phonology.Correspondence.Corr.identity_identFeature_zero {α : Type u_2} {F : Type u_3} [DecidableEq F] (proj : α → F) (s : List α) : identViolFeature proj (identity s) Side.lhs Side.rhs = 0

Identity correspondence has zero featural-IDENT violations (for any feature projection).

theorem Phonology.Correspondence.Corr.maxViol_le_length {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : c.maxViol r₁ r₂ ≤ (c.form r₁).length

theorem Phonology.Correspondence.Corr.depViol_le_length {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : c.depViol r₁ r₂ ≤ (c.form r₂).length

theorem Phonology.Correspondence.Corr.uniformityViol_le_length {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : c.uniformityViol r₁ r₂ ≤ (c.form r₂).length

theorem Phonology.Correspondence.Corr.integrityViol_le_length {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : c.integrityViol r₁ r₂ ≤ (c.form r₁).length

def Phonology.Correspondence.Corr.toConstraint {Role : Type u_3} {α : Type u_4} (family : Core.Constraint.OT.ConstraintFamily) (label : String) (eval : Corr Role α → ℕ) : Core.Constraint.OT.NamedConstraint (Corr Role α)

Build a NamedConstraint from a Corr-violation function. The single point of plumbing into Core.Constraint.OT's evaluation machinery — every named correspondence constraint factors through this.

Equations

• Phonology.Correspondence.Corr.toConstraint family label eval = { name := label, family := family, eval := eval }

def Phonology.Correspondence.Corr.toIdentConstraint {Role : Type u_3} {α : Type u_4} [DecidableEq α] (r₁ r₂ : Role) (label : String) : Core.Constraint.OT.NamedConstraint (Corr Role α)

IDENT as a NamedConstraint. Specializes toConstraint to identViol.

Equations

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

def Phonology.Correspondence.Corr.toIdentFeatureConstraint {Role : Type u_3} {α : Type u_4} {F : Type u_5} [DecidableEq F] (proj : α → F) (r₁ r₂ : Role) (label : String) : Core.Constraint.OT.NamedConstraint (Corr Role α)

IDENT-[F] as a NamedConstraint. Featural variant of toIdentConstraint.

Equations

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

def Phonology.Correspondence.Corr.toMaxConstraint {Role : Type u_3} {α : Type u_4} (r₁ r₂ : Role) (label : String) : Core.Constraint.OT.NamedConstraint (Corr Role α)

MAX as a NamedConstraint.

Equations

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

def Phonology.Correspondence.Corr.toDepConstraint {Role : Type u_3} {α : Type u_4} (r₁ r₂ : Role) (label : String) : Core.Constraint.OT.NamedConstraint (Corr Role α)

DEP as a NamedConstraint.

Equations

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

The canonical M&P 1995 reduplicative-faithfulness constraints, as NamedConstraint (Corr RedupRole α). Each is a 1-line specialization of the role-polymorphic Corr.toMaxConstraint/toIdentConstraint family above. Study files import these names instead of re-rolling Corr.toMaxConstraint .input .base "IO" inline at every callsite.

def Phonology.Correspondence.Reduplication.maxIO {α : Type u_1} : Core.Constraint.OT.NamedConstraint (Corr RedupRole α)

MAX-IO: every input segment has a base correspondent.

Equations

• Phonology.Correspondence.Reduplication.maxIO = Phonology.Correspondence.Corr.toMaxConstraint Phonology.Correspondence.RedupRole.input Phonology.Correspondence.RedupRole.base "IO"

def Phonology.Correspondence.Reduplication.maxBR {α : Type u_1} : Core.Constraint.OT.NamedConstraint (Corr RedupRole α)

MAX-BR: every base segment has a reduplicant correspondent (penalises partial reduplication).

Equations

• Phonology.Correspondence.Reduplication.maxBR = Phonology.Correspondence.Corr.toMaxConstraint Phonology.Correspondence.RedupRole.base Phonology.Correspondence.RedupRole.reduplicant "BR"

def Phonology.Correspondence.Reduplication.depIO {α : Type u_1} : Core.Constraint.OT.NamedConstraint (Corr RedupRole α)

DEP-IO: every base segment has an input correspondent (penalises epenthesis).

Equations

• Phonology.Correspondence.Reduplication.depIO = Phonology.Correspondence.Corr.toDepConstraint Phonology.Correspondence.RedupRole.input Phonology.Correspondence.RedupRole.base "IO"

def Phonology.Correspondence.Reduplication.identBR {α : Type u_1} [DecidableEq α] : Core.Constraint.OT.NamedConstraint (Corr RedupRole α)

IDENT-BR: corresponding base/reduplicant segments are featurally identical.

Equations

• Phonology.Correspondence.Reduplication.identBR = Phonology.Correspondence.Corr.toIdentConstraint Phonology.Correspondence.RedupRole.base Phonology.Correspondence.RedupRole.reduplicant "BR"

def Phonology.Correspondence.Reduplication.identIO {α : Type u_1} [DecidableEq α] : Core.Constraint.OT.NamedConstraint (Corr RedupRole α)

IDENT-IO: corresponding input/base segments are featurally identical.

Equations

• Phonology.Correspondence.Reduplication.identIO = Phonology.Correspondence.Corr.toIdentConstraint Phonology.Correspondence.RedupRole.input Phonology.Correspondence.RedupRole.base "IO"

def Phonology.Correspondence.Corr.RoleQuiv {Role : Type u_1} {α : Type u_2} : Corr Role α → Type u_1

A correspondence diagram c : Corr Role α carries a labeled-quiver structure on Role: the morphisms from r₁ to r₂ are the correspondence pairs (i, j) ∈ c.edge r₁ r₂. The Quiver instance cannot live on Role itself (it would need to depend on the value c); instead we wrap Role in a definitional newtype RoleQuiv c and put the Quiver instance there.

Use case: stratal/OT-CC chained evaluation, where derivations are paths in the role-quiver. Quiver.Path and the rest of mathlib's Combinatorics.Quiver API then become available.

Equations

• x✝.RoleQuiv = Role

@[implicit_reducible]

instance Phonology.Correspondence.Corr.instQuiverRoleQuiv {Role : Type u_1} {α : Type u_2} (c : Corr Role α) : Quiver c.RoleQuiv

Equations

• c.instQuiverRoleQuiv = { Hom := fun (r₁ r₂ : c.RoleQuiv) => ↥(c.edge r₁ r₂) }