McCarthy (2005): Optimal Paradigms

This file formalizes optimal paradigms after [McC05]. Entire inflectional paradigms are candidates: markedness and input–output faithfulness are summed over the members, and the stem of every member stands in a correspondence relation with the stem of every other, with no distinguished base, the symmetric counterpart of the base priority of [Ben97], which optimal paradigms leave to derivational morphology. Faithfulness on that relation resists alternation within the paradigm, and three consequences follow from the architecture alone: overapplication only, attraction to the unmarked, and majority rules. A paradigm carries the shared input and its members with their cells, surface stems, and input–stem correspondences (Paradigm), the correspondence diagram is read off those (Paradigm.corr), symmetric and base-free by construction, and markedness, ioFaith, and opFaith sum a constraint over the members or the ordered member pairs. The Classical Arabic tableaux for the right and left edges of the verb stem and for geminate verbs, the Moroccan majority-rules paradigm, and the Hebrew jussive paradigms of Benua are rerun under the paper's ranking.

References

• [McC05]
• [Ben97]

Paradigms as candidates

inductive McCarthy2005.Role : Type

The roles of a candidate paradigm: the shared input stem and the stem of each member.

• input : Role
• member (i : ℕ) : Role

def McCarthy2005.instDecidableEqRole.decEq (x✝ x✝¹ : Role) : Decidable (x✝ = x✝¹)

Equations

