Alderete 2001: dominance effects as transderivational anti-faithfulness

For every faithfulness constraint F there is an anti-faithfulness constraint ¬F, satisfied exactly when F is violated at least once. Ranked above F on a base–derivative correspondence that only some affixes subcategorize for, ¬F forces one alternation in the shared stem and no more: ¬IDENT[voice] gives the Luo plural's voicing exchange, ¬MAX(Accent) the accent deletion of Japanese dominant affixes — accented or not — and ¬NOFLOP(Tone) the dragging-to-falling mutation of Limburg Dutch. Because ¬F reads the base–derivative relation, only an accent of the base can satisfy it (strict base mutation), and what replaces the deleted structure is decided by the rest of the grammar (grammar-dependence).

This file defines the transderivational diagram tct, the accent constraints on it, and the paper's tableaux: luo_exchange (11), dominant_accented (21), recessive (22), dominant_unaccented (23), dragging_mutates (52), falling_stays (53). strict_base_mutation is (27) as a theorem about Constraint.antifaithful; the row theorems dominant_rows and recessive_rows read (1), (17), (18) off the data.

References

• [Ald01]
• [Ald99]
• [Ben97]
• [McCP95]

Transderivational correspondence

inductive Alderete2001.Role : Type

The roles of a transderivational diagram are the input, its base, and the derivative.

• input : Role
• base : Role
• output : Role

@[instance_reducible]

instance Alderete2001.instDecidableEqRole : DecidableEq Role

Equations

• Alderete2001.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

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

Equations

• Alderete2001.instReprRole.repr Alderete2001.Role.input prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alderete2001.Role.input")).group prec✝
• Alderete2001.instReprRole.repr Alderete2001.Role.base prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alderete2001.Role.base")).group prec✝
• Alderete2001.instReprRole.repr Alderete2001.Role.output prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alderete2001.Role.output")).group prec✝

@[instance_reducible]

instance Alderete2001.instReprRole : Repr Role

Equations

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

def Alderete2001.tct {α : Type u_1} (input base output : List α) : OptimalityTheory.Correspondence Role α

In the diagram of (8) the input and the base each correspond diagonally to the derivative.

Equations

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

theorem Alderete2001.strict_base_mutation {α : Type u_1} (P : α → Prop) [DecidablePred P] (c : OptimalityTheory.Correspondence Role α) (r₁ r₂ : Role) (h : OptimalityTheory.Constraint.antifaithful ((fun (n : ℕ) (x : Unit) => n) (OptimalityTheory.Correspondence.maxViolFeature P c r₁ r₂)) () = 0) : ∃ p ∈ c.edge r₁ r₂, P (c.form r₁)[p.1] ∧ ¬P (c.form r₂)[p.2]

Satisfying ¬F for F the loss of P along some correspondence means some correspondent of that relation loses P: anti-faithfulness on a base–derivative relation can only be met by mutating the base ((27)).

Luo: voicing exchange ((6), (11))

structure Alderete2001.Seg : Type

A Luo segment with its voicing where contrastive.

• sym : Char
• voice : Option Bool

@[instance_reducible]

instance Alderete2001.instDecidableEqSeg : DecidableEq Seg

Equations

• Alderete2001.instDecidableEqSeg = Alderete2001.instDecidableEqSeg.decEq

def Alderete2001.instDecidableEqSeg.decEq (x✝ x✝¹ : Seg) : Decidable (x✝ = x✝¹)

Equations

