Transderivational identity: [benua-1997]

[benua-1997] proposes that morphologically related words are held identical by ranked, violable constraints on an output–output (OO) correspondence relation between two surface words, each also tied to its own input by IO-faithfulness (the subparadigm (11)). Misapplication — overapplication, OO-Identity, M >> IO-Faith (21); underapplication, OO-Identity >> M >> IO-Faith (28); and its restriction TETRU, M₁ >> OO-Identity >> M₂ >> IO-Faith (35) — falls out of ranking, with no cyclic derivation. What lets a dominated constraint compel violation of a dominant one is recursive evaluation (§2.3.1): the hierarchy is duplicated, the base's recursion dominating the derived word's, so misapplication in the base is always fatal (the priority of the base) and a paradigm competes by the base's violation profile first and the derived word's second. recursive states this over the substrate's Correspondence, Constraint and Tableau; nonrecursive is the summed evaluation the paper shows going wrong in (57), (88) and (119).

The paper's tableaux then run as stated: the English diminutive paradigm Larry ~ Lar ((16), (29)); Sundanese nasal harmony from any rich input (47), its overapplication in infixed plurals (52), its normal application under a nasal affix (55) and the base that must not overapply (56) versus (57); Tiberian Hebrew jussive truncation with epenthesis underapplying (87) versus (88), TETRU forcing it in rising-sonority clusters (92) and the emergent markedness relation SON-CON ⊆ *COMPLEX-CODA, spirantization underapplying in 2fs truncation (118) versus (119), and the imperative's normal application (135) — the two truncations under the single ranking (137), distinguished only by which OO relation their morphology invokes (§4.6.3). Out of scope: English affix classes (Ch. 5), the guttural CODACOND (§4.3.3), opacity (§4.4.3), and the serial alternatives (§3.5, §4.7), which the paper rejects as over-generating rather than reconstructs.

Subparadigms and recursive evaluation

inductive Benua1997.Role : Type

The four positions of a subparadigm (11): each word with its own input.

• baseInput : Role
• base : Role
• derivInput : Role
• derivative : Role

@[instance_reducible]

instance Benua1997.instDecidableEqRole : DecidableEq Role

Equations

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

@[instance_reducible]

instance Benua1997.instReprRole : Repr Role

Equations

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

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

Equations

• Benua1997.instReprRole.repr Benua1997.Role.baseInput prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Role.baseInput")).group prec✝
• Benua1997.instReprRole.repr Benua1997.Role.base prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Role.base")).group prec✝
• Benua1997.instReprRole.repr Benua1997.Role.derivInput prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Role.derivInput")).group prec✝
• Benua1997.instReprRole.repr Benua1997.Role.derivative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Role.derivative")).group prec✝

def Benua1997.paradigm {α : Type u_1} (bIn b dIn d : List α) (ioB ioD oo : List (ℕ × ℕ)) : OptimalityTheory.Correspondence Role α

A subparadigm: the base and the derived word with their inputs, and the three correspondence relations of (11) — each word's IO relation and the OO relation.

Equations

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

structure Benua1997.ParadigmConstraint (α : Type u_3) : Type u_3

A constraint of the hierarchy read at each word of the subparadigm: a markedness constraint on the word's output, IO-Faith on its IO relation, OO-Identity on the OO relation and vacuous at the base, which bears none (§2.3.1).

• atBase : OptimalityTheory.Correspondence Role α → ℕ
• atDerived : OptimalityTheory.Correspondence Role α → ℕ

def Benua1997.markedness {α : Type u_1} {ρ : Type u_2} (m : List α → ℕ) : ρ → ParadigmConstraint α

A markedness constraint, read off each output.

Equations

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

def Benua1997.ioFaith {α : Type u_1} {ρ : Type u_2} (f : OptimalityTheory.Correspondence Role α → Role → Role → ℕ) : ρ → ParadigmConstraint α

