Steriade (1997): Lexical Conservatism

This file formalizes Steriade's lexical conservatism, a family of grammatical conditions against phonologically novel forms: a property of the allomorph under evaluation must have a precedent in some listed allomorph of the same morpheme. The Lex(P) conditions (lexP) require a precedent for a phonological property, and the Lex(P, M) conditions (lexPM) require the target to share a property with a listed allomorph bearing a morphosyntactic feature the target must encode; unlike the correspondence conditions of McCarthy and Prince, both search the whole paradigm rather than compare with one base, and the morphosyntactic base is only the listed allomorph carrying the required features (IsBase). Listed allomorphs are conservative by construction (lexP_of_mem), and with a single listed allomorph every precedent is that base (lexP_singleton), one of the sources of the appearance of single-base derivation.

The split-base effect arises when a phonological property is desirable in a novel form but absent from the morphosyntactic base and present in another listed allomorph: the novel form adopts the property from the second allomorph and a property identifying the base from the first, and satisfies the precedent condition, the phonological constraint and the base-identity condition at once, whereas each listed allomorph violates one of them (split_base). The forms compete under the ranking schema in which the precedent condition and the phonological constraint outrank the base-identity condition (split_wins_of_phono_over_lexPM), and the base-faithful form wins under the reverse ranking (base_wins_of_lexPM_over_phono). The French masculine liaison allomorph of vain, the masculine vowel with the feminine consonant, is the split-base form for speakers who rank identity of the accented vowel to the masculine above identity of the whole rime to a listed allomorph; the feminine form wins for the others (vain_split, vain_feminine). The English -able adjective on remedy adopts the stress of remedial to avoid a lapse for speakers who rank the lapse constraint above stress identity to the verbal allomorph, and keeps the verb's stress for the others, while parody, with no listed amphibrachic allomorph, admits only the lapsed form (remediable, parodiable).

Implementation notes

The listed allomorphs are treated as categorical, as the paper does, and only the properties the analysed conditions mention are represented. A French adjective form is its string of segments and its gender, from which its accented vowel, its final consonant, its rime and its hiatus with the following noun are read, and an English stem allomorph is its stress pattern and its lexical category. The paper's survey of -able forms, in which the accentually heterogeneous paradigms take the stress of the non-verbal allomorph in most responses and the homogeneous ones keep the verb's stress, and its corpus of 186 forms, are described and not reproduced. The lapse constraint is the paper's three-stressless-syllable version.

References

• [Ste97]
• [McCP95]
• [Pri83]

Lexical conservatism conditions

def Steriade1997.lexP {Form : Type u_1} (L : List Form) (P : Form → Prop) [DecidablePred P] : OptimalityTheory.Constraint Form

Lex(P), the paper's (7), lets the target allomorph have the property P only if some listed allomorph of the morpheme has it.

Equations

• Steriade1997.lexP L P = OptimalityTheory.Constraint.binary fun (t : Form) => P t ∧ ∀ l ∈ L, ¬P l

def Steriade1997.lexPM {Form : Type u_1} (L : List Form) (P M : Form → Prop) [DecidablePred P] [DecidablePred M] : OptimalityTheory.Constraint Form

Lex(P, M), the paper's (9), requires the target to have the property P if some listed allomorph has P and the morphosyntactic feature M the target must encode.

Equations

• Steriade1997.lexPM L P M = OptimalityTheory.Constraint.binary fun (t : Form) => (∃ l ∈ L, P l ∧ M l) ∧ ¬P t

def Steriade1997.wellFormed {Form : Type u_1} (P : Form → Prop) [DecidablePred P] : OptimalityTheory.Constraint Form

A phonological well-formedness constraint demanding the property P.

Equations

• Steriade1997.wellFormed P = OptimalityTheory.Constraint.binary fun (t : Form) => ¬P t

def Steriade1997.IsBase {Form : Type u_1} (L : List Form) (M : Form → Prop) (b : Form) : Prop

The morphosyntactically appropriate base, the paper's (12), is a listed allomorph with the required features.

Equations

• Steriade1997.IsBase L M b = (b ∈ L ∧ M b)

theorem Steriade1997.lexP_eq_zero_iff {Form : Type u_1} (L : List Form) (P : Form → Prop) [DecidablePred P] (t : Form) : lexP L P t = 0 ↔ P t → ∃ l ∈ L, P l

theorem Steriade1997.lexPM_eq_zero_iff {Form : Type u_1} (L : List Form) (P M : Form → Prop) [DecidablePred P] [DecidablePred M] (t : Form) : lexPM L P M t = 0 ↔ (∃ l ∈ L, P l ∧ M l) → P t