• McCarthy2005.instDecidableEqRole.decEq McCarthy2005.Role.input McCarthy2005.Role.input = isTrue ⋯
• McCarthy2005.instDecidableEqRole.decEq McCarthy2005.Role.input (McCarthy2005.Role.member i) = isFalse ⋯
• McCarthy2005.instDecidableEqRole.decEq (McCarthy2005.Role.member i) McCarthy2005.Role.input = isFalse ⋯
• McCarthy2005.instDecidableEqRole.decEq (McCarthy2005.Role.member a) (McCarthy2005.Role.member b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance McCarthy2005.instDecidableEqRole : DecidableEq Role

Equations

• McCarthy2005.instDecidableEqRole = McCarthy2005.instDecidableEqRole.decEq

def McCarthy2005.instReprRole.repr : Role → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• McCarthy2005.instReprRole.repr McCarthy2005.Role.input prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy2005.Role.input")).group prec✝

@[instance_reducible]

instance McCarthy2005.instReprRole : Repr Role

Equations

• McCarthy2005.instReprRole = { reprPrec := McCarthy2005.instReprRole.repr }

structure McCarthy2005.Member (α : Type u_3) (ι : Type u_4) : Type (max u_3 u_4)

A paradigm member: its inflectional cell, its surface stem, and the correspondence from the input to the stem.

• cell : ι
• stem : List α
• io : List (ℕ × ℕ)

structure McCarthy2005.Paradigm (α : Type u_3) (ι : Type u_4) : Type (max u_3 u_4)

A candidate paradigm (2a): the inflected forms of one input stem.

• input : List α
• members : List (Member α ι)

def McCarthy2005.Paradigm.stem {α : Type u_1} {ι : Type u_2} (P : Paradigm α ι) (i : ℕ) : List α

The stem of the ith member, empty beyond the paradigm.

Equations

• P.stem i = (Option.map McCarthy2005.Member.stem P.members[i]?).getD []

def McCarthy2005.Paradigm.io {α : Type u_1} {ι : Type u_2} (P : Paradigm α ι) (i : ℕ) : List (ℕ × ℕ)

The input correspondence of the ith member, empty beyond the paradigm.

Equations

• P.io i = (Option.map McCarthy2005.Member.io P.members[i]?).getD []

def McCarthy2005.compose (l₁ l₂ : List (ℕ × ℕ)) : List (ℕ × ℕ)

The positions of two stems that realise the same input position.

Equations

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

def McCarthy2005.epenthetic (l : List (ℕ × ℕ)) (n : ℕ) : List ℕ

The positions of a stem of length n without an input correspondent.

Equations

• McCarthy2005.epenthetic l n = List.filter (fun (p : ℕ) => decide (∀ rp ∈ l, rp.2 ≠ p)) (List.range n)

def McCarthy2005.site (l : List (ℕ × ℕ)) (p : ℕ) : Option ℕ

The site of a stem position: the last input position realised at or before it.

Equations

• McCarthy2005.site l p = (List.map Prod.fst (List.filter (fun (rp : ℕ × ℕ) => decide (rp.2 ≤ p)) l)).max?

def McCarthy2005.opPairs (l₁ l₂ : List (ℕ × ℕ)) (n₁ n₂ : ℕ) : List (ℕ × ℕ)

ℛ_OP between two stems of lengths n₁, n₂ with input correspondences l₁, l₂: the positions realising the same input position, and the epenthetic positions at the same site.

Equations

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

def McCarthy2005.Paradigm.corr {α : Type u_1} {ι : Type u_2} (P : Paradigm α ι) : OptimalityTheory.Correspondence Role α

The correspondence diagram of a candidate (2c): each member's input–stem relation, and between the stems of distinct members the relation ℛ_OP of opPairs.

Equations

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

def McCarthy2005.markedness {α : Type u_1} {ι : Type u_2} (m : ι → List α → ℕ) : OptimalityTheory.Constraint (Paradigm α ι)

A markedness constraint on the word of each cell, summed over the members (2b).

Equations

• McCarthy2005.markedness m P = (List.map (fun (x : McCarthy2005.Member α ι) => m x.cell x.stem) P.members).sum

def McCarthy2005.ioFaith {α : Type u_1} {ι : Type u_2} (f : OptimalityTheory.Correspondence Role α → Role → Role → ℕ) : OptimalityTheory.Constraint (Paradigm α ι)

An input–output faithfulness constraint summed over the members (2b).

Equations

• McCarthy2005.ioFaith f P = (List.map (fun (i : ℕ) => f P.corr McCarthy2005.Role.input (McCarthy2005.Role.member i)) (List.range P.members.length)).sum

def McCarthy2005.opFaith {α : Type u_1} {ι : Type u_2} (f : OptimalityTheory.Correspondence Role α → Role → Role → ℕ) : OptimalityTheory.Constraint (Paradigm α ι)

An OP faithfulness constraint (2d): a correspondence constraint summed over the ordered pairs of distinct members.

Equations

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

def McCarthy2005.tableau {α : Type u_1} {ι : Type u_2} {L : Type u_3} [DecidableEq L] (cand : L → Paradigm α ι) (labels : List L) (ranking : List (OptimalityTheory.Constraint (Paradigm α ι))) (h : labels ≠ [] := by decide) : OptimalityTheory.Tableau L (List.map (OptimalityTheory.Constraint.comap cand) ranking).length

The tableau of the labelled candidate paradigms under a ranking.

Equations

• McCarthy2005.tableau cand labels ranking h = OptimalityTheory.Tableau.ofRanking labels (List.map (OptimalityTheory.Constraint.comap cand) ranking) h

inductive McCarthy2005.Cand : Type

The candidate paradigms of a tableau.

• a : Cand
• b : Cand
• c : Cand
• d : Cand
• e : Cand

@[instance_reducible]

instance McCarthy2005.instDecidableEqCand : DecidableEq Cand

Equations

• McCarthy2005.instDecidableEqCand x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def McCarthy2005.instReprCand.repr : Cand → ℕ → Std.Format

Equations

• McCarthy2005.instReprCand.repr McCarthy2005.Cand.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy2005.Cand.a")).group prec✝
• McCarthy2005.instReprCand.repr McCarthy2005.Cand.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy2005.Cand.b")).group prec✝
• McCarthy2005.instReprCand.repr McCarthy2005.Cand.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy2005.Cand.c")).group prec✝
• McCarthy2005.instReprCand.repr McCarthy2005.Cand.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy2005.Cand.d")).group prec✝
• McCarthy2005.instReprCand.repr McCarthy2005.Cand.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy2005.Cand.e")).group prec✝

@[instance_reducible]

instance McCarthy2005.instReprCand : Repr Cand

Equations

• McCarthy2005.instReprCand = { reprPrec := McCarthy2005.instReprCand.repr }

Palatalization before -i (§8.2)

From /mat/ with the plural suffix -i, the paradigm ⟨mat, maʧi⟩ draws two OP-IDENT(high) marks, one on each direction of ℛ_OP, and ⟨ma, maʧi⟩ one OP-MAX and one OP-DEP mark (fn. 5).

inductive McCarthy2005.Palatalization.Seg : Type

• m : Seg
• a : Seg
• t : Seg
• ch : Seg
• i : Seg

@[instance_reducible]

instance McCarthy2005.Palatalization.instDecidableEqSeg : DecidableEq Seg

Equations

• McCarthy2005.Palatalization.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def McCarthy2005.Palatalization.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance McCarthy2005.Palatalization.instReprSeg : Repr Seg

Equations

• McCarthy2005.Palatalization.instReprSeg = { reprPrec := McCarthy2005.Palatalization.instReprSeg.repr }

def McCarthy2005.Palatalization.high : Seg → Option Bool

The feature distinguishing t from ʧ.

Equations

• McCarthy2005.Palatalization.high McCarthy2005.Palatalization.Seg.t = some false
• McCarthy2005.Palatalization.high McCarthy2005.Palatalization.Seg.ch = some true
• McCarthy2005.Palatalization.high x✝ = none

def McCarthy2005.Palatalization.mat : Paradigm Seg (List Seg)

⟨mat, maʧi⟩.

Equations

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

def McCarthy2005.Palatalization.ma : Paradigm Seg (List Seg)

⟨ma, maʧi⟩.

Equations

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

Arabic syllables and feet

The markedness constraints of §8.4 read syllable weight and foot structure. Each vowel is a nucleus, long or short by weight; the consonants before a vowel but the last, its onset, close the preceding syllable. Feet are right-to-left moraic trochees with the final syllable extrametrical, as the paper assumes; SWP marks a stressed light syllable, so an (LL) foot.

inductive McCarthy2005.Arabic.Seg : Type

• f : Seg
• ayn : Seg
• l : Seg
• s : Seg
• sh : Seg
• t : Seg
• j : Seg
• k : Seg
• b : Seg
• n : Seg
• m : Seg
• r : Seg
• hh : Seg
• g : Seg
• d : Seg
• ch : Seg
• x : Seg
• q : Seg
• w : Seg
• z : Seg
• zh : Seg
• a : Seg
• aa : Seg
• i : Seg
• ii : Seg
• u : Seg
• schwa : Seg

@[instance_reducible]

instance McCarthy2005.Arabic.instDecidableEqSeg : DecidableEq Seg

Equations

• McCarthy2005.Arabic.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance McCarthy2005.Arabic.instReprSeg : Repr Seg

Equations

• McCarthy2005.Arabic.instReprSeg = { reprPrec := McCarthy2005.Arabic.instReprSeg.repr }

def McCarthy2005.Arabic.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

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

def McCarthy2005.Arabic.IsVowel (c : Seg) : Prop

Equations

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

@[instance_reducible]

instance McCarthy2005.Arabic.instDecidablePredSegIsVowel : DecidablePred IsVowel

Equations

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

def McCarthy2005.Arabic.weight : Seg → Option Bool

The weight of a vowel: long or short.

Equations

• McCarthy2005.Arabic.weight McCarthy2005.Arabic.Seg.aa = some true
• McCarthy2005.Arabic.weight McCarthy2005.Arabic.Seg.ii = some true
• McCarthy2005.Arabic.weight McCarthy2005.Arabic.Seg.a = some false
• McCarthy2005.Arabic.weight McCarthy2005.Arabic.Seg.i = some false
• McCarthy2005.Arabic.weight McCarthy2005.Arabic.Seg.u = some false
• McCarthy2005.Arabic.weight McCarthy2005.Arabic.Seg.schwa = some false
• McCarthy2005.Arabic.weight x✝ = none

structure McCarthy2005.Arabic.Syllable : Type

A syllable by its nucleus and coda.

• nucleus : Seg
• coda : List Seg

@[instance_reducible]

instance McCarthy2005.Arabic.instDecidableEqSyllable : DecidableEq Syllable

Equations

• McCarthy2005.Arabic.instDecidableEqSyllable = McCarthy2005.Arabic.instDecidableEqSyllable.decEq

def McCarthy2005.Arabic.instDecidableEqSyllable.decEq (x✝ x✝¹ : Syllable) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance McCarthy2005.Arabic.instReprSyllable : Repr Syllable

Equations

• McCarthy2005.Arabic.instReprSyllable = { reprPrec := McCarthy2005.Arabic.instReprSyllable.repr }

def McCarthy2005.Arabic.instReprSyllable.repr : Syllable → ℕ → Std.Format

Equations

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

def McCarthy2005.Arabic.Syllable.moras (σ : Syllable) : ℕ

Equations

• σ.moras = (if McCarthy2005.Arabic.weight σ.nucleus = some true then 2 else 1) + σ.coda.length

def McCarthy2005.Arabic.closeLast (coda : List Seg) : List Syllable → List Syllable

Close the latest syllable with coda.

Equations

• McCarthy2005.Arabic.closeLast coda [] = []
• McCarthy2005.Arabic.closeLast coda (σ :: σs) = { nucleus := σ.nucleus, coda := coda } :: σs

def McCarthy2005.Arabic.syllabifyRev : List Syllable → List Seg → List Seg → List Syllable

The syllables of a word, latest first: a vowel opens a syllable, the consonants pending before it but its onset close the previous one, and the final consonants close the last.

Equations

• One or more equations did not get rendered due to their size.
• McCarthy2005.Arabic.syllabifyRev x✝¹ x✝ [] = McCarthy2005.Arabic.closeLast x✝ x✝¹

def McCarthy2005.Arabic.syllabify (w : List Seg) : List Syllable

Equations

• McCarthy2005.Arabic.syllabify w = (McCarthy2005.Arabic.syllabifyRev [] [] w).reverse

def McCarthy2005.Arabic.footRev (pending : Option Syllable) : List Syllable → List (List Syllable)

Right-to-left moraic trochees over syllables listed latest first, carrying a light syllable awaiting a partner: a heavy syllable is a foot, two light syllables are a foot, a lone light syllable is unparsed.

Equations

• McCarthy2005.Arabic.footRev pending [] = []
• McCarthy2005.Arabic.footRev none (σ :: σs) = if 2 ≤ σ.moras then [σ] :: McCarthy2005.Arabic.footRev none σs else McCarthy2005.Arabic.footRev (some σ) σs
• McCarthy2005.Arabic.footRev (some σ₀) (σ :: σs) = if 2 ≤ σ.moras then [σ] :: McCarthy2005.Arabic.footRev none σs else [σ, σ₀] :: McCarthy2005.Arabic.footRev none σs

def McCarthy2005.Arabic.feet (w : List Seg) : List (List Syllable)

The feet of a word, the final syllable extrametrical unless nothing else can be footed (fn. 22).

Equations

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

def McCarthy2005.Arabic.swp (w : List Seg) : ℕ

SWP: stressed light syllables, the heads of (LL) feet.

Equations

• McCarthy2005.Arabic.swp w = (List.filter (fun (ft : List McCarthy2005.Arabic.Syllable) => decide (ft.length = 2)) (McCarthy2005.Arabic.feet w)).length

def McCarthy2005.Arabic.superheavy (w : List Seg) : ℕ

Superheavy syllables, parsed with a moraic coda (*µµµ]σ) or a syllable appendix (*APP-σ).