An IO-Faith constraint, read off each word's IO relation.

Equations

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

def Benua1997.ooIdentity {α : Type u_1} {ρ : Type u_2} [DecidableEq ρ] (rel : ρ) (f : OptimalityTheory.Correspondence Role α → Role → Role → ℕ) : ρ → ParadigmConstraint α

The OO-Identity constraint proper to the relation rel: read off the OO relation of a paradigm bearing rel, vacuous on paradigms bearing another (§4.6.3) and at the base.

Equations

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

def Benua1997.recursive {α : Type u_1} {ρ : Type u_2} (ranking : List (ρ → ParadigmConstraint α)) (r : ρ) : List (Constraints.Constraint (OptimalityTheory.Correspondence Role α))

Recursive evaluation (§2.3.1): the ranking is duplicated and the recursions ranked, the base's above the derived word's, for paradigms bearing relation r.

Equations

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

def Benua1997.nonrecursive {α : Type u_1} {ρ : Type u_2} (ranking : List (ρ → ParadigmConstraint α)) (r : ρ) : List (Constraints.Constraint (OptimalityTheory.Correspondence Role α))

Non-recursive evaluation, each constraint's violations tallied over both words — the evaluation of (57), (88), (119).

Equations

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

def Benua1997.tableau {α : Type u_1} {ρ : Type u_2} {L : Type u_3} [DecidableEq L] (cand : L → OptimalityTheory.Correspondence Role α) (labels : List L) (eval : List (ρ → ParadigmConstraint α) → ρ → List (Constraints.Constraint (OptimalityTheory.Correspondence Role α))) (ranking : List (ρ → ParadigmConstraint α)) (r : ρ) (h : labels ≠ [] := by decide) : OptimalityTheory.Tableau L (List.map (Constraints.Constraint.comap cand) (eval ranking r)).length

The tableau of the labelled candidate paradigms cand under eval — recursive or nonrecursive — for paradigms bearing r.

Equations

• Benua1997.tableau cand labels eval ranking r h = OptimalityTheory.Tableau.ofRanking labels (List.map (Constraints.Constraint.comap cand) (eval ranking r)) h

inductive Benua1997.Cand4 : Type

The candidate paradigms of a four-way tableau.

• a : Cand4
• b : Cand4
• c : Cand4
• d : Cand4

@[instance_reducible]

instance Benua1997.instDecidableEqCand4 : DecidableEq Cand4

Equations

• Benua1997.instDecidableEqCand4 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Benua1997.instReprCand4 : Repr Cand4

Equations

• Benua1997.instReprCand4 = { reprPrec := Benua1997.instReprCand4.repr }

def Benua1997.instReprCand4.repr : Cand4 → ℕ → Std.Format

Equations

• Benua1997.instReprCand4.repr Benua1997.Cand4.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Cand4.a")).group prec✝
• Benua1997.instReprCand4.repr Benua1997.Cand4.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Cand4.b")).group prec✝
• Benua1997.instReprCand4.repr Benua1997.Cand4.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Cand4.c")).group prec✝
• Benua1997.instReprCand4.repr Benua1997.Cand4.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Cand4.d")).group prec✝

inductive Benua1997.Cand3 : Type

The candidate paradigms of a three-way tableau.

• a : Cand3
• b : Cand3
• c : Cand3

@[instance_reducible]

instance Benua1997.instDecidableEqCand3 : DecidableEq Cand3

Equations

• Benua1997.instDecidableEqCand3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Benua1997.instReprCand3 : Repr Cand3

Equations

• Benua1997.instReprCand3 = { reprPrec := Benua1997.instReprCand3.repr }

def Benua1997.instReprCand3.repr : Cand3 → ℕ → Std.Format

Equations