theorem Steriade1997.wellFormed_eq_zero_iff {Form : Type u_1} (P : Form → Prop) [DecidablePred P] (t : Form) : wellFormed P t = 0 ↔ P t

theorem Steriade1997.lexP_of_mem {Form : Type u_1} (L : List Form) (P : Form → Prop) [DecidablePred P] {t : Form} (h : t ∈ L) : lexP L P t = 0

A listed allomorph never violates a Lex(P) condition.

theorem Steriade1997.lexP_singleton {Form : Type u_1} (P : Form → Prop) [DecidablePred P] (b t : Form) : lexP [b] P t = 0 ↔ P t → P b

With a single listed allomorph, a precedent is identity to that allomorph, which gives the appearance of single-base derivation from an impoverished paradigm.

The split-base effect

def Steriade1997.con30 {Form : Type u_1} (L : List Form) (P Q M : Form → Prop) [DecidablePred P] [DecidablePred Q] [DecidablePred M] : OptimalityTheory.ConstraintSet Form (Fin 3)

The constraints of the paper's (30) are the precedent condition for the desired property P, the phonological constraint demanding it, and the base-identity condition for the property Q of the listed allomorphs carrying the feature M.

Equations

• Steriade1997.con30 L P Q M = ![Steriade1997.lexP L P, Steriade1997.wellFormed P, Steriade1997.lexPM L Q M]

def Steriade1997.con30' {Form : Type u_1} (L : List Form) (P Q M : Form → Prop) [DecidablePred P] [DecidablePred Q] [DecidablePred M] : OptimalityTheory.ConstraintSet Form (Fin 3)

The reverse ranking, with the base-identity condition above the phonological one.

Equations

• Steriade1997.con30' L P Q M = ![Steriade1997.lexP L P, Steriade1997.lexPM L Q M, Steriade1997.wellFormed P]

theorem Steriade1997.con30_profile {Form : Type u_1} (L : List Form) (P Q M : Form → Prop) [DecidablePred P] [DecidablePred Q] [DecidablePred M] (t : Form) : (toLex fun (x : Fin 3) => con30 L P Q M x t) = toLex ![lexP L P t, wellFormed P t, lexPM L Q M t]

The profile of a form under the ranking of (30), constraint by constraint.

theorem Steriade1997.con30'_profile {Form : Type u_1} (L : List Form) (P Q M : Form → Prop) [DecidablePred P] [DecidablePred Q] [DecidablePred M] (t : Form) : (toLex fun (x : Fin 3) => con30' L P Q M x t) = toLex ![lexP L P t, lexPM L Q M t, wellFormed P t]

theorem Steriade1997.lexPM_eq_one {Form : Type u_1} (L : List Form) (P M : Form → Prop) [DecidablePred P] [DecidablePred M] {μ t : Form} (h : μ ∈ L) (hP : P μ) (hM : M μ) (ht : ¬P t) : lexPM L P M t = 1

theorem Steriade1997.wellFormed_eq_one {Form : Type u_1} (P : Form → Prop) [DecidablePred P] {t : Form} (ht : ¬P t) : wellFormed P t = 1

theorem Steriade1997.split_base {Form : Type u_1} (L : List Form) (P Q M : Form → Prop) [DecidablePred P] [DecidablePred Q] [DecidablePred M] {μ₁ μ₂ t : Form} (h₁ : μ₁ ∈ L) (hM₁ : M μ₁) (hQ₁ : Q μ₁) (hP₁ : ¬P μ₁) (h₂ : μ₂ ∈ L) (hP₂ : P μ₂) (hQ₂ : ¬Q μ₂) (hPt : P t) (hQt : Q t) : (toLex fun (x : Fin 3) => con30 L P Q M x t) = toLex ![0, 0, 0] ∧ wellFormed P μ₁ = 1 ∧ lexPM L Q M μ₂ = 1

The split-base effect, the paper's (11): with a listed allomorph μ₁ carrying M and the identifying property Q but not P, and another μ₂ with P but not Q, a novel form with P and Q violates none of the three constraints, while μ₁ violates the phonological constraint and μ₂ the base-identity condition.

theorem Steriade1997.split_wins_of_phono_over_lexPM {Form : Type u_1} (L : List Form) (P Q M : Form → Prop) [DecidablePred P] [DecidablePred Q] [DecidablePred M] {μ₁ μ₂ a b : Form} (h₁ : μ₁ ∈ L) (hM₁ : M μ₁) (hQ₁ : Q μ₁) (h₂ : μ₂ ∈ L) (hP₂ : P μ₂) (hPa : P a) (hQa : ¬Q a) (hPb : ¬P b) (hQb : Q b) : (toLex fun (x : Fin 3) => con30 L P Q M x a) < toLex fun (x : Fin 3) => con30 L P Q M x b