Equations

• McCarthy2005.Arabic.superheavy w = (List.filter (fun (σ : McCarthy2005.Arabic.Syllable) => decide (3 ≤ σ.moras)) (McCarthy2005.Arabic.syllabify w)).length

def McCarthy2005.Arabic.alignL : List Seg → ℕ

ALIGN-L(Stem, σ): a stem-initial consonant before another is never syllable-initial.

Equations

• McCarthy2005.Arabic.alignL (c₁ :: c₂ :: tail) = if ¬McCarthy2005.Arabic.IsVowel c₁ ∧ ¬McCarthy2005.Arabic.IsVowel c₂ then 1 else 0
• McCarthy2005.Arabic.alignL x✝ = 0

def McCarthy2005.Arabic.identicalOnsets : List Seg → ℕ

*.CᵢV.CᵢV: identical consonants in the onsets of successive syllables.

Equations

• One or more equations did not get rendered due to their size.
• McCarthy2005.Arabic.identicalOnsets x✝ = 0

structure McCarthy2005.Arabic.Cell : Type

An inflectional cell of the Classical Arabic verb or noun: its affixes, and whether a superheavy coda is parsed as an appendix.

• prefixes : List Seg
• suffixes : List Seg
• appendix : Bool

def McCarthy2005.Arabic.instDecidableEqCell.decEq (x✝ x✝¹ : Cell) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance McCarthy2005.Arabic.instDecidableEqCell : DecidableEq Cell