• Benua1997.instReprCand3.repr Benua1997.Cand3.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Cand3.a")).group prec✝
• Benua1997.instReprCand3.repr Benua1997.Cand3.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Cand3.b")).group prec✝
• Benua1997.instReprCand3.repr Benua1997.Cand3.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.Cand3.c")).group prec✝

English diminutive truncation (§2.3.1)

L[æ]rry ~ L[æ]r: the a/æ neutralisation before tautosyllabic r underapplies in the diminutive, under OO-IDENT[BK] >> *ær]σ >> IO-IDENT[BK] (15).

inductive Benua1997.English.Seg : Type

The segments of Larry.

• l : Seg
• r : Seg
• i : Seg
• a : Seg
• ae : Seg

@[instance_reducible]

instance Benua1997.English.instDecidableEqSeg : DecidableEq Seg

Equations

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

def Benua1997.English.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

• Benua1997.English.instReprSeg.repr Benua1997.English.Seg.l prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.English.Seg.l")).group prec✝
• Benua1997.English.instReprSeg.repr Benua1997.English.Seg.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.English.Seg.r")).group prec✝
• Benua1997.English.instReprSeg.repr Benua1997.English.Seg.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.English.Seg.i")).group prec✝
• Benua1997.English.instReprSeg.repr Benua1997.English.Seg.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.English.Seg.a")).group prec✝
• Benua1997.English.instReprSeg.repr Benua1997.English.Seg.ae prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benua1997.English.Seg.ae")).group prec✝

@[instance_reducible]

instance Benua1997.English.instReprSeg : Repr Seg

Equations

• Benua1997.English.instReprSeg = { reprPrec := Benua1997.English.instReprSeg.repr }

def Benua1997.English.back : Seg → Option Bool

Backness of the low vowels.

Equations

• Benua1997.English.back Benua1997.English.Seg.a = some true
• Benua1997.English.back Benua1997.English.Seg.ae = some false
• Benua1997.English.back x✝ = none

def Benua1997.English.aerSigma : List Seg → ℕ

*ær]σ: a front low vowel before a syllable-closing r.

Equations

• One or more equations did not get rendered due to their size.
• Benua1997.English.aerSigma (head :: rest) = Benua1997.English.aerSigma rest
• Benua1997.English.aerSigma [] = 0

def Benua1997.English.ranking : List (Unit → ParadigmConstraint Seg)

(15): OO-IDENT[BK] >> *ær]σ >> IO-IDENT[BK].

Equations

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

def Benua1997.English.cand : Cand4 → OptimalityTheory.Correspondence Role Seg

The paradigms of (16): base L[a]rry or L[æ]rry with diminutive L[a]r or L[æ]r, from the inputs /læri/ and /læri + TRUNC/.

Equations

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

theorem Benua1997.English.underapplication : (tableau cand [Cand4.a, Cand4.b, Cand4.c, Cand4.d] recursive ranking () ⋯).optimal = {Cand4.d}

(16), (29): under recursive evaluation the underapplication paradigm L[æ]rry ~ L[æ]r wins — overapplication in the base costs an IO-IDENT violation in the dominant recursion.

theorem Benua1997.English.overapplication_nonrecursive : (tableau cand [Cand4.a, Cand4.b, Cand4.c, Cand4.d] nonrecursive ranking () ⋯).optimal = {Cand4.a}

Without recursion, overapplication in the base L[a]rry ~ L[a]r wins: it satisfies OO-Identity and *ær]σ at the cost of low-ranked IO-Faith only.

Sundanese nasal harmony (Ch. 3)

Nasality is allophonic — nasal after a nasal segment, oral elsewhere — by *NVORAL >> *VNAS >> IO-IDENT[NAS] (48); it overapplies in the infixed plural ɲĩãr ~ ɲ-ãl-ĩãr and applies normally in dəhəs ~ d-um-ə̃hə̃s under the single ranking *NVORAL >> OO-IDENT[NAS] >> *VNAS >> IO-IDENT[NAS] (58); data from [cohn-1990].