Under the ranking of (30) the form adopting P from a non-base allomorph beats the form faithful to the base's Q but lacking P.

theorem Steriade1997.base_wins_of_lexPM_over_phono {Form : Type u_1} (L : List Form) (P Q M : Form → Prop) [DecidablePred P] [DecidablePred Q] [DecidablePred M] {μ₁ μ₂ a b : Form} (h₁ : μ₁ ∈ L) (hM₁ : M μ₁) (hQ₁ : Q μ₁) (h₂ : μ₂ ∈ L) (hP₂ : P μ₂) (hPa : P a) (hQa : ¬Q a) (hPb : ¬P b) (hQb : Q b) : (toLex fun (x : Fin 3) => con30' L P Q M x b) < toLex fun (x : Fin 3) => con30' L P Q M x a

Under the reverse ranking the base-faithful form wins.

French liaison

inductive Steriade1997.Gender : Type

Grammatical gender.

• masculine : Gender
• feminine : Gender

@[instance_reducible]

instance Steriade1997.instDecidableEqGender : DecidableEq Gender

Equations

• Steriade1997.instDecidableEqGender x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Steriade1997.instReprGender.repr : Gender → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Steriade1997.instReprGender : Repr Gender

Equations

• Steriade1997.instReprGender = { reprPrec := Steriade1997.instReprGender.repr }

def Steriade1997.v : Phonology.Segment

The consonant [v].

Equations

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

def Steriade1997.n : Phonology.Segment

The consonant [n].

Equations

• Steriade1997.n = Phonology.Segment.ofSpecs [(Phonology.Feature.syllabic, false), (Phonology.Feature.consonantal, true), (Phonology.Feature.coronal, true), (Phonology.Feature.nasal, true)]

def Steriade1997.eOral : Phonology.Segment

The oral vowel [ɛ], the accented vowel of the feminine vaine and the first vowel of espoir.

Equations

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

def Steriade1997.eNasal : Phonology.Segment

The nasal vowel [ɛ̃], the accented vowel of the masculine vain.

Equations

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

structure Steriade1997.Adjective : Type

A form of a French adjective is its string of segments and its gender.

• segments : List Phonology.Segment
• gender : Gender

@[instance_reducible]

instance Steriade1997.instDecidableEqAdjective : DecidableEq Adjective

Equations

• Steriade1997.instDecidableEqAdjective = Steriade1997.instDecidableEqAdjective.decEq

def Steriade1997.instDecidableEqAdjective.decEq (x✝ x✝¹ : Adjective) : Decidable (x✝ = x✝¹)

Equations

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

def Steriade1997.Adjective.accentedVowel (t : Adjective) : Option Phonology.Segment

The accented vowel of a form, its last vowel.

Equations

• t.accentedVowel = (List.filter (fun (s : Phonology.Segment) => decide s.IsVowel) t.segments).getLast?

def Steriade1997.Adjective.rime (t : Adjective) : List Phonology.Segment

The rime of the accented syllable of a monosyllabic form, its segments from the vowel on.

Equations

• t.rime = List.dropWhile (fun (s : Phonology.Segment) => decide ¬s.IsVowel) t.segments

def Steriade1997.vainListed : List Adjective

The listed allomorphs of vain are the citation masculine [vɛ̃] and the citation feminine [vɛn].

Equations

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

def Steriade1997.vainMasc : Adjective

The masculine liaison candidates are the citation masculine [vɛ̃], the citation feminine [vɛn], and the split-base blend [vɛ̃n] of the masculine vowel with the feminine consonant.

Equations

• Steriade1997.vainMasc = { segments := [Steriade1997.v, Steriade1997.eNasal], gender := Steriade1997.Gender.masculine }

def Steriade1997.vainFem : Adjective

Equations

• Steriade1997.vainFem = { segments := [Steriade1997.v, Steriade1997.eOral, Steriade1997.n], gender := Steriade1997.Gender.masculine }

def Steriade1997.vainBlend : Adjective

Equations

• Steriade1997.vainBlend = { segments := [Steriade1997.v, Steriade1997.eNasal, Steriade1997.n], gender := Steriade1997.Gender.masculine }

def Steriade1997.lexC : OptimalityTheory.Constraint Adjective

Lex C], the paper's (8), requires a listed precedent for the final consonant [n].

Equations

• Steriade1997.lexC = Steriade1997.lexP Steriade1997.vainListed fun (x : Steriade1997.Adjective) => x.segments.getLast? = some Steriade1997.n

