Rose & Walker (2004): A Typology of Consonant Agreement as Correspondence

This file formalizes the paper's account of long-distance consonant agreement: consonants of an output that are similar enough stand in a correspondence relation, demanded by CORR constraints arrayed in a fixed hierarchy by similarity, and IDENT-CC constraints require correspondents to agree in the harmonizing feature, so that intervening segments are neutral and agreement holds between exactly the pairs whose CORR constraint outranks the input–output faithfulness resisting the change. The nasal case studies are formalized: the nasal correspondence hierarchy (nasalSimilarity, corr), IDENT-OI(nasal) interpolated at a cut in it, and the typology winner_eq, that a nasal and an oral consonant agree in the optimal output exactly when their pair is at least as similar as the cut, so that demoting the faithfulness constraint only widens the agreeing class (agree_of_le). Ngbaka cuts the hierarchy below the homorganic nasal–prenasal pairs, and its words are the fixed points of that grammar (ngbaka_rows); Kikongo cuts it below every nasal–voiced-stop and nasal–approximant pair and splits IDENT-CC by direction, so that only consonants to the right of a nasal agree, and its alternations are the rows of kikongo_rows, with the paper's tableaux for the agreeing suffix, the neutral voiceless stop, and the direction of agreement reproduced over generated or the paper's own candidates.

Implementation notes

Segments are the paper's chart of stop series on the nasality–voicing continuum by place, approximants, fricatives, and vocoids; a candidate is an output string aligned with the input and a correspondence relation among its consonants, listed as coindexed pairs. CORR constraints count the consonant pairs at least as similar as their stratum that fail to correspond, the directional IDENT-CC constraints the coindexed pairs in which a nasal is followed, or preceded, by an oral correspondent, and IDENT-OI(nasal) the consonants nasalized. GEN keeps or nasalizes each consonant and coindexes the consonants by any partition; the tableau of the paper's five-consonant directional example is over the paper's own candidates. Kikongo's surface map harmonize is the analysis's generalization, rightward agreement at the Kikongo cut with NC clusters neither triggering nor undergoing, which the paper attributes to a constraint on the structural roles of correspondents; that constraint, the exclusion of prefixes from the stem domain, and the laryngeal case studies are not formalized. Transcriptions omit tone, and the example numbers of the rows are those of the manuscript [RW01].

References

• [RW04a]
• [RW01]
• [McCP95]
• [PS93]

Segments and similarity

inductive RoseWalker2004.Place : Type

The places of articulation of the stops.

• labial : Place
• coronal : Place
• dorsal : Place

@[instance_reducible]

instance RoseWalker2004.instDecidableEqPlace : DecidableEq Place

Equations

• RoseWalker2004.instDecidableEqPlace x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance RoseWalker2004.instReprPlace : Repr Place

Equations

• RoseWalker2004.instReprPlace = { reprPrec := RoseWalker2004.instReprPlace.repr }

def RoseWalker2004.instReprPlace.repr : Place → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance RoseWalker2004.instFintypePlace : Fintype Place

Equations

• RoseWalker2004.instFintypePlace = { elems := { val := ↑RoseWalker2004.Place.enumList, nodup := RoseWalker2004.Place.enumList_nodup }, complete := RoseWalker2004.instFintypePlace._proof_1 }

inductive RoseWalker2004.Series : Type

The series of stops on the nasality–voicing continuum.

• voiceless : Series
• voiced : Series
• prenasal : Series
• nasal : Series

@[instance_reducible]

instance RoseWalker2004.instDecidableEqSeries : DecidableEq Series

Equations

• RoseWalker2004.instDecidableEqSeries x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RoseWalker2004.instReprSeries.repr : Series → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance RoseWalker2004.instReprSeries : Repr Series

Equations

• RoseWalker2004.instReprSeries = { reprPrec := RoseWalker2004.instReprSeries.repr }

@[instance_reducible]

instance RoseWalker2004.instFintypeSeries : Fintype Series

Equations

• RoseWalker2004.instFintypeSeries = { elems := { val := ↑RoseWalker2004.Series.enumList, nodup := RoseWalker2004.Series.enumList_nodup }, complete := RoseWalker2004.instFintypeSeries._proof_1 }

inductive RoseWalker2004.Seg : Type

A segment: a stop of some place and series, an approximant consonant, a fricative, or a vocoid.