Equations

• McCarthy2005.Arabic.instDecidableEqCell = McCarthy2005.Arabic.instDecidableEqCell.decEq

@[instance_reducible]

instance McCarthy2005.Arabic.instReprCell : Repr Cell

Equations

• McCarthy2005.Arabic.instReprCell = { reprPrec := McCarthy2005.Arabic.instReprCell.repr }

def McCarthy2005.Arabic.instReprCell.repr : Cell → ℕ → Std.Format

Equations

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

def McCarthy2005.Arabic.Cell.word (c : Cell) (stem : List Seg) : List Seg

The word of a stem in a cell.

Equations

• c.word stem = c.prefixes ++ stem ++ c.suffixes

The Classical Arabic verb (§8.4)

Verb stems end in CVC] and may begin with [CCV; noun stems may end in CVːC] or CVCC] and begin only with [CV. Verbs alone have C-initial suffixes and CV- prefixes: before a C-initial suffix a superheavy coda is shortened or broken up and OP faithfulness carries the repair through the paradigm; after a CV- prefix SWP blocks the epenthesis that alignment would force into a stem-initial cluster, and OP faithfulness carries the blocking to the unprefixed forms. The noun's one-member paradigms leave each form to markedness alone.

def McCarthy2005.Arabic.starTrimoraic : OptimalityTheory.Constraint (Paradigm Seg Cell)

*µµµ]σ.

Equations

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

def McCarthy2005.Arabic.starAppendix : OptimalityTheory.Constraint (Paradigm Seg Cell)

*APP-σ.

Equations

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

def McCarthy2005.Arabic.swpParadigm : OptimalityTheory.Constraint (Paradigm Seg Cell)

Equations

• McCarthy2005.Arabic.swpParadigm = McCarthy2005.markedness fun (c : McCarthy2005.Arabic.Cell) (s : List McCarthy2005.Arabic.Seg) => McCarthy2005.Arabic.swp (c.word s)

def McCarthy2005.Arabic.alignLParadigm : OptimalityTheory.Constraint (Paradigm Seg Cell)

Equations

• McCarthy2005.Arabic.alignLParadigm = McCarthy2005.markedness fun (x : McCarthy2005.Arabic.Cell) (s : List McCarthy2005.Arabic.Seg) => McCarthy2005.Arabic.alignL s

def McCarthy2005.Arabic.opDepV : OptimalityTheory.Constraint (Paradigm Seg Cell)

Equations

• McCarthy2005.Arabic.opDepV = McCarthy2005.opFaith (OptimalityTheory.Correspondence.depViolOn McCarthy2005.Arabic.IsVowel)

def McCarthy2005.Arabic.opIdentWt : OptimalityTheory.Constraint (Paradigm Seg Cell)

Equations

• McCarthy2005.Arabic.opIdentWt = McCarthy2005.opFaith (OptimalityTheory.Correspondence.identViolFeature McCarthy2005.Arabic.weight)

def McCarthy2005.Arabic.ioDepV : OptimalityTheory.Constraint (Paradigm Seg Cell)

Equations

• McCarthy2005.Arabic.ioDepV = McCarthy2005.ioFaith (OptimalityTheory.Correspondence.depViolOn McCarthy2005.Arabic.IsVowel)

def McCarthy2005.Arabic.ioMaxV : OptimalityTheory.Constraint (Paradigm Seg Cell)

Equations

• McCarthy2005.Arabic.ioMaxV = McCarthy2005.ioFaith (OptimalityTheory.Correspondence.maxViolOn McCarthy2005.Arabic.IsVowel)

def McCarthy2005.Arabic.ioMaxC : OptimalityTheory.Constraint (Paradigm Seg Cell)

Equations

• McCarthy2005.Arabic.ioMaxC = McCarthy2005.ioFaith (OptimalityTheory.Correspondence.maxViolOn fun (c : McCarthy2005.Arabic.Seg) => ¬McCarthy2005.Arabic.IsVowel c)

def McCarthy2005.Arabic.ioIdentWt : OptimalityTheory.Constraint (Paradigm Seg Cell)

Equations

