Docs / Morphology / Exponence / Elsewhere

The Elsewhere Condition

import Linglib.Morphology.Exponence.Elsewhere

An Elsewhere winner of a rule set at a context is a rule that applies there and is minimal, among the rules that apply, in specificity. Specificity is read through a key into an ordered type, as closeness is for a probe: Kiparsky's specificity is the key applySet, a rule being more specific when it applies in fewer contexts, and other theories choose other keys. This file defines Elsewhere winners and the prediction relation they induce.

Main definitions

RuleSet.IsElsewhereWinner: an applicable rule of a rule set at a context that no applicable rule is more specific than.
RuleSet.Coherent: rules equally specific carry the same exponent.
RuleSet.Realizes: some Elsewhere winner carries the given exponent.
RuleSet.Antihomophonous: distinct rules carry distinct exponents.

Main results

RuleSet.Realizes.eq: where the Elsewhere winners form a chain, Pāṇinian Determinism, a coherent rule set makes a unique prediction.
RuleSet.Realizes.of_realizes: no ABA pattern across nested contexts.

References

Kiparsky 1973, “Elsewhere” in Phonology
Bobaljik 2012, Universals in comparative morphology: Suppletion, superlatives, and the structure of words formalized

Elsewhere winners

L47–50

An applicable rule of v at c that no applicable rule is more specific than, specificity read through key.

@[reducible, inline] abbrev Morphology.Exponence.RuleSet.IsElsewhereWinner L52–55

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] {κ : Type u_4} [Preorder κ] (v : RuleSet R) (key : R → κ) (c : Ctx) (r : R) :

Prop

v.IsElsewhereWinner key c r = MinimalFor (fun (s : R) => s ∈ v ∧ Morphology.Exponence.Applies s c) key r

Used by Morphology.Exponence.RuleSet.IsElsewhereWinner.exponent_eq, Morphology.Exponence.RuleSet.exists_isElsewhereWinner, Morphology.Exponence.RuleSet.Realizes, Morphology.Exponence.RuleSet.Realizes.eq, Morphology.Exponence.RuleSet.IsElsewhereWinner.of_applies

Used in Morphology/DistributedMorphology/VocabularyInsertion/Basic, Morphology/Exponence/Domain, Morphology/Exponence/Select, Morphology/Nanosyntax/TreeSpellout, ODonnell2015

A rule set is coherent if rules equally specific carry the same exponent.

def Morphology.Exponence.RuleSet.Coherent L57–59

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] {κ : Type u_4} [Preorder κ] (v : RuleSet R) (key : R → κ) :

Prop

v.Coherent key = ∀ r ∈ v, ∀ s ∈ v, AntisymmRel (fun (x1 x2 : κ) => x1 ≤ x2) (key r) (key s) → Morphology.Exponence.exponent r = Morphology.Exponence.exponent s

Used by Morphology.Exponence.RuleSet.IsElsewhereWinner.exponent_eq, Morphology.Exponence.RuleSet.Realizes.eq

Used in Morphology/Exponence/Select

L61–64

L66–68

The prediction relation

φ is realized at c when some Elsewhere winner carries it.

def Morphology.Exponence.RuleSet.Realizes L72–74

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] {κ : Type u_4} [Preorder κ] (v : RuleSet R) (key : R → κ) (c : Ctx) (φ : E) :

Prop

v.Realizes key c φ = ∃ (r : R), v.IsElsewhereWinner key c r ∧ Morphology.Exponence.exponent r = φ

Built from

Used by Morphology.Exponence.RuleSet.Realizes.eq, Morphology.Exponence.RuleSet.Realizes.of_realizes

Used in Morphology/DistributedMorphology/VocabularyInsertion/Basic, Morphology/Exponence/Containment/Selection, Morphology/Exponence/Select, AdamsonAnagnostopoulou2025

Over a coherent rule set whose Elsewhere winners form a chain, Stump's Pāṇinian Determinism, the prediction is unique.

theorem Morphology.Exponence.RuleSet.Realizes.eq L76–83

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] {κ : Type u_4} [Preorder κ] {key : R → κ} {v : RuleSet R} {c : Ctx} {φ ψ : E} (hv : v.Coherent key) (hc : IsChain (fun (r s : R) => key r ≤ key s) {s : R | v.IsElsewhereWinner key c s}) (hφ : v.Realizes key c φ) (hψ : v.Realizes key c ψ) :

φ = ψ

Built from , ,

Containment

A rule set is antihomophonous when distinct rules carry distinct exponents, setting accidental homophony aside. This generalizes Bobaljik 2012's Antihomophony, which bars only a contextual allomorph homophonous with the default; homophonous contextual allomorphs break contiguity from four nested contexts on.

def Morphology.Exponence.RuleSet.Antihomophonous L87–92

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] (v : RuleSet R) :

Prop

v.Antihomophonous = Set.InjOn Morphology.Exponence.exponent {r : R | r ∈ v}

Used by Morphology.Exponence.RuleSet.instDecidableAntihomophonousOfDecidableEq, Morphology.Exponence.RuleSet.Realizes.of_realizes

Used in Morphology/DistributedMorphology/VocabularyInsertion/Basic, Morphology/Exponence/Containment/Contiguity, Morphology/Exponence/Containment/Selection, Morphology/Exponence/Domain, Morphology/Exponence/Select and 6 more

L94–95

L97–99

There is no ABA across nested contexts. Over an antihomophonous rule set, an exponent realized at the smallest and the largest of three nested contexts is realized at the middle one.

theorem Morphology.Exponence.RuleSet.Realizes.of_realizes L101–110

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] {κ : Type u_4} [Preorder κ] {key : R → κ} {v : RuleSet R} {c : Ctx} {φ : E} {c₁ c₂ : Ctx} (hv : v.Antihomophonous) (h₁ : ∀ s ∈ v, Applies s c₁ → Applies s c₂) (h₂ : ∀ s ∈ v, Applies s c₂ → Applies s c) (hr₁ : v.Realizes key c₁ φ) (hr : v.Realizes key c φ) :

v.Realizes key c₂ φ

Built from ,