• Alderete2001.instDecidableEqSeg.decEq { sym := a, voice := a_1 } { sym := b, voice := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Alderete2001.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Alderete2001.instReprSeg : Repr Seg

Equations

• Alderete2001.instReprSeg = { reprPrec := Alderete2001.instReprSeg.repr }

def Alderete2001.b : Seg

Equations

• Alderete2001.b = { sym := 'b', voice := some true }

def Alderete2001.p : Seg

Equations

• Alderete2001.p = { sym := 'p', voice := some false }

def Alderete2001.t : Seg

Equations

• Alderete2001.t = { sym := 't', voice := some false }

def Alderete2001.d : Seg

Equations

• Alderete2001.d = { sym := 'd', voice := some true }

def Alderete2001.a : Seg

Equations

• Alderete2001.a = { sym := 'a', voice := none }

def Alderete2001.e : Seg

Equations

• Alderete2001.e = { sym := 'e', voice := none }

def Alderete2001.ooIdentVoice (base : List Seg) : OptimalityTheory.Constraint (List Seg)

OO-IDENT[voice] between a base and a candidate derivative (10a).

Equations

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

theorem Alderete2001.luo_exchange : (OptimalityTheory.Tableau.ofRanking [[b, e, t, e], [b, e, d, e], [p, e, d, e]] [(ooIdentVoice [b, a, t]).antifaithful, ooIdentVoice [b, a, t]] luo_exchange._proof_1).optimal = {[b, e, d, e]}

In (11a), under ¬OO-IDENT[voice] ≫ OO-IDENT[voice] the plural of bat is bed-e. The faithful bet-e violates the anti-faithfulness constraint, and the total reversal ped-e satisfies it only with a gratuitous second violation of faithfulness.

Japanese: dominance effects ((17), (18), (21)–(23))

structure Alderete2001.Syl : Type

A syllable with its accent.

• form : String
• accent : Bool

@[instance_reducible]

instance Alderete2001.instDecidableEqSyl : DecidableEq Syl

Equations

• Alderete2001.instDecidableEqSyl = Alderete2001.instDecidableEqSyl.decEq

def Alderete2001.instDecidableEqSyl.decEq (x✝ x✝¹ : Syl) : Decidable (x✝ = x✝¹)

Equations

• Alderete2001.instDecidableEqSyl.decEq { form := a, accent := a_1 } { form := b, accent := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Alderete2001.instReprSyl : Repr Syl

Equations

• Alderete2001.instReprSyl = { reprPrec := Alderete2001.instReprSyl.repr }

def Alderete2001.instReprSyl.repr : Syl → ℕ → Std.Format

Equations

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

def Alderete2001.acc (s : String) : Syl

s accented, s' unaccented.

Equations

• Alderete2001.acc s = { form := s, accent := true }

def Alderete2001.un (s : String) : Syl

Equations

• Alderete2001.un s = { form := s, accent := false }

def Alderete2001.maxAccent (input base : List Syl) (r₁ : Role) : OptimalityTheory.Constraint (List Syl)

MAX(Accent) (14a) from role r₁ to the derivative.

Equations

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

def Alderete2001.depAccent (input base : List Syl) : OptimalityTheory.Constraint (List Syl)

DEP(Accent) (14b) from the input to the derivative.

Equations

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

def Alderete2001.culmin : OptimalityTheory.Constraint (List Syl)

CULMINATIVITY (15a) requires the word to bear an accent.

Equations

• Alderete2001.culmin = OptimalityTheory.Constraint.binary fun (out : List Alderete2001.Syl) => (out.all fun (x : Alderete2001.Syl) => !x.accent) = true

def Alderete2001.adaInput : List Syl

The inputs and bases of (21)–(23) are adá+ppó+i, yóm+tára and kóobe+kko.

Equations

• Alderete2001.adaInput = [Alderete2001.un "a", Alderete2001.acc "da", Alderete2001.acc "ppo", Alderete2001.un "i"]

def Alderete2001.adaBase : List Syl

Equations

• Alderete2001.adaBase = [Alderete2001.un "a", Alderete2001.acc "da"]

def Alderete2001.yomInput : List Syl

Equations

• Alderete2001.yomInput = [Alderete2001.acc "yom", Alderete2001.acc "ta", Alderete2001.un "ra"]

def Alderete2001.yomBase : List Syl

Equations

• Alderete2001.yomBase = [Alderete2001.acc "yon", Alderete2001.un "da"]

def Alderete2001.koobeInput : List Syl

Equations

• Alderete2001.koobeInput = [Alderete2001.acc "koo", Alderete2001.un "be", Alderete2001.un "kko"]

def Alderete2001.koobeBase : List Syl

Equations

• Alderete2001.koobeBase = [Alderete2001.acc "koo", Alderete2001.un "be"]

theorem Alderete2001.dominant_accented : (OptimalityTheory.Tableau.ofRanking [[un "a", acc "da", un "ppo", un "i"], [un "a", un "da", un "ppo", un "i"], [un "a", un "da", acc "ppo", un "i"]] [(maxAccent adaInput adaBase Role.base).antifaithful, maxAccent adaInput adaBase Role.base, maxAccent adaInput adaBase Role.input] dominant_accented._proof_1).optimal = {[un "a", un "da", acc "ppo", un "i"]}

In (21) the dominant accented suffix -ppó under ¬OO-MAX ≫ OO-MAX ≫ IO-MAX deletes the base accent and keeps its own, giving ada-ppó-i.

theorem Alderete2001.recessive : (OptimalityTheory.Tableau.ofRanking [[un "yon", acc "da", un "ra"], [acc "yon", un "da", un "ra"]] [maxAccent yomInput yomBase Role.base, (maxAccent yomInput yomBase Role.base).antifaithful] recessive._proof_1).optimal = {[acc "yon", un "da", un "ra"]}

In (22) the recessive suffix -tára, with OO-MAX ≫ ¬OO-MAX, leaves the base accent, giving yón-dara.

theorem Alderete2001.dominant_unaccented : (OptimalityTheory.Tableau.ofRanking [[acc "koo", un "be", un "kko"], [un "koo", acc "be", un "kko"], [un "koo", un "be", un "kko"]] [(maxAccent koobeInput koobeBase Role.base).antifaithful, depAccent koobeInput koobeBase, culmin] dominant_unaccented._proof_1).optimal = {[un "koo", un "be", un "kko"]}

In (23) the dominant unaccented suffix -kko deletes the base accent, and with IO-DEP(Accent) ≫ CULMIN nothing replaces it, giving koobe-kko, unaccented like any accentless word.

Limburg Dutch: dragging tone mutation ((42), (52)–(53))

A tonic syllable is its two moras' H links: the dragging tone is doubly linked, the falling tone linked on the first mora only, and a rising tone — linked on the second only — is unattested.

def Alderete2001.alignL : OptimalityTheory.Constraint (List Bool)

ALIGN-L(H, σ) (44): a linked H must be linked to the first mora.

Equations

• Alderete2001.alignL = OptimalityTheory.Constraint.binary fun (t : List Bool) => t.head? = some false ∧ t.any id = true

def Alderete2001.noFlop (base : List Bool) : OptimalityTheory.Constraint (List Bool)

NOFLOP(Tone) between a base and a candidate counts the links of the base lost in the derivative.

Equations

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

def Alderete2001.noSpread (base : List Bool) : OptimalityTheory.Constraint (List Bool)

NOSPREAD(Tone) counts the links inserted in the derivative.

Equations

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

theorem Alderete2001.dragging_mutates : (OptimalityTheory.Tableau.ofRanking [[true, false], [true, true], [false, true]] [alignL, (noFlop [true, true]).antifaithful, noFlop [true, true]] dragging_mutates._proof_1).optimal = {[true, false]}

In (52), under ALIGN-L ≫ ¬OO-NOFLOP ≫ OO-NOFLOP the dragging tone of káál loses its second link, giving káal-ə, rather than its first, which would leave a rising tone.

theorem Alderete2001.falling_stays : (OptimalityTheory.Tableau.ofRanking [[true, false], [true, true], [false, true]] [alignL, (noFlop [true, false]).antifaithful, noSpread [true, false]] dragging_mutates._proof_1).optimal = {[true, false]}

In (53) a falling-tone base cannot mutate, since losing its only link leaves the rising tone ALIGN-L bans and spreading it violates NOSPREAD, so stúur-ə stays faithful.

The data

def Alderete2001.stripAccent (s : String) : List Char

A form's characters with the accent mark removed.

Equations

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

theorem Alderete2001.dominant_rows (row : Datum) : row ∈ Examples.all → row.feature? "affixClass" = some "dominant" → stripAccent ((row.feature? "base").getD "") <+: row.primaryText.toList

As in (17) and (18), with a dominant affix the derivative begins with the base de-accented.

theorem Alderete2001.recessive_rows (row : Datum) : row ∈ Examples.all → row.feature? "affixClass" = some "recessive" → ((row.feature? "base").getD "").toList <+: row.primaryText.toList

As in (1), with a recessive affix the derivative begins with the base as it is.