Docs / Phonology / OptimalityTheory / Constraint / Alignment

Alignment constraints

import Linglib.Phonology.OptimalityTheory.Constraint.Alignment · namespace OptimalityTheory.Constraint

This file defines Generalized Alignment, the constraint family requiring each constituent of one category to share an edge with a constituent of another, assessed categorically. Constraint.align R scores a pair of constituent families with one violation for each member of the first family that bears R to no member of the second. Over the spans of a tree's constituents (RoseTree.spans), R comparing right edges gives Align-R, comparing left edges Align-L, and equality gives the Match constraints of Match Theory, which require both edges to coincide with those of one constituent of the other family. Constraint.deficiency R counts instead the members left without a partner when partners must be distinct, the MAX of a one-to-one correspondence. A constraint on candidates of another type is the Constraint.comap of either along the candidate's two families.

Main definitions

Constraint.align: Generalized Alignment of one family of constituents to another along R.
Constraint.alignLeft, Constraint.alignRight: Align-L and Align-R over spans, the edges compared at their left or their right cut.
Constraint.deficiency: the members of the first family left unpaired by a largest pairing with distinct members of the second along R.

Main results

Constraint.align_eq_zero_iff: a pair satisfies align R iff each member of the first family bears R to a member of the second.
Constraint.deficiency_le_align: correspondence along R demands no more than alignment along a relation contained in R that pairs no two members with one, as identity does Match.

References

McCarthy & Prince 1993b, Generalized Alignment
McCarthy & Prince 1995, Faithfulness and Reduplicative Identity formalized
Selkirk 2011, The Syntax-Phonology Interface

Declarations

Generalized Alignment (McCarthy & Prince 1993b) of one family of constituents to another along R, assessed categorically: one violation for each member of the first family that bears R to no member of the second. On spans, R comparing right or left edges is Align-R or Align-L, and equality is the Match constraint (Selkirk 2011).

def align L53–57

{β : Type u_1} {γ : Type u_2} (R : β → γ → Prop) [DecidableRel R] :

Constraint (List β × List γ)

align R x = List.countP (fun (a : β) => decide (∀ b ∈ x.2, ¬R a b)) x.1

Used by align_eq_zero_iff, alignLeft, alignRight, deficiency_le_align

Used in Phonology/Prosody/Match

theorem align_eq_zero_iff L61–62

{β : Type u_1} {γ : Type u_2} {R : β → γ → Prop} [DecidableRel R] {x : List β × List γ} :

align R x = 0 ↔ ∀ a ∈ x.1, ∃ b ∈ x.2, R a b

Built from

Align-L over spans, Align(Cat₁, L, Cat₂, L) (McCarthy & Prince 1993b): one violation for each span of the first family whose left cut begins no span of the second.

@[reducible, inline] abbrev alignLeft L64–66

Constraint (List (ℕ × ℕ) × List (ℕ × ℕ))

alignLeft = align fun (a b : ℕ × ℕ) => a.1 = b.1

Built from

Used in HartmannZimmermann2004, ItoMester2009

Align-R over spans, Align(Cat₁, R, Cat₂, R) (McCarthy & Prince 1993b): one violation for each span of the first family whose right cut ends no span of the second.

@[reducible, inline] abbrev alignRight L68–70

Constraint (List (ℕ × ℕ) × List (ℕ × ℕ))

alignRight = align fun (a b : ℕ × ℕ) => a.2 = b.2

Built from

One-to-one correspondence

Correspondence along R with each member of the second family answering to at most one of the first, the MAX of McCarthy & Prince 1995 under UNIFORMITY: one violation for each member of the first family left unpaired by a largest such pairing (List.le_matchingNumber_iff), the deficiency of R.

def deficiency L84–88

{β : Type u_1} {γ : Type u_2} (R : β → γ → Prop) [DecidableRel R] [DecidableEq γ] :

Constraint (List β × List γ)

deficiency R x = x.1.length - List.matchingNumber R x.1 x.2

Used by deficiency_le_align

Used in Phonology/Prosody/Match

Correspondence asks no more than alignment along a stricter relation: where S is contained in R and no two members of a duplicate-free family bear S to one member, the members left without a correspondent along R are among those bearing S to none.

theorem deficiency_le_align L92–103

{β : Type u_1} {γ : Type u_2} {R : β → γ → Prop} [DecidableRel R] [DecidableEq γ] {S : β → γ → Prop} [DecidableRel S] {x : List β × List γ} (hx : x.1.Nodup) (hSR : ∀ a ∈ x.1, ∀ (b : γ), S a b → R a b) (hS : ∀ a ∈ x.1, ∀ a' ∈ x.1, ∀ (b : γ), S a b → S a' b → a = a') :

deficiency R x ≤ align S x

Built from ,