def Steriade1997.noHiatus : OptimalityTheory.Constraint Adjective

*Hiatus counts the adjacent vowels of the adjective followed by the vowel-initial noun espoir.

Equations

• Steriade1997.noHiatus t = Phonology.Hiatus.count (t.segments ++ [Steriade1997.eOral])

def Steriade1997.lexVGender : OptimalityTheory.Constraint Adjective

Lex 'V-gender, the paper's (10), requires the accented vowel to be that of a listed allomorph of the same gender, here the nasal vowel of the masculine.

Equations

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

def Steriade1997.lexSyllable : OptimalityTheory.Constraint Adjective

Lex σ' requires the rime of the accented syllable to be identical in its entirety to that of some listed allomorph.

Equations

• Steriade1997.lexSyllable = OptimalityTheory.Constraint.binary fun (t : Steriade1997.Adjective) => ∀ l ∈ Steriade1997.vainListed, l.rime ≠ t.rime

theorem Steriade1997.noHiatus_vain : noHiatus vainMasc = 1 ∧ noHiatus vainFem = 0 ∧ noHiatus vainBlend = 0

The three candidates differ on *Hiatus as the paper's tableau has them. The citation masculine [vɛ̃] espoir has a hiatus, and the two consonant-final forms have none.

theorem Steriade1997.vain_split : have con := ![lexC, noHiatus, lexVGender, lexSyllable]; ((toLex fun (x : Fin 4) => con x vainBlend) < toLex fun (x : Fin 4) => con x vainMasc) ∧ (toLex fun (x : Fin 4) => con x vainBlend) < toLex fun (x : Fin 4) => con x vainFem

Speakers ranking Lex 'V-gender above Lex σ' select the split-base form [vɛ̃n] espoir over both citation forms.

theorem Steriade1997.vain_feminine : have con := ![lexC, noHiatus, lexSyllable, lexVGender]; ((toLex fun (x : Fin 4) => con x vainFem) < toLex fun (x : Fin 4) => con x vainMasc) ∧ (toLex fun (x : Fin 4) => con x vainFem) < toLex fun (x : Fin 4) => con x vainBlend

Speakers ranking Lex σ' above Lex 'V-gender select the citation feminine [vɛn] espoir.

English -able

inductive Steriade1997.Stress : Type

The stress patterns of a trisyllabic stem allomorph.

• dactyl : Stress
• amphibrach : Stress

@[instance_reducible]

instance Steriade1997.instDecidableEqStress : DecidableEq Stress

Equations

• Steriade1997.instDecidableEqStress x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Steriade1997.instReprStress.repr : Stress → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Steriade1997.instReprStress : Repr Stress

Equations

• Steriade1997.instReprStress = { reprPrec := Steriade1997.instReprStress.repr }

inductive Steriade1997.LexCat : Type

Lexical category of a listed allomorph.

• verb : LexCat
• adjective : LexCat

@[instance_reducible]

instance Steriade1997.instDecidableEqLexCat : DecidableEq LexCat

Equations

• Steriade1997.instDecidableEqLexCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Steriade1997.instReprLexCat.repr : LexCat → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Steriade1997.instReprLexCat : Repr LexCat

Equations

• Steriade1997.instReprLexCat = { reprPrec := Steriade1997.instReprLexCat.repr }

structure Steriade1997.Stem : Type

A stem allomorph by its stress pattern and lexical category.

• stress : Stress
• lexcat : LexCat

@[instance_reducible]

instance Steriade1997.instDecidableEqStem : DecidableEq Stem

Equations

• Steriade1997.instDecidableEqStem = Steriade1997.instDecidableEqStem.decEq

def Steriade1997.instDecidableEqStem.decEq (x✝ x✝¹ : Stem) : Decidable (x✝ = x✝¹)

Equations