inductive Benua1997.Sundanese.Seg : Type

Sundanese segments by the features the constraints read: laryngeals are transparent to nasal spread.

• nasalC : Seg
• oralC : Seg
• laryngeal : Seg
• oralV : Seg
• nasalV : Seg

@[instance_reducible]

instance Benua1997.Sundanese.instDecidableEqSeg : DecidableEq Seg

Equations

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

def Benua1997.Sundanese.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Benua1997.Sundanese.instReprSeg : Repr Seg

Equations

• Benua1997.Sundanese.instReprSeg = { reprPrec := Benua1997.Sundanese.instReprSeg.repr }

def Benua1997.Sundanese.nasal : Seg → Bool

Nasality.

Equations

• Benua1997.Sundanese.nasal Benua1997.Sundanese.Seg.nasalC = true
• Benua1997.Sundanese.nasal Benua1997.Sundanese.Seg.nasalV = true
• Benua1997.Sundanese.nasal x✝ = false

def Benua1997.Sundanese.nvOral : List Seg → ℕ

*NVORAL (45): an oral vowel in post-nasal context, laryngeals skipped.

Equations

• Benua1997.Sundanese.nvOral = Benua1997.Sundanese.nvOral.go false

def Benua1997.Sundanese.nvOral.go (postNasal : Bool) : List Seg → ℕ

postNasal records whether the last non-laryngeal segment was nasal.

Equations

• Benua1997.Sundanese.nvOral.go postNasal [] = 0
• Benua1997.Sundanese.nvOral.go postNasal (Benua1997.Sundanese.Seg.oralV :: rest) = (if postNasal = true then 1 else 0) + Benua1997.Sundanese.nvOral.go false rest
• Benua1997.Sundanese.nvOral.go postNasal (Benua1997.Sundanese.Seg.laryngeal :: rest) = Benua1997.Sundanese.nvOral.go postNasal rest
• Benua1997.Sundanese.nvOral.go postNasal (s :: rest) = Benua1997.Sundanese.nvOral.go (Benua1997.Sundanese.nasal s) rest

def Benua1997.Sundanese.vNas (w : List Seg) : ℕ

*VNAS (44): a nasal vowel.

Equations

• Benua1997.Sundanese.vNas w = List.count Benua1997.Sundanese.Seg.nasalV w

def Benua1997.Sundanese.ranking : List (Unit → ParadigmConstraint Seg)

(58): *NVORAL >> OO-IDENT[NAS] >> *VNAS >> IO-IDENT[NAS].

Equations

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

def Benua1997.Sundanese.inputs : List (List Seg)

(47): the four rich inputs for ŋãtur 'arrange' and the candidates ŋatur, ŋatũr, ŋãtũr, ŋãtur.

Equations

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

def Benua1997.Sundanese.word : Cand4 → List Seg

The output candidates of (47), by their vowels.

Equations

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

theorem Benua1997.Sundanese.allophony (input : List Seg) : input ∈ inputs → (OptimalityTheory.Tableau.ofRanking [Cand4.a, Cand4.b, Cand4.c, Cand4.d] [Constraints.Constraint.comap word nvOral, Constraints.Constraint.comap word vNas, fun (w : Cand4) => OptimalityTheory.Correspondence.identViolFeature nasal (OptimalityTheory.Correspondence.parallel input (word w)) OptimalityTheory.Correspondence.Side.lhs OptimalityTheory.Correspondence.Side.rhs] ⋯).optimal = {Cand4.d}

(47): whatever the input's vowels, *NVORAL >> *VNAS >> IO-IDENT[NAS] selects ŋãtur — allophony is decided by markedness over the rich input.

def Benua1997.Sundanese.infixIO : List (ℕ × ℕ)

The correspondence of the plural's input /ãl + ɲĩãr/ with its infixed output ɲ-ãl-ĩãr: the affix's segments land after the root-initial nasal.