• McCarthy2005.Arabic.ioIdentWt = McCarthy2005.ioFaith (OptimalityTheory.Correspondence.identViolFeature McCarthy2005.Arabic.weight)

def McCarthy2005.Arabic.ranking : List (OptimalityTheory.Constraint (Paradigm Seg Cell))

The summary ranking (21): IO-MAX-V, OP-DEP-V, *µµµ]σ, *APP-σ, IO-MAX-C, OP-IDENT-WT >> SWP >> ALIGN-L(Stem, σ) >> IO-DEP-V >> IO-IDENT-WT.

Equations

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

def McCarthy2005.Arabic.perfective : Cell

The 3sg.m. perfective, suffix -a.

Equations

• McCarthy2005.Arabic.perfective = { suffixes := [McCarthy2005.Arabic.Seg.a] }

def McCarthy2005.Arabic.perfective1 : Cell

The 1sg perfective, suffix -tu.

Equations

• McCarthy2005.Arabic.perfective1 = { suffixes := [McCarthy2005.Arabic.Seg.t, McCarthy2005.Arabic.Seg.u] }

def McCarthy2005.Arabic.imperfective : Cell

The 3sg.m. imperfective, ja- … -u.

Equations

• McCarthy2005.Arabic.imperfective = { prefixes := [McCarthy2005.Arabic.Seg.j, McCarthy2005.Arabic.Seg.a], suffixes := [McCarthy2005.Arabic.Seg.u] }

def McCarthy2005.Arabic.imperfectiveF : Cell

The 3pl.f. imperfective, ja- … -na.

Equations

• McCarthy2005.Arabic.imperfectiveF = { prefixes := [McCarthy2005.Arabic.Seg.j, McCarthy2005.Arabic.Seg.a], suffixes := [McCarthy2005.Arabic.Seg.n, McCarthy2005.Arabic.Seg.a] }

def McCarthy2005.Arabic.long : Cand → Paradigm Seg Cell

The paradigms of /faʕaːl/ in (12): shortened throughout, long throughout with the superheavy coda an appendix or moraic, or alternating.

Equations

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

def McCarthy2005.Arabic.long.input : List Seg

Equations

• McCarthy2005.Arabic.long.input = [McCarthy2005.Arabic.Seg.f, McCarthy2005.Arabic.Seg.a, McCarthy2005.Arabic.Seg.ayn, McCarthy2005.Arabic.Seg.aa, McCarthy2005.Arabic.Seg.l]

def McCarthy2005.Arabic.long.short : List Seg

Equations

• McCarthy2005.Arabic.long.short = [McCarthy2005.Arabic.Seg.f, McCarthy2005.Arabic.Seg.a, McCarthy2005.Arabic.Seg.ayn, McCarthy2005.Arabic.Seg.a, McCarthy2005.Arabic.Seg.l]

def McCarthy2005.Arabic.long.diag : List (ℕ × ℕ)

Equations

• McCarthy2005.Arabic.long.diag = OptimalityTheory.Correspondence.diagonalPairs 5

theorem McCarthy2005.Arabic.shortening_overapplies : (tableau long [Cand.a, Cand.b, Cand.c, Cand.d] ranking shortening_overapplies._proof_1).optimal = {Cand.a}

(12): the long vowel of /faʕaːl/ is shortened throughout the paradigm, ⟨faʕala, faʕaltu⟩ — overapplication of closed-syllable shortening, under OP-IDENT-WT >> IO-IDENT-WT.

def McCarthy2005.Arabic.cluster : Cand → Paradigm Seg Cell

The paradigms of /faʕl/ in (13): epenthesis throughout, the cluster kept throughout with the superheavy coda an appendix or moraic, or alternating.

Equations

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

def McCarthy2005.Arabic.cluster.input : List Seg

Equations

• McCarthy2005.Arabic.cluster.input = [McCarthy2005.Arabic.Seg.f, McCarthy2005.Arabic.Seg.a, McCarthy2005.Arabic.Seg.ayn, McCarthy2005.Arabic.Seg.l]

def McCarthy2005.Arabic.cluster.epenthesized : List Seg

Equations

• McCarthy2005.Arabic.cluster.epenthesized = [McCarthy2005.Arabic.Seg.f, McCarthy2005.Arabic.Seg.a, McCarthy2005.Arabic.Seg.ayn, McCarthy2005.Arabic.Seg.i, McCarthy2005.Arabic.Seg.l]

def McCarthy2005.Arabic.cluster.diag : List (ℕ × ℕ)

Equations

• McCarthy2005.Arabic.cluster.diag = OptimalityTheory.Correspondence.diagonalPairs 4

def McCarthy2005.Arabic.cluster.epenthetic : List (ℕ × ℕ)

A vowel epenthesized into the final cluster.

Equations

• McCarthy2005.Arabic.cluster.epenthetic = [(0, 0), (1, 1), (2, 2), (3, 4)]

theorem McCarthy2005.Arabic.epenthesis_overapplies : (tableau cluster [Cand.a, Cand.b, Cand.c, Cand.d] ranking shortening_overapplies._proof_1).optimal = {Cand.a}

(13): epenthesis into the final cluster of /faʕl/ carries through the paradigm, ⟨faʕila, faʕiltu⟩, under OP-DEP-V >> IO-DEP-V.