• Steriade1997.instDecidableEqStem.decEq { stress := a, lexcat := a_1 } { stress := b, lexcat := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Steriade1997.instReprStem : Repr Stem

Equations

• Steriade1997.instReprStem = { reprPrec := Steriade1997.instReprStem.repr }

def Steriade1997.instReprStem.repr : Stem → ℕ → Std.Format

Equations

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

def Steriade1997.remedyListed : List Stem

The listed allomorphs of remedy are the dactylic verb rémedy and the amphibrachic adjective stem of remédial, the paper's (13).

Equations

• Steriade1997.remedyListed = [{ stress := Steriade1997.Stress.dactyl, lexcat := Steriade1997.LexCat.verb }, { stress := Steriade1997.Stress.amphibrach, lexcat := Steriade1997.LexCat.adjective }]

def Steriade1997.parodyListed : List Stem

The only listed allomorph of parody is the dactylic verb.

Equations

• Steriade1997.parodyListed = [{ stress := Steriade1997.Stress.dactyl, lexcat := Steriade1997.LexCat.verb }]

def Steriade1997.dactylAble : Stem

The -able stem is verbal; the candidates differ in stress.

Equations

• Steriade1997.dactylAble = { stress := Steriade1997.Stress.dactyl, lexcat := Steriade1997.LexCat.verb }

def Steriade1997.amphibrachAble : Stem

Equations

• Steriade1997.amphibrachAble = { stress := Steriade1997.Stress.amphibrach, lexcat := Steriade1997.LexCat.verb }

def Steriade1997.lexStress (L : List Stem) : OptimalityTheory.Constraint Stem

Lex [±stress], the paper's (15), requires a listed precedent for the stress pattern.

Equations

• Steriade1997.lexStress L = Steriade1997.lexP L fun (x : Steriade1997.Stem) => x.stress = Steriade1997.Stress.amphibrach

def Steriade1997.noLapse : OptimalityTheory.Constraint Stem

*Lapse σσσ bans three stressless syllables before -able, so the stem must shift its stress rightward.

Equations

• Steriade1997.noLapse = Steriade1997.wellFormed fun (x : Steriade1997.Stem) => x.stress = Steriade1997.Stress.amphibrach

def Steriade1997.lexStressLexcat (L : List Stem) : OptimalityTheory.Constraint Stem

Lex([±stress], lexcat), the paper's (17), requires the stress pattern of the verbal target to match that of a listed verbal allomorph.

Equations

• Steriade1997.lexStressLexcat L = Steriade1997.lexPM L (fun (x : Steriade1997.Stem) => x.stress = Steriade1997.Stress.dactyl) fun (x : Steriade1997.Stem) => x.lexcat = Steriade1997.LexCat.verb

theorem Steriade1997.remediable : ((toLex fun (x : Fin 3) => con30 remedyListed (fun (x : Stem) => x.stress = Stress.amphibrach) (fun (x : Stem) => x.stress = Stress.dactyl) (fun (x : Stem) => x.lexcat = LexCat.verb) x amphibrachAble) < toLex fun (x : Fin 3) => con30 remedyListed (fun (x : Stem) => x.stress = Stress.amphibrach) (fun (x : Stem) => x.stress = Stress.dactyl) (fun (x : Stem) => x.lexcat = LexCat.verb) x dactylAble) ∧ (toLex fun (x : Fin 3) => con30' remedyListed (fun (x : Stem) => x.stress = Stress.amphibrach) (fun (x : Stem) => x.stress = Stress.dactyl) (fun (x : Stem) => x.lexcat = LexCat.verb) x dactylAble) < toLex fun (x : Fin 3) => con30' remedyListed (fun (x : Stem) => x.stress = Stress.amphibrach) (fun (x : Stem) => x.stress = Stress.dactyl) (fun (x : Stem) => x.lexcat = LexCat.verb) x amphibrachAble

remédiable wins under the ranking Lex [±stress] ≫ *Lapse ≫ Lex([±stress], lexcat) and rémediable under Lex [±stress] ≫ Lex([±stress], lexcat) ≫ *Lapse, the paper's (18).

theorem Steriade1997.parodiable : ((toLex fun (x : Fin 3) => con30 parodyListed (fun (x : Stem) => x.stress = Stress.amphibrach) (fun (x : Stem) => x.stress = Stress.dactyl) (fun (x : Stem) => x.lexcat = LexCat.verb) x dactylAble) < toLex fun (x : Fin 3) => con30 parodyListed (fun (x : Stem) => x.stress = Stress.amphibrach) (fun (x : Stem) => x.stress = Stress.dactyl) (fun (x : Stem) => x.lexcat = LexCat.verb) x amphibrachAble) ∧ (toLex fun (x : Fin 3) => con30' parodyListed (fun (x : Stem) => x.stress = Stress.amphibrach) (fun (x : Stem) => x.stress = Stress.dactyl) (fun (x : Stem) => x.lexcat = LexCat.verb) x dactylAble) < toLex fun (x : Fin 3) => con30' parodyListed (fun (x : Stem) => x.stress = Stress.amphibrach) (fun (x : Stem) => x.stress = Stress.dactyl) (fun (x : Stem) => x.lexcat = LexCat.verb) x amphibrachAble

With no amphibrachic allomorph listed, paródiable violates Lex [±stress], so párodiable wins under either ranking despite its lapse.