Equations

• Benua1997.Sundanese.infixIO = [(0, 1), (1, 2), (2, 0), (3, 3), (4, 4), (5, 5)]

def Benua1997.Sundanese.infixOO : List (ℕ × ℕ)

The OO correspondence of ɲĩãr with ɲ-ãl-ĩãr: the root around the infix.

Equations

• Benua1997.Sundanese.infixOO = [(0, 0), (1, 3), (2, 4), (3, 5)]

def Benua1997.Sundanese.plural : Cand4 → OptimalityTheory.Correspondence Role Seg

The paradigms of (52): base ɲiar or ɲĩãr, plural ɲ-ãl-iar or ɲ-ãl-ĩãr, from the inputs /ɲĩãr/ and /ãl + ɲĩãr/.

Equations

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

theorem Benua1997.Sundanese.overapplication : (tableau plural [Cand4.a, Cand4.b, Cand4.c, Cand4.d] recursive ranking () ⋯).optimal = {Cand4.d}

(52): nasal spread overapplies in the plural — ɲĩãr ~ ɲ-ãl-ĩãr wins, the root vowels nasal in oral context to match the base.

def Benua1997.Sundanese.umOO : List (ℕ × ℕ)

The OO correspondence of dəhəs with d-um-əhəs.

Equations

• Benua1997.Sundanese.umOO = [(0, 0), (1, 3), (2, 4), (3, 5), (4, 6)]

def Benua1997.Sundanese.umIO : List (ℕ × ℕ)

The correspondence of /ũm + dəhəs/ with d-um-əhəs.

Equations

• Benua1997.Sundanese.umIO = [(0, 1), (1, 2), (2, 0), (3, 3), (4, 4), (5, 5), (6, 6)]

def Benua1997.Sundanese.approach : Cand4 → OptimalityTheory.Correspondence Role Seg

The paradigms of (55), all on the canonical base dəhəs: the infixed word's vowels oral or nasal in the infix and in the root.

Equations

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

def Benua1997.Sundanese.approach.base : List Seg

Equations

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

def Benua1997.Sundanese.approach.input : List Seg

Equations

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

theorem Benua1997.Sundanese.normalApplication : (tableau approach [Cand4.a, Cand4.b, Cand4.c, Cand4.d] recursive ranking () ⋯).optimal = {Cand4.c}

(55): under a nasal affix harmony applies normally — dəhəs ~ d-um-ə̃hə̃s — OO-Identity giving way to *NVORAL, and *VNAS keeping the infix vowel oral.

def Benua1997.Sundanese.baseChoice : Cand3 → OptimalityTheory.Correspondence Role Seg

(56)/(57): the base də̃hə̃s that would overapply to restore identity against the canonical dəhəs.

Equations

• One or more equations did not get rendered due to their size.
• Benua1997.Sundanese.baseChoice x✝ = Benua1997.Sundanese.approach Benua1997.Cand4.c

theorem Benua1997.Sundanese.base_priority : (tableau baseChoice [Cand3.a, Cand3.b] recursive ranking () ⋯).optimal = {Cand3.b}

(56): the base cannot misapply — its *VNAS marks fall in the dominant recursion.

theorem Benua1997.Sundanese.base_overapplies_nonrecursive : (tableau baseChoice [Cand3.a, Cand3.b] nonrecursive ranking () ⋯).optimal = {Cand3.a}

(57): the non-recursive tally wrongly prefers the overapplying base, which satisfies *NVORAL and OO-Identity outright.

Tiberian Hebrew truncation (Ch. 4)

Jussive/2fs truncation invokes one OO relation, imperative truncation another (§4.6.3). Epenthesis, driven by *COMPLEX-CODA >> IO-DEP (85), underapplies in jussives under OOJ-DEP >> *COMPLEX-CODA (89) except into rising-sonority clusters, SON-CON >> OOJ-DEP (93); post-vocalic spirantization, driven by *V-STOP >> *SPIR >> IO-IDENT[CONT] (115), underapplies in 2fs stems and applies normally in imperatives, OOJ-ID[CONT] >> *V-STOP >> *SPIR >> OOI-ID[CONT], IO-ID[CONT] (137).