def McCarthy2005.Arabic.syncope : Cand → Paradigm Seg Cell

The paradigms of /faʕal/ in (17): the (LL) feet kept, or syncopated.

Equations

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

def McCarthy2005.Arabic.syncope.input : List Seg

Equations

• McCarthy2005.Arabic.syncope.input = [McCarthy2005.Arabic.Seg.f, McCarthy2005.Arabic.Seg.a, McCarthy2005.Arabic.Seg.ayn, McCarthy2005.Arabic.Seg.a, McCarthy2005.Arabic.Seg.l]

def McCarthy2005.Arabic.syncope.syncopated : List (ℕ × ℕ)

Equations

• McCarthy2005.Arabic.syncope.syncopated = [(0, 0), (1, 1), (2, 2), (4, 3)]

theorem McCarthy2005.Arabic.no_syncope : (tableau syncope [Cand.a, Cand.b] ranking no_syncope._proof_1).optimal = {Cand.a}

(17): SWP cannot force syncope, IO-MAX-V >> SWP.

def McCarthy2005.Arabic.noun : Cand → Paradigm Seg Cell

The noun /fʕal/ with the case suffixes in (24): epenthesis, or the initial cluster.

Equations

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

def McCarthy2005.Arabic.noun.input : List Seg

Equations

• McCarthy2005.Arabic.noun.input = [McCarthy2005.Arabic.Seg.f, McCarthy2005.Arabic.Seg.ayn, McCarthy2005.Arabic.Seg.a, McCarthy2005.Arabic.Seg.l]

def McCarthy2005.Arabic.noun.cases : List Seg

Equations

• McCarthy2005.Arabic.noun.cases = [McCarthy2005.Arabic.Seg.u, McCarthy2005.Arabic.Seg.a, McCarthy2005.Arabic.Seg.i]

def McCarthy2005.Arabic.noun.epenthetic : List (ℕ × ℕ)

Equations

• McCarthy2005.Arabic.noun.epenthetic = [(0, 0), (1, 2), (2, 3), (3, 4)]

theorem McCarthy2005.Arabic.noun_epenthesis : (tableau noun [Cand.a, Cand.b] ranking no_syncope._proof_1).optimal = {Cand.a}