• stop (place : Place) (series : Series) : Seg
• approximant : Seg
• fricative : Seg
• vocoid : Seg

@[instance_reducible]

instance RoseWalker2004.instDecidableEqSeg : DecidableEq Seg

Equations

• RoseWalker2004.instDecidableEqSeg = RoseWalker2004.instDecidableEqSeg.decEq

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

Equations

• RoseWalker2004.instDecidableEqSeg.decEq (RoseWalker2004.Seg.stop a a_1) (RoseWalker2004.Seg.stop b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• RoseWalker2004.instDecidableEqSeg.decEq (RoseWalker2004.Seg.stop place series) RoseWalker2004.Seg.approximant = isFalse ⋯
• RoseWalker2004.instDecidableEqSeg.decEq (RoseWalker2004.Seg.stop place series) RoseWalker2004.Seg.fricative = isFalse ⋯
• RoseWalker2004.instDecidableEqSeg.decEq (RoseWalker2004.Seg.stop place series) RoseWalker2004.Seg.vocoid = isFalse ⋯
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.approximant (RoseWalker2004.Seg.stop place series) = isFalse ⋯
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.approximant RoseWalker2004.Seg.approximant = isTrue ⋯
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.approximant RoseWalker2004.Seg.fricative = isFalse RoseWalker2004.instDecidableEqSeg.decEq._proof_9
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.approximant RoseWalker2004.Seg.vocoid = isFalse RoseWalker2004.instDecidableEqSeg.decEq._proof_10
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.fricative (RoseWalker2004.Seg.stop place series) = isFalse ⋯
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.fricative RoseWalker2004.Seg.approximant = isFalse RoseWalker2004.instDecidableEqSeg.decEq._proof_12
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.fricative RoseWalker2004.Seg.fricative = isTrue ⋯
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.fricative RoseWalker2004.Seg.vocoid = isFalse RoseWalker2004.instDecidableEqSeg.decEq._proof_13
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.vocoid (RoseWalker2004.Seg.stop place series) = isFalse ⋯
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.vocoid RoseWalker2004.Seg.approximant = isFalse RoseWalker2004.instDecidableEqSeg.decEq._proof_15
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.vocoid RoseWalker2004.Seg.fricative = isFalse RoseWalker2004.instDecidableEqSeg.decEq._proof_16
• RoseWalker2004.instDecidableEqSeg.decEq RoseWalker2004.Seg.vocoid RoseWalker2004.Seg.vocoid = isTrue ⋯

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

Equations

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

@[instance_reducible]

instance RoseWalker2004.instReprSeg : Repr Seg

Equations

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

@[instance_reducible]

instance RoseWalker2004.instFintypeSeg : Fintype Seg

Equations

• RoseWalker2004.instFintypeSeg = Fintype.ofEquiv ((_ : RoseWalker2004.Place) × RoseWalker2004.Series ⊕ Unit ⊕ Unit ⊕ Unit) RoseWalker2004.Seg.proxyTypeEquiv

def RoseWalker2004.Seg.IsNasal : Seg → Prop

A nasal stop.

Equations

• (RoseWalker2004.Seg.stop place RoseWalker2004.Series.nasal).IsNasal = True
• x✝.IsNasal = False

@[instance_reducible]

instance RoseWalker2004.Seg.instDecidablePredIsNasal : DecidablePred IsNasal

Equations

• (RoseWalker2004.Seg.stop place RoseWalker2004.Series.nasal).instDecidablePredIsNasal = isTrue trivial
• (RoseWalker2004.Seg.stop place RoseWalker2004.Series.voiceless).instDecidablePredIsNasal = isFalse ⋯
• (RoseWalker2004.Seg.stop place RoseWalker2004.Series.voiced).instDecidablePredIsNasal = isFalse ⋯
• (RoseWalker2004.Seg.stop place RoseWalker2004.Series.prenasal).instDecidablePredIsNasal = isFalse ⋯
• RoseWalker2004.Seg.approximant.instDecidablePredIsNasal = isFalse RoseWalker2004.Seg.instDecidablePredIsNasal._proof_4
• RoseWalker2004.Seg.fricative.instDecidablePredIsNasal = isFalse RoseWalker2004.Seg.instDecidablePredIsNasal._proof_5
• RoseWalker2004.Seg.vocoid.instDecidablePredIsNasal = isFalse RoseWalker2004.Seg.instDecidablePredIsNasal._proof_6

def RoseWalker2004.Seg.IsConsonant (s : Seg) : Prop

A consonant.

Equations

• s.IsConsonant = (s ≠ RoseWalker2004.Seg.vocoid)

@[instance_reducible]

instance RoseWalker2004.Seg.instDecidablePredIsConsonant : DecidablePred IsConsonant

Equations

• s.instDecidablePredIsConsonant = { decide := !decide (s = RoseWalker2004.Seg.vocoid), reflects_decide := ⋯ }

def RoseWalker2004.Seg.nasalize : Seg → Seg

The nasal counterpart of a consonant: the nasal at a stop's place, the coronal nasal for an approximant.

Equations

• (RoseWalker2004.Seg.stop p series).nasalize = RoseWalker2004.Seg.stop p RoseWalker2004.Series.nasal
• RoseWalker2004.Seg.approximant.nasalize = RoseWalker2004.Seg.stop RoseWalker2004.Place.coronal RoseWalker2004.Series.nasal
• x✝.nasalize = x✝

def RoseWalker2004.nasalSimilarity : Seg → Seg → Option (Fin 4)

The strata of the nasal correspondence hierarchy, the similarity of a nasal to another consonant: identical nasals; heterorganic nasals or a homorganic nasal and prenasal stop; a heterorganic nasal and prenasal stop or a homorganic nasal and voiced stop; a heterorganic nasal and voiced stop or a nasal and an approximant. Pairs without a nasal, and pairs with a voiceless stop, a fricative, or a vocoid, are below the threshold of similarity.

Equations

• RoseWalker2004.nasalSimilarity (RoseWalker2004.Seg.stop p RoseWalker2004.Series.nasal) (RoseWalker2004.Seg.stop q RoseWalker2004.Series.nasal) = some (if p = q then 0 else 1)
• RoseWalker2004.nasalSimilarity (RoseWalker2004.Seg.stop p RoseWalker2004.Series.nasal) (RoseWalker2004.Seg.stop q RoseWalker2004.Series.prenasal) = some (if p = q then 1 else 2)
• RoseWalker2004.nasalSimilarity (RoseWalker2004.Seg.stop q RoseWalker2004.Series.prenasal) (RoseWalker2004.Seg.stop p RoseWalker2004.Series.nasal) = some (if p = q then 1 else 2)
• RoseWalker2004.nasalSimilarity (RoseWalker2004.Seg.stop p RoseWalker2004.Series.nasal) (RoseWalker2004.Seg.stop q RoseWalker2004.Series.voiced) = some (if p = q then 2 else 3)
• RoseWalker2004.nasalSimilarity (RoseWalker2004.Seg.stop q RoseWalker2004.Series.voiced) (RoseWalker2004.Seg.stop p RoseWalker2004.Series.nasal) = some (if p = q then 2 else 3)
• RoseWalker2004.nasalSimilarity (RoseWalker2004.Seg.stop place RoseWalker2004.Series.nasal) RoseWalker2004.Seg.approximant = some 3
• RoseWalker2004.nasalSimilarity RoseWalker2004.Seg.approximant (RoseWalker2004.Seg.stop place RoseWalker2004.Series.nasal) = some 3
• RoseWalker2004.nasalSimilarity x✝¹ x✝ = none

def RoseWalker2004.AtLeast (k : Fin 4) (a b : Seg) : Prop

A pair at least as similar as stratum k.

Equations

• RoseWalker2004.AtLeast k a b = match RoseWalker2004.nasalSimilarity a b with | some r => r ≤ k | none => False

@[instance_reducible]

instance RoseWalker2004.instDecidableAtLeast (k : Fin 4) (a b : Seg) : Decidable (AtLeast k a b)

Equations

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

theorem RoseWalker2004.AtLeast.mono {k k' : Fin 4} {a b : Seg} (h : AtLeast k a b) (hk : k ≤ k') : AtLeast k' a b

Candidates and constraints

def RoseWalker2004.consonants (w : List Seg) : List ℕ

The positions of the consonants of a string.

Equations

• RoseWalker2004.consonants w = List.filter (fun (i : ℕ) => decide (w.getD i RoseWalker2004.Seg.vocoid).IsConsonant) (List.range w.length)

def RoseWalker2004.consonantPairs (w : List Seg) : List (ℕ × ℕ)

The pairs of consonant positions of a string, left position first.

Equations

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

structure RoseWalker2004.Cand : Type

An output candidate: the output string, aligned position by position with the input, and the correspondence relation among its consonants as coindexed pairs of positions, each written left position first.

• out : List Seg
• corr : List (ℕ × ℕ)

@[instance_reducible]

instance RoseWalker2004.instDecidableEqCand : DecidableEq Cand

Equations

• RoseWalker2004.instDecidableEqCand = RoseWalker2004.instDecidableEqCand.decEq

def RoseWalker2004.instDecidableEqCand.decEq (x✝ x✝¹ : Cand) : Decidable (x✝ = x✝¹)

Equations

• RoseWalker2004.instDecidableEqCand.decEq { out := a, corr := a_1 } { out := b, corr := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

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

Equations

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

@[instance_reducible]

instance RoseWalker2004.instReprCand : Repr Cand

Equations

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

def RoseWalker2004.Cand.seg (c : Cand) (i : ℕ) : Seg

The segment of a candidate at a position.

Equations

• c.seg i = c.out.getD i RoseWalker2004.Seg.vocoid

def RoseWalker2004.corr (k : Fin 4) : OptimalityTheory.Constraint Cand

CORR at stratum k: a violation for each consonant pair at least as similar as the stratum that does not correspond.

Equations

• RoseWalker2004.corr k c = (List.filter (fun (p : ℕ × ℕ) => decide (RoseWalker2004.AtLeast k (c.seg p.1) (c.seg p.2) ∧ p ∉ c.corr)) (RoseWalker2004.consonantPairs c.out)).length

def RoseWalker2004.identCLCR : OptimalityTheory.Constraint Cand

IDENT-CLCR(nasal): a violation for each coindexed pair whose left member is nasal and whose right member is oral.

Equations

• RoseWalker2004.identCLCR c = (List.filter (fun (p : ℕ × ℕ) => decide ((c.seg p.1).IsNasal ∧ ¬(c.seg p.2).IsNasal)) c.corr).length

def RoseWalker2004.identCRCL : OptimalityTheory.Constraint Cand

IDENT-CRCL(nasal): a violation for each coindexed pair whose right member is nasal and whose left member is oral.

Equations

• RoseWalker2004.identCRCL c = (List.filter (fun (p : ℕ × ℕ) => decide (¬(c.seg p.1).IsNasal ∧ (c.seg p.2).IsNasal)) c.corr).length

def RoseWalker2004.identOI (input : List Seg) : OptimalityTheory.Constraint Cand

IDENT-OI(nasal) for an input: a violation for each segment nasal in the output but not in the input.

Equations

• RoseWalker2004.identOI input c = (List.filter (fun (i : ℕ) => decide (¬(input.getD i RoseWalker2004.Seg.vocoid).IsNasal ∧ (c.seg i).IsNasal)) (List.range input.length)).length

def RoseWalker2004.hierarchy (top : List (OptimalityTheory.Constraint Cand)) (k : Fin 4) (input : List Seg) (bottom : List (OptimalityTheory.Constraint Cand)) : List (OptimalityTheory.Constraint Cand)

The nasal correspondence hierarchy with IDENT-OI(nasal) interpolated below stratum k, under the IDENT-CC constraints top and above bottom.

Equations

• RoseWalker2004.hierarchy top k input bottom = top ++ (List.map RoseWalker2004.corr (List.finRange 4)).insertIdx (↑k + 1) (RoseWalker2004.identOI input) ++ bottom

def RoseWalker2004.ngbaka (input : List Seg) : List (OptimalityTheory.Constraint Cand)

The Ngbaka ranking: both directional IDENT-CC constraints undominated and IDENT-OI(nasal) below the homorganic nasal–prenasal stratum.

Equations

• RoseWalker2004.ngbaka input = RoseWalker2004.hierarchy [RoseWalker2004.identCLCR, RoseWalker2004.identCRCL] 1 input []

def RoseWalker2004.kikongo (input : List Seg) : List (OptimalityTheory.Constraint Cand)

The Kikongo ranking: IDENT-CLCR undominated, IDENT-OI(nasal) below every stratum, and IDENT-CRCL at the bottom.

Equations

• RoseWalker2004.kikongo input = RoseWalker2004.hierarchy [RoseWalker2004.identCLCR] 3 input [RoseWalker2004.identCRCL]

GEN

def RoseWalker2004.outputs : List Seg → List (List Seg)

The outputs for an input: each consonant kept or nasalized.

Equations

• RoseWalker2004.outputs [] = [[]]
• RoseWalker2004.outputs (s :: rest) = List.flatMap (fun (o : List RoseWalker2004.Seg) => (s :: o) :: if s.nasalize = s then [] else [s.nasalize :: o]) (RoseWalker2004.outputs rest)

def RoseWalker2004.partitions : List ℕ → List (List (List ℕ))

The partitions of a list into blocks.

Equations

• One or more equations did not get rendered due to their size.
• RoseWalker2004.partitions [] = [[]]

def RoseWalker2004.corrOf (P : List (List ℕ)) : List (ℕ × ℕ)

The coindexed pairs of a partition, left position first.

Equations

• RoseWalker2004.corrOf P = List.flatMap (fun (b : List ℕ) => List.flatMap (fun (i : ℕ) => List.map (fun (x : ℕ) => (i, x)) (List.filter (fun (x : ℕ) => decide (i < x)) b)) b) P

def RoseWalker2004.gen (input : List Seg) : List Cand

GEN: every output under every coindexation of the consonants.

Equations

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

theorem RoseWalker2004.outputs_ne_nil (w : List Seg) : outputs w ≠ []

theorem RoseWalker2004.partitions_ne_nil (l : List ℕ) : partitions l ≠ []

theorem RoseWalker2004.gen_ne_nil (input : List Seg) : gen input ≠ []

def RoseWalker2004.tableau (ranking : List Seg → List (OptimalityTheory.Constraint Cand)) (input : List Seg) : OptimalityTheory.Tableau Cand (ranking input).length

The tableau of an input under a ranking, over GEN.

Equations

• RoseWalker2004.tableau ranking input = OptimalityTheory.Tableau.ofRanking (RoseWalker2004.gen input) (ranking input) ⋯

The typology of the cut

def RoseWalker2004.pair (a b : Seg) : List Seg

A nasal and a consonant across a vocoid.

Equations

• RoseWalker2004.pair a b = [a, RoseWalker2004.Seg.vocoid, b]

def RoseWalker2004.cut (k : Fin 4) (input : List Seg) : List (OptimalityTheory.Constraint Cand)

Both directional IDENT-CC constraints undominated and IDENT-OI(nasal) below stratum k.

Equations

• RoseWalker2004.cut k input = RoseWalker2004.hierarchy [RoseWalker2004.identCLCR, RoseWalker2004.identCRCL] k input []

theorem RoseWalker2004.winner_eq (k : Fin 4) (p : Place) (b : Seg) (hb : b.IsConsonant) (hn : ¬b.IsNasal) : (tableau (cut k) (pair (Seg.stop p Series.nasal) b)).optimal = {if AtLeast k (Seg.stop p Series.nasal) b then { out := [Seg.stop p Series.nasal, Seg.vocoid, b.nasalize], corr := [(0, 2)] } else { out := pair (Seg.stop p Series.nasal) b, corr := [] }}

The typology: a nasal followed by an oral consonant agrees with it, the two corresponding, exactly when the pair is at least as similar as the cut below which IDENT-OI(nasal) sits; otherwise the input surfaces faithfully with no correspondence.

theorem RoseWalker2004.agree_of_le {k k' : Fin 4} (hk : k ≤ k') (p : Place) (b : Seg) (hb : b.IsConsonant) (hn : ¬b.IsNasal) (h : (tableau (cut k) (pair (Seg.stop p Series.nasal) b)).optimal = {{ out := [Seg.stop p Series.nasal, Seg.vocoid, b.nasalize], corr := [(0, 2)] }}) : (tableau (cut k') (pair (Seg.stop p Series.nasal) b)).optimal = {{ out := [Seg.stop p Series.nasal, Seg.vocoid, b.nasalize], corr := [(0, 2)] }}

Demoting IDENT-OI(nasal) only widens the agreeing class: a pair that agrees at a cut agrees at every lower cut.

The rows

def RoseWalker2004.segment : Char → Option Seg

The segment of a transcription character: nasals m n ŋ, voiced stops b d g, voiceless stops p t k, the approximant l, the fricatives s z f v, and vocoids.

Equations

• RoseWalker2004.segment 'm' = some (RoseWalker2004.Seg.stop RoseWalker2004.Place.labial RoseWalker2004.Series.nasal)
• RoseWalker2004.segment 'n' = some (RoseWalker2004.Seg.stop RoseWalker2004.Place.coronal RoseWalker2004.Series.nasal)
• RoseWalker2004.segment 'ŋ' = some (RoseWalker2004.Seg.stop RoseWalker2004.Place.dorsal RoseWalker2004.Series.nasal)
• RoseWalker2004.segment 'b' = some (RoseWalker2004.Seg.stop RoseWalker2004.Place.labial RoseWalker2004.Series.voiced)
• RoseWalker2004.segment 'd' = some (RoseWalker2004.Seg.stop RoseWalker2004.Place.coronal RoseWalker2004.Series.voiced)
• RoseWalker2004.segment 'g' = some (RoseWalker2004.Seg.stop RoseWalker2004.Place.dorsal RoseWalker2004.Series.voiced)
• RoseWalker2004.segment 'p' = some (RoseWalker2004.Seg.stop RoseWalker2004.Place.labial RoseWalker2004.Series.voiceless)
• RoseWalker2004.segment 't' = some (RoseWalker2004.Seg.stop RoseWalker2004.Place.coronal RoseWalker2004.Series.voiceless)
• RoseWalker2004.segment 'k' = some (RoseWalker2004.Seg.stop RoseWalker2004.Place.dorsal RoseWalker2004.Series.voiceless)
• RoseWalker2004.segment 'l' = some RoseWalker2004.Seg.approximant
• RoseWalker2004.segment 's' = some RoseWalker2004.Seg.fricative
• RoseWalker2004.segment 'z' = some RoseWalker2004.Seg.fricative
• RoseWalker2004.segment 'f' = some RoseWalker2004.Seg.fricative
• RoseWalker2004.segment 'v' = some RoseWalker2004.Seg.fricative
• RoseWalker2004.segment 'a' = some RoseWalker2004.Seg.vocoid
• RoseWalker2004.segment 'e' = some RoseWalker2004.Seg.vocoid
• RoseWalker2004.segment 'i' = some RoseWalker2004.Seg.vocoid
• RoseWalker2004.segment 'o' = some RoseWalker2004.Seg.vocoid
• RoseWalker2004.segment 'u' = some RoseWalker2004.Seg.vocoid
• RoseWalker2004.segment 'ɛ' = some RoseWalker2004.Seg.vocoid
• RoseWalker2004.segment 'ɔ' = some RoseWalker2004.Seg.vocoid
• RoseWalker2004.segment 'w' = some RoseWalker2004.Seg.vocoid
• RoseWalker2004.segment x✝ = none

def RoseWalker2004.parse : List Char → List Seg

The segments of a transcription, prenasal stops written with a superscript nasal and hyphens marking morpheme boundaries.

Equations

• RoseWalker2004.parse ('ᵐ' :: 'b' :: cs) = RoseWalker2004.Seg.stop RoseWalker2004.Place.labial RoseWalker2004.Series.prenasal :: RoseWalker2004.parse cs
• RoseWalker2004.parse ('ⁿ' :: 'd' :: cs) = RoseWalker2004.Seg.stop RoseWalker2004.Place.coronal RoseWalker2004.Series.prenasal :: RoseWalker2004.parse cs
• RoseWalker2004.parse ('ᵑ' :: 'g' :: cs) = RoseWalker2004.Seg.stop RoseWalker2004.Place.dorsal RoseWalker2004.Series.prenasal :: RoseWalker2004.parse cs
• RoseWalker2004.parse (c :: cs) = (RoseWalker2004.segment c).toList ++ RoseWalker2004.parse cs
• RoseWalker2004.parse [] = []

def RoseWalker2004.IsFixedPoint (ranking : List Seg → List (OptimalityTheory.Constraint Cand)) (w : List Seg) : Prop

The words of a language as the fixed points of its grammar: some optimal candidate has the input as its output.

Equations

• RoseWalker2004.IsFixedPoint ranking w = ∃ c ∈ (RoseWalker2004.tableau ranking w).optimal, c.out = w

@[instance_reducible]

instance RoseWalker2004.instDecidableIsFixedPoint (ranking : List Seg → List (OptimalityTheory.Constraint Cand)) (w : List Seg) : Decidable (IsFixedPoint ranking w)

Equations

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

def RoseWalker2004.ngbakaData : List (List Seg × Judgment)

The Ngbaka words of the rows, with their judgments.

Equations

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

theorem RoseWalker2004.ngbaka_tableaux : (tableau ngbaka (parse "naⁿdɛ".toList)).optimal = {{ out := parse "nanɛ".toList, corr := [(0, 2)] }} ∧ (tableau ngbaka (parse "maᵑga".toList)).optimal = {{ out := parse "maᵑga".toList, corr := [] }}

Ngbaka's tableaux: a homorganic nasal and prenasal stop agree, the prenasal nasalized, while a heterorganic pair surfaces faithfully.

theorem RoseWalker2004.ngbaka_rows (d : List Seg × Judgment) : d ∈ ngbakaData → (d.2 = Judgment.acceptable ↔ IsFixedPoint ngbaka d.1)

The morpheme structure constraint: a word of the rows is well formed exactly when it is a fixed point of the Ngbaka grammar.

def RoseWalker2004.kikongoData : List (List Seg × List Seg)

The Kikongo alternations of the rows: the underlying and surface stems.

Equations

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

def RoseWalker2004.Triggers (w : List Seg) (i : ℕ) : Prop

A nasal that triggers agreement: a singleton nasal, not the first half of an NC cluster.

Equations

• RoseWalker2004.Triggers w i = ((w.getD i RoseWalker2004.Seg.vocoid).IsNasal ∧ ¬(w.getD (i + 1) RoseWalker2004.Seg.vocoid).IsConsonant)

@[instance_reducible]

instance RoseWalker2004.instDecidableTriggers (w : List Seg) (i : ℕ) : Decidable (Triggers w i)

Equations

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

def RoseWalker2004.harmonize (w : List Seg) : List Seg

Kikongo's surface map: rightward agreement at the Kikongo cut, a consonant at least as similar as the cut to a preceding trigger nasalized unless it is the second half of an NC cluster.

Equations

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

theorem RoseWalker2004.kikongo_rows (d : List Seg × List Seg) : d ∈ kikongoData → harmonize d.1 = d.2

Every alternation of the rows is the surface map of its underlying stem.

def RoseWalker2004.NoCluster (w : List Seg) : Prop

A stem without NC clusters.

Equations

• RoseWalker2004.NoCluster w = ∀ i < w.length, (w.getD i RoseWalker2004.Seg.vocoid).IsNasal → ¬(w.getD (i + 1) RoseWalker2004.Seg.vocoid).IsConsonant

@[instance_reducible]

instance RoseWalker2004.instDecidableNoCluster (w : List Seg) : Decidable (NoCluster w)

Equations

• RoseWalker2004.instDecidableNoCluster w = RoseWalker2004.instDecidableNoCluster._aux_1 w

theorem RoseWalker2004.kikongo_grammar (d : List Seg × List Seg) : d ∈ kikongoData → (consonants d.1).length ≤ 4 → NoCluster d.1 → ∃ c ∈ (tableau kikongo d.1).optimal, c.out = harmonize d.1

The grammar agrees with the map: for the stems without NC clusters and with at most four consonants, some optimal candidate of the Kikongo ranking has the map's output.

theorem RoseWalker2004.tumidi : (tableau kikongo (parse "tum-idi".toList)).optimal = {{ out := parse "tum-ini".toList, corr := [(2, 4)] }}

tum-idi: the suffix consonant nasalizes and corresponds with the nasal.

theorem RoseWalker2004.nikulu : (tableau kikongo (parse "nik-ulu".toList)).optimal = {{ out := parse "nik-unu".toList, corr := [(0, 4)] }}

nik-ulu: the voiceless stop is neutral, agreeing with nothing and corresponding with nothing, while the approximant nasalizes.

def RoseWalker2004.kudumukila : List Cand

The paper's candidates for kudumuk-ila: the voiced stop, nasal, and suffix consonant coindexed with only the suffix nasalized; both nasalized; the stop nasalized and coindexed with the nasal alone; the nasal and suffix coindexed; the stop and suffix coindexed; and all three coindexed with nothing nasalized.

Equations

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

theorem RoseWalker2004.kudumukila_winner : (OptimalityTheory.Tableau.ofRanking kudumukila (kikongo (parse "kudumuk-ila".toList)) kudumukila_winner._proof_1).optimal = {kudumukila[0]}

The direction of agreement: with IDENT-CLCR above IDENT-OI(nasal) and IDENT-CRCL below it, the suffix consonant to the right of the nasal nasalizes and the voiced stop to its left stays oral.