inductive Benua1997.Hebrew.Relation : Type

The two OO relations of the grammar: jussive/2fs truncation and imperative truncation.

• jussive : Relation
• imperative : Relation

@[instance_reducible]

instance Benua1997.Hebrew.instDecidableEqRelation : DecidableEq Relation

Equations

• Benua1997.Hebrew.instDecidableEqRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Benua1997.Hebrew.instReprRelation.repr : Relation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Benua1997.Hebrew.instReprRelation : Repr Relation

Equations

• Benua1997.Hebrew.instReprRelation = { reprPrec := Benua1997.Hebrew.instReprRelation.repr }

inductive Benua1997.Hebrew.Seg : Type

Segments by the classes the constraints read: the sonority scale of fn. 64 and the stop/spirant contrast.

• vowel : Seg
• glide : Seg
• guttural : Seg
• liquid : Seg
• nasal : Seg
• sibilant : Seg
• spirant : Seg
• stop : Seg

@[instance_reducible]

instance Benua1997.Hebrew.instDecidableEqSeg : DecidableEq Seg

Equations

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

def Benua1997.Hebrew.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Benua1997.Hebrew.instReprSeg : Repr Seg

Equations

• Benua1997.Hebrew.instReprSeg = { reprPrec := Benua1997.Hebrew.instReprSeg.repr }

def Benua1997.Hebrew.sonority : Seg → ℕ

Sonority (fn. 64): vowel > glide > liquid > nasal > fricative > stop.

Equations

• Benua1997.Hebrew.sonority Benua1997.Hebrew.Seg.vowel = 6
• Benua1997.Hebrew.sonority Benua1997.Hebrew.Seg.glide = 5
• Benua1997.Hebrew.sonority Benua1997.Hebrew.Seg.guttural = 5
• Benua1997.Hebrew.sonority Benua1997.Hebrew.Seg.liquid = 4
• Benua1997.Hebrew.sonority Benua1997.Hebrew.Seg.nasal = 3
• Benua1997.Hebrew.sonority Benua1997.Hebrew.Seg.sibilant = 2
• Benua1997.Hebrew.sonority Benua1997.Hebrew.Seg.spirant = 2
• Benua1997.Hebrew.sonority Benua1997.Hebrew.Seg.stop = 1

def Benua1997.Hebrew.continuant : Seg → Option Bool

[±continuant] on the alternating obstruents.

Equations

• Benua1997.Hebrew.continuant Benua1997.Hebrew.Seg.stop = some false
• Benua1997.Hebrew.continuant Benua1997.Hebrew.Seg.spirant = some true
• Benua1997.Hebrew.continuant x✝ = none

def Benua1997.Hebrew.finalCluster : List Seg → Option (Seg × Seg)

The word-final consonant cluster, if any: a complex coda.

Equations

• Benua1997.Hebrew.finalCluster [] = none
• Benua1997.Hebrew.finalCluster [head] = none
• Benua1997.Hebrew.finalCluster [x_1, y] = if x_1 ≠ Benua1997.Hebrew.Seg.vowel ∧ y ≠ Benua1997.Hebrew.Seg.vowel then some (x_1, y) else none
• Benua1997.Hebrew.finalCluster (head :: rest) = Benua1997.Hebrew.finalCluster rest

def Benua1997.Hebrew.complexCoda (w : List Seg) : ℕ

*COMPLEX-CODA (84).

Equations

• Benua1997.Hebrew.complexCoda w = if (Benua1997.Hebrew.finalCluster w).isSome = true then 1 else 0