(24): a [CCV noun stem is broken up by epenthesis, which SWP does not block in a prefixless paradigm, ALIGN-L(Stem, σ) >> IO-DEP-V.

def McCarthy2005.Arabic.verbal (pfA pfTu impfU impfNa : Member Seg Cell) : List (Member Seg Cell)

The four representative cells of a verbal paradigm: the perfectives -a, -tu and the imperfectives ja-…-u, ja-…-na.

Equations

• McCarthy2005.Arabic.verbal pfA pfTu impfU impfNa = [pfA, pfTu, impfU, impfNa]

def McCarthy2005.Arabic.eighth : Cand → Paradigm Seg Cell

The paradigms of the eighth conjugation /ftaʕal/ in (19) and (25): the initial cluster kept throughout, epenthesis throughout, or epenthesis in the unprefixed forms only.

Equations

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

def McCarthy2005.Arabic.eighth.input : List Seg

Equations

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

def McCarthy2005.Arabic.eighth.ablaut : List Seg

The imperfective stem vowel.

Equations

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

def McCarthy2005.Arabic.eighth.epenthesized (s : List Seg) : List Seg

Equations

• McCarthy2005.Arabic.eighth.epenthesized s = List.take 1 s ++ [McCarthy2005.Arabic.Seg.i] ++ List.drop 1 s

def McCarthy2005.Arabic.eighth.diag : List (ℕ × ℕ)

Equations

• McCarthy2005.Arabic.eighth.diag = OptimalityTheory.Correspondence.diagonalPairs 6

def McCarthy2005.Arabic.eighth.epenthetic : List (ℕ × ℕ)

Equations

• McCarthy2005.Arabic.eighth.epenthetic = [(0, 0), (1, 2), (2, 3), (3, 4), (4, 5), (5, 6)]

theorem McCarthy2005.Arabic.attraction_to_the_unmarked : (tableau eighth [Cand.a, Cand.b, Cand.c] ranking attraction_to_the_unmarked._proof_1).optimal = {Cand.a}

(25): attraction to the unmarked — the prefixed jaftaʕilu, where epenthesis would make an (LL) foot, is the attractor, and ftaʕala keeps its misaligned cluster: OP-DEP-V >> SWP >> ALIGN-L(Stem, σ).

def McCarthy2005.Arabic.tenth : Cand → Paradigm Seg Cell

The paradigms of /stafʕaːl/ in (27), the candidates obeying the undominated constraints: levelled to the short, unepenthesized stem; epenthesized throughout; long before V-initial suffixes; epenthesized in the perfectives; or both.

Equations

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

def McCarthy2005.Arabic.tenth.input : List Seg

Equations

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

def McCarthy2005.Arabic.tenth.short : List Seg

Equations

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

def McCarthy2005.Arabic.tenth.ablaut : List Seg

Equations

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

def McCarthy2005.Arabic.tenth.shortAblaut : List Seg

Equations

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

def McCarthy2005.Arabic.tenth.epenthesized (s : List Seg) : List Seg

Equations

• McCarthy2005.Arabic.tenth.epenthesized s = List.take 1 s ++ [McCarthy2005.Arabic.Seg.i] ++ List.drop 1 s

def McCarthy2005.Arabic.tenth.diag : List (ℕ × ℕ)

Equations

• McCarthy2005.Arabic.tenth.diag = OptimalityTheory.Correspondence.diagonalPairs 7

def McCarthy2005.Arabic.tenth.epenthetic : List (ℕ × ℕ)

Equations

• McCarthy2005.Arabic.tenth.epenthetic = [(0, 0), (1, 2), (2, 3), (3, 4), (4, 5), (5, 6), (6, 7)]

theorem McCarthy2005.Arabic.two_attractors : (tableau tenth [Cand.a, Cand.b, Cand.c, Cand.d, Cand.e] ranking two_attractors._proof_1).optimal = {Cand.a}

(27): different members attract different edges — the prefixed imperfectives block epenthesis at the left edge via OP-DEP-V, the C-suffixed forms force shortening at the right edge via OP-IDENT-WT — under the single ranking (21).

Domination of OP faithfulness (§8.4.4)

Geminate verbs delete the vowel between their identical consonants before V-initial suffixes, ħmarra ~ ħmarartu, so *.CᵢV.CᵢV dominates IO-MAX-V and OP-MAX-V (29).

def McCarthy2005.Arabic.opMaxV : OptimalityTheory.Constraint (Paradigm Seg Cell)

Equations

• McCarthy2005.Arabic.opMaxV = McCarthy2005.opFaith (OptimalityTheory.Correspondence.maxViolOn McCarthy2005.Arabic.IsVowel)

def McCarthy2005.Arabic.geminate : Cand → Paradigm Seg Cell

The paradigms of /ħmarar/ in (29): the vowel deleted before V-initial suffixes, or kept throughout.

Equations

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

def McCarthy2005.Arabic.geminate.input : List Seg

Equations

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

def McCarthy2005.Arabic.geminate.ablaut : List Seg

Equations

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

def McCarthy2005.Arabic.geminate.diag : List (ℕ × ℕ)

Equations

• McCarthy2005.Arabic.geminate.diag = OptimalityTheory.Correspondence.diagonalPairs 6

def McCarthy2005.Arabic.geminate.deleted : List (ℕ × ℕ)

Equations

• McCarthy2005.Arabic.geminate.deleted = [(0, 0), (1, 1), (2, 2), (3, 3), (5, 4)]

theorem McCarthy2005.Arabic.geminate_alternation : (tableau geminate [Cand.a, Cand.b] ((markedness fun (c : Cell) (s : List Seg) => identicalOnsets (c.word s)) :: ranking) no_syncope._proof_1).optimal = {Cand.a}

(29): normal application — neither levelling wins, the vowel/zero alternation staying in the paradigm, *.CᵢV.CᵢV >> IO-MAX-V, OP-MAX-V.

Moroccan Arabic majority rules (§8.5.1)

Schwa is banned from open syllables and triconsonantal clusters are prohibited, so the phonology fixes CCəC before C-initial and CəCC before V-initial suffixes; the unaffixed verb joins the larger class, ʃrəb, whereas nouns — paradigms of one — follow SONCON.

def McCarthy2005.Arabic.schwaOpen (w : List Seg) : ℕ

*ə]σ.

Equations

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

def McCarthy2005.Arabic.ccc : List Seg → ℕ

*CCC.

Equations

• One or more equations did not get rendered due to their size.
• McCarthy2005.Arabic.ccc x✝ = 0

def McCarthy2005.Arabic.sonority : Seg → ℕ

Sonority: glide > liquid > nasal > fricative > stop.

Equations

• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.j = 5
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.w = 5
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.l = 4
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.r = 4
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.n = 3
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.m = 3
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.f = 2
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.s = 2
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.sh = 2
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.hh = 2
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.ayn = 2
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.x = 2
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.z = 2
• McCarthy2005.Arabic.sonority McCarthy2005.Arabic.Seg.zh = 2
• McCarthy2005.Arabic.sonority x✝ = 1

def McCarthy2005.Arabic.sonCon : List Seg → ℕ

SONCON (30), on a word of three consonants and a schwa: CəC₂C₃ wants C₂ more sonorous than C₃, CC₂əC₃ not.

Equations

• McCarthy2005.Arabic.sonCon [head, McCarthy2005.Arabic.Seg.schwa, c₂, c₃] = if McCarthy2005.Arabic.sonority c₂ > McCarthy2005.Arabic.sonority c₃ then 0 else 1
• McCarthy2005.Arabic.sonCon [head, c₂, McCarthy2005.Arabic.Seg.schwa, c₃] = if McCarthy2005.Arabic.sonority c₂ > McCarthy2005.Arabic.sonority c₃ then 1 else 0
• McCarthy2005.Arabic.sonCon x✝ = 0

def McCarthy2005.Arabic.moroccanRanking : List (OptimalityTheory.Constraint (Paradigm Seg (List Seg)))

The ranking of (32): *ə]σ, *CCC >> OP-MAX-V >> SONCON >> IO-MAX-V, IO-DEP-V.

Equations

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

def McCarthy2005.Arabic.ccec (suffix : List Seg) : Member Seg (List Seg)

A CCəC member from /ʃərb/: the input schwa deleted, a schwa epenthesized.

Equations

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

def McCarthy2005.Arabic.cecc (suffix : List Seg) : Member Seg (List Seg)