def Benua1997.Hebrew.sonCon (w : List Seg) : ℕ

SON-CON (91): a coda that rises in sonority.

Equations

• Benua1997.Hebrew.sonCon w = match Benua1997.Hebrew.finalCluster w with | some (x, y) => if Benua1997.Hebrew.sonority x < Benua1997.Hebrew.sonority y then 1 else 0 | none => 0

theorem Benua1997.Hebrew.sonCon_le_complexCoda (w : List Seg) : sonCon w ≤ complexCoda w

The markedness relation TETRU makes emerge (§4.3.2): SON-CON marks a subset of the codas *COMPLEX-CODA marks.

def Benua1997.Hebrew.vStop : List Seg → ℕ

*V-STOP (112): a post-vocalic stop.

Equations

• Benua1997.Hebrew.vStop (Benua1997.Hebrew.Seg.vowel :: Benua1997.Hebrew.Seg.stop :: rest) = 1 + Benua1997.Hebrew.vStop (Benua1997.Hebrew.Seg.stop :: rest)
• Benua1997.Hebrew.vStop (head :: rest) = Benua1997.Hebrew.vStop rest
• Benua1997.Hebrew.vStop [] = 0

def Benua1997.Hebrew.spir (w : List Seg) : ℕ

*SPIR (111).

Equations

• Benua1997.Hebrew.spir w = List.count Benua1997.Hebrew.Seg.spirant w

def Benua1997.Hebrew.epenthesis : List (Relation → ParadigmConstraint Seg)

The epenthesis hierarchy of (93): SON-CON >> OOJ-DEP >> *COMPLEX-CODA >> IO-DEP.

Equations

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

def Benua1997.Hebrew.spirantization : List (Relation → ParadigmConstraint Seg)

The spirantization hierarchy of (137).

Equations

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

def Benua1997.Hebrew.captive : Cand4 → OptimalityTheory.Correspondence Role Seg

The jussive paradigms of (87), from /ya-šbē/ and /ya-šbē-TRUNC/: the base yi.šə.bē or yiš.bē, the jussive yi.šeb or yišb.

Equations

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

def Benua1997.Hebrew.captive.input : List Seg

Equations

• Benua1997.Hebrew.captive.input = [Benua1997.Hebrew.Seg.glide, Benua1997.Hebrew.Seg.vowel, Benua1997.Hebrew.Seg.sibilant, Benua1997.Hebrew.Seg.stop, Benua1997.Hebrew.Seg.vowel]

def Benua1997.Hebrew.captive.epenthetic : List (ℕ × ℕ)

An IO correspondence with a vowel epenthesized after the third segment.

Equations

• Benua1997.Hebrew.captive.epenthetic = [(0, 0), (1, 1), (2, 2), (3, 4), (4, 5)]

theorem Benua1997.Hebrew.epenthesis_underapplies : (tableau captive [Cand4.a, Cand4.b, Cand4.c, Cand4.d] recursive epenthesis Relation.jussive ⋯).optimal = {Cand4.d}

(87): epenthesis underapplies in yiš.bē ~ yišb 'take captive' — the complex coda is kept to give every jussive segment a base correspondent.

theorem Benua1997.Hebrew.epenthesis_overapplies_nonrecursive : (tableau captive [Cand4.a, Cand4.b, Cand4.c, Cand4.d] nonrecursive epenthesis Relation.jussive ⋯).optimal = {Cand4.a}

(88): the non-recursive tally prefers epenthesis overapplying in the base, yi.šə.bē ~ yi.šeb.

def Benua1997.Hebrew.uncover : Cand3 → OptimalityTheory.Correspondence Role Seg

The paradigms of (92), from /ya-glē/: base yi.ɣə.lē or yiɣ.lē, jussive yi.ɣel or yiɣl.

Equations

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

def Benua1997.Hebrew.uncover.input : List Seg

Equations