A CəCC member from /ʃərb/.

Equations

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

def McCarthy2005.Arabic.suffixes : List (List Seg)

The suffixes of the perfective paradigm (31): none, four C-initial, two V-initial.

Equations

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

def McCarthy2005.Arabic.drink : Cand → Paradigm Seg (List Seg)

The paradigms of /ʃərb/ in (32): the unaffixed verb CCəC or CəCC with the rest fixed by the phonology, or levelled to CCəC or to CəCC throughout.

Equations

• One or more equations did not get rendered due to their size.
• McCarthy2005.Arabic.drink McCarthy2005.Cand.c = { input := McCarthy2005.Arabic.drink.input, members := List.map McCarthy2005.Arabic.ccec McCarthy2005.Arabic.suffixes }
• McCarthy2005.Arabic.drink x✝ = { input := McCarthy2005.Arabic.drink.input, members := List.map McCarthy2005.Arabic.cecc McCarthy2005.Arabic.suffixes }

def McCarthy2005.Arabic.drink.input : List Seg

Equations

• McCarthy2005.Arabic.drink.input = [McCarthy2005.Arabic.Seg.sh, McCarthy2005.Arabic.Seg.schwa, McCarthy2005.Arabic.Seg.r, McCarthy2005.Arabic.Seg.b]

theorem McCarthy2005.Arabic.majority_rules : (tableau drink [Cand.a, Cand.b, Cand.c, Cand.d] moroccanRanking shortening_overapplies._proof_1).optimal = {Cand.a}

(32): majority rules — the unaffixed ʃrəb joins the five CCəC members against the two CəCC members, OP-MAX-V being violated once in each direction by every CCəC–CəCC pair (twenty against twenty-four marks).

Tiberian Hebrew jussives (§8.5.2)

The jussive truncates the final vowel of the imperfective, jibkɛ ~ jeːbk, and the final cluster is not broken up by the epenthesis nouns undergo — the underapplication [Ben97] derives from base priority. Under OP every candidate loses a vowel to truncation, and ⟨jibkɛ, jeːbk⟩ wins because its levelled rival ⟨jibəkɛ, jibɛk⟩ puts a schwa between an open and a following syllable, *VCəCV >> OP-MAX-V >> *CC# (33); into a rising-sonority cluster epenthesis applies in the jussive alone, SON-CON >> OP-MAX-V (fn. 34). The segments and the markedness constraints are those of the [Ben97] study, whose winners the OP tableaux reproduce.

def McCarthy2005.Hebrew.twoSidedOpen : List Benua1997.Hebrew.Seg → ℕ

*VCəCV: a vowel between an open syllable and a following one.

Equations

• One or more equations did not get rendered due to their size.
• McCarthy2005.Hebrew.twoSidedOpen x✝ = 0

def McCarthy2005.Hebrew.ranking : List (OptimalityTheory.Constraint (Paradigm Benua1997.Hebrew.Seg Unit))

*VCəCV, SON-CON >> OP-MAX-V >> *CC#.

Equations

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

def McCarthy2005.Hebrew.jussive (x y : Benua1997.Hebrew.Seg) : Cand → Paradigm Benua1997.Hebrew.Seg Unit

The paradigms of an imperfective and its truncated jussive from a stem ending in the cluster x y: the cluster kept, epenthesis throughout, or epenthesis in the jussive alone.

Equations

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

def McCarthy2005.Hebrew.jussive.stem (x y : Benua1997.Hebrew.Seg) : List Benua1997.Hebrew.Seg

Equations

• McCarthy2005.Hebrew.jussive.stem x y = [Benua1997.Hebrew.Seg.glide, Benua1997.Hebrew.Seg.vowel, x, y, Benua1997.Hebrew.Seg.vowel]

def McCarthy2005.Hebrew.jussive.epenthesized (x y : Benua1997.Hebrew.Seg) : List Benua1997.Hebrew.Seg

Equations

• McCarthy2005.Hebrew.jussive.epenthesized x y = [Benua1997.Hebrew.Seg.glide, Benua1997.Hebrew.Seg.vowel, x, Benua1997.Hebrew.Seg.vowel, y]

def McCarthy2005.Hebrew.jussive.epenthetic : List (ℕ × ℕ)

Equations

• McCarthy2005.Hebrew.jussive.epenthetic = [(0, 0), (1, 1), (2, 2), (3, 4)]

theorem McCarthy2005.Hebrew.cry : (tableau (jussive Benua1997.Hebrew.Seg.spirant Benua1997.Hebrew.Seg.stop) [Cand.a, Cand.b, Cand.c] ranking Arabic.attraction_to_the_unmarked._proof_1).optimal = {Cand.a}

(33): jibkɛ ~ jeːbk 'cry' — the cluster is kept, overapplication of epenthesis being blocked.

theorem McCarthy2005.Hebrew.uncover : (tableau (jussive Benua1997.Hebrew.Seg.spirant Benua1997.Hebrew.Seg.liquid) [Cand.a, Cand.b, Cand.c] ranking Arabic.attraction_to_the_unmarked._proof_1).optimal = {Cand.c}

fn. 34: jɛɣlɛ ~ jɛɣɛl 'uncover' — into a rising-sonority cluster epenthesis applies in the jussive alone, OP-MAX-V being dominated by SON-CON.