• Benua1997.Hebrew.uncover.input = [Benua1997.Hebrew.Seg.glide, Benua1997.Hebrew.Seg.vowel, Benua1997.Hebrew.Seg.spirant, Benua1997.Hebrew.Seg.liquid, Benua1997.Hebrew.Seg.vowel]

theorem Benua1997.Hebrew.tetru : (tableau uncover [Cand3.a, Cand3.b, Cand3.c] recursive epenthesis Relation.jussive ⋯).optimal = {Cand3.b}

(92), TETRU: into a rising-sonority cluster epenthesis applies normally — yiɣ.lē ~ yi.ɣel 'uncover' — SON-CON outranking OOJ-DEP, while the overapplying base loses in the dominant recursion.

def Benua1997.Hebrew.heard : Cand3 → OptimalityTheory.Correspondence Role Seg

The 2fs paradigms of (118), from /šamaʕ-tī/ and its truncation: the base's coronal a stop or a spirant, the 2fs stem's a stop or a spirant after the epenthetic vowel.

Equations

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

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

šāmaʕ followed by two segments.

Equations

• Benua1997.Hebrew.heard.stem x y = [Benua1997.Hebrew.Seg.sibilant, Benua1997.Hebrew.Seg.vowel, Benua1997.Hebrew.Seg.nasal, Benua1997.Hebrew.Seg.vowel, Benua1997.Hebrew.Seg.guttural, x, y]

def Benua1997.Hebrew.heard.input : List Seg

Equations

• Benua1997.Hebrew.heard.input = Benua1997.Hebrew.heard.stem Benua1997.Hebrew.Seg.stop Benua1997.Hebrew.Seg.vowel

def Benua1997.Hebrew.heard.truncated : List (ℕ × ℕ)

The correspondence of šāmaʕtī with šāmaʕat: the final vowel truncated, a vowel epenthesized before the stop.

Equations

• Benua1997.Hebrew.heard.truncated = [(0, 0), (1, 1), (2, 2), (3, 3), (4, 4), (5, 6)]

theorem Benua1997.Hebrew.spirantization_underapplies : (tableau heard [Cand3.a, Cand3.b, Cand3.c] recursive spirantization Relation.jussive ⋯).optimal = {Cand3.c}

(118): spirantization underapplies in šāmaʕtī ~ šāmaʕat 'I/you (fs) heard' — the post-vocalic stop matches the base's.

theorem Benua1997.Hebrew.spirantization_overapplies_nonrecursive : (tableau heard [Cand3.a, Cand3.b, Cand3.c] nonrecursive spirantization Relation.jussive ⋯).optimal = {Cand3.a}

(119): the non-recursive tally prefers spirantization overapplying in the base.

def Benua1997.Hebrew.write : Cand3 → OptimalityTheory.Correspondence Role Seg

The imperative paradigms of (135), from /ya-ktōb/: base yikθōβ or yixtōβ, imperative kəθōβ or xətōβ.

Equations

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

def Benua1997.Hebrew.write.input : List Seg

Equations

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

def Benua1997.Hebrew.write.imperativeIO : List (ℕ × ℕ)

The imperative keeps the root; its second vowel is epenthetic.

Equations

• Benua1997.Hebrew.write.imperativeIO = [(2, 0), (3, 2), (4, 3), (5, 4)]

def Benua1997.Hebrew.write.imperativeOO : List (ℕ × ℕ)

Equations

• Benua1997.Hebrew.write.imperativeOO = [(2, 0), (3, 2), (4, 3), (5, 4)]

theorem Benua1997.Hebrew.imperative_normalApplication : (tableau write [Cand3.a, Cand3.b, Cand3.c] recursive spirantization Relation.imperative ⋯).optimal = {Cand3.c}

(135): in the imperative yixtōβ ~ kəθōβ 'write' spirantization applies normally — the same ranking (137), the imperative's OO-Identity ranked below the spirantization constraints.