Paradigm linkage

import Linglib.Morphology.Paradigm.Linkage · namespace Morphology

This file defines Stump's paradigm linkage, which realizes a lexeme's content cell ⟨l, σ⟩ through form cells ⟨z, τ⟩ of its stems. A linkage is a stem selection, a Realization of lexemes by stems, together with a lexeme-sensitive property mapping from content property sets to form property sets. Each deviation from canonical linkage negates one of its axes, after Corbett's canonical typology. Stump maintains that PRAMEN, whose stem is phonologically constant across two inflection classes, exhibits "a kind of stem suppletion", on which view heteroclisis "simply entails suppletion". Stump's rules of paradigm linkage compete by Pāṇini's principle, here the Elsewhere selection of a narrowest applicable rule, and a cell that no rule reaches takes the lexeme's root.

Main definitions

Linkage, Linkage.corr, Linkage.realized: the linkage, its form correspondents, and the realized paradigm.
Linkage.IsCanonical, relative to an identification ι of content with form property sets, with the deviations IsDefective, IsSyncretic, IsUnfaithful.
Linkage.IsInvariantAlong, Linkage.IsHeteroclite: per-lexeme invariance and variance of stems along a projection, such as their inflection class.
Linkage.ofFun, Linkage.canonical: the linkage of a stem-choice function.
Linkage.ofRules: the linkage of rules of paradigm linkage, each cell taking the stem its lexeme's rules realize over the lexeme's root.
Linkage.toInflectionalParadigm: the inflectional paradigm of a linkage's form correspondents.

Main results

Linkage.IsHeteroclite.isSuppletive, Linkage.IsHeteroclite.not_isClassDetermined: heteroclisis entails suppletion, the stems of a heteroclite lexeme being determined by no one class.
Linkage.realized_eq_of_corr_eq: equal correspondent sets force equal realizations.
Linkage.ofFun_isCanonical_iff: under an injective identification, the linkage of a stem choice is canonical exactly when each lexeme's stem is constant.
Linkage.ofRules_nil: with no language-specific rules, the linkage of rules is the canonical linkage of the roots.

Implementation notes

IsTotal, IsUnivalent, and the per-lexeme IsInvariant, IsSuppletive, and IsOverabundant (Thornton's cell-mates) are inherited from Realization. Taking S = M and ι = id recovers a single type of property sets. The universal default rule (5) is not a listed rule of ofRules but the fallback of Exponence.RuleSet.realizeMinimalD, the lexeme's root.

References

Corbett 2007, Canonical typology, suppletion, and possible words
Stump 2006, Heteroclisis and Paradigm Linkage formalized
Stump 2012, The formal and functional architecture of inflectional morphology formalized
Stump 2016, Inflectional Paradigms: Content and Form at the Syntax-Morphology Interface formalized
Thornton 2011, Overabundance (Multiple Forms Realizing the Same Cell): A Non-canonical Phenomenon in Italian Verb Morphology

Declarations

A paradigm linkage (Stump 2012) consists of a stem selection, the inherited realize, which gives the finite set of stems realizing each content cell ⟨l, σ⟩, and a property mapping pm. The stem set is empty at a gap in the stem specification and has several members at an overabundant cell. Content and form cells carry property sets of types S and M, since Stump 2006 (p. 288) distinguishes a language's s-properties, "any property belonging to σ in a content-cell ⟨L, σ⟩", from its m-properties, "any property belonging to τ in a form-cell ⟨s, τ⟩", so that the relation between their property sets "can be represented as a function from sets of s-properties to sets of m-properties", a property mapping; "in the simplest cases—those determined by the default rule of paradigm linkage in 5—the relevant property mapping is an identity function".

structure Linkage L67–80

(L : Type u_1) (Z : Type u_2) (S : Type u_3) (M : Type u_4) extends Realization L S Z :

Type (max (max (max u_1 u_2) u_3) u_4)

realize : L → S → Finset Z
pm : L → S → M
The property mapping carries a content cell's property set to that of its form correspondents, and may consult the lexeme.

Used in Morphology/Paradigm/Function, JackendoffAudring2020, Stump2006, Stump2012, Stump2016

The form correspondents of a content cell ⟨l, σ⟩ pair each of its stems with the mapped property set ℓ.pm l σ.

def Linkage.corr L86–88

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} (ℓ : Linkage L Z S M) (l : L) (σ : S) :

Finset (Z × M)

ℓ.corr l σ = ℓ.realize l σ ×ˢ {ℓ.pm l σ}

Built from

Used by Linkage.mem_corr, Linkage.corr_nonempty, Linkage.card_corr, Linkage.IsInjective, Linkage.IsSyncretic, Linkage.IsVirtual, Linkage.instDecidableIsVirtualOfDecidableEq, Linkage.realized_eq_image_corr, Linkage.realized_eq_of_corr_eq, Linkage.toInflectionalParadigm, Linkage.ofFun_corr

Used in JackendoffAudring2020, Stump2006, Stump2012, Stump2016

L90–92

L94–96

L98–99

The realized paradigm of a content cell realizes each form correspondent ⟨z, τ⟩ as rf z τ, keeping the property set τ.

def Linkage.realized L101–104

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} {W : Type u_5} (ℓ : Linkage L Z S M) [DecidableEq W] (rf : Z → M → W) (l : L) (σ : S) :

Finset (W × M)

ℓ.realized rf l σ = Finset.image (fun (z : Z) => rf z (ℓ.pm l σ)) (ℓ.realize l σ) ×ˢ {ℓ.pm l σ}

Built from

Used by Linkage.mem_realized, Linkage.realized_eq_image_corr, Linkage.realized_eq_of_corr_eq, Linkage.ofFun_realized

Used in Morphology/Paradigm/Function, JackendoffAudring2020, Stump2006, Stump2012

L106–108

Canonical linkage

L112–114

L116–117

L119–122

A linkage is canonical (Stump 2012) relative to an identification ι of content with form property sets when it satisfies all five axes.

structure Linkage.IsCanonical L124–136

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} (ℓ : Linkage L Z S M) (ι : S → M) :

Prop

total : ℓ.IsTotal
Every content cell has a form correspondent.
univalent : ℓ.IsUnivalent
No content cell has more than one form correspondent.
stemInvariant : ℓ.IsStemInvariant
Each lexeme draws on a single stem.
injective : ℓ.IsInjective
No two content cells of a lexeme share a form correspondent.
propertyPreserving : ℓ.IsPropertyPreserving ι
Every form correspondent carries the image of its content cell's property set.

Built from , , ,

Used by Linkage.ofFun_isCanonical_iff, Linkage.canonical_isCanonical

Used in Stump2012, Stump2016

Deviations from canonical linkage

A linkage is defective (Stump 2012) when some content cell has no stem.

def Linkage.IsDefective L140–141

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} (ℓ : Linkage L Z S M) :

Prop

ℓ.IsDefective = ∃ (l : L) (σ : S), ℓ.realize l σ = ∅

Built from

Used by Linkage.not_isTotal_iff, Linkage.instDecidableIsDefectiveOfDecidableEq

Used in Stump2012

A linkage is syncretic (Stump 2012) when two distinct content cells of a lexeme share a form correspondent.

def Linkage.IsSyncretic L143–145

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} (ℓ : Linkage L Z S M) :

Prop

ℓ.IsSyncretic = ∃ (l : L) (σ₁ : S) (σ₂ : S), σ₁ ≠ σ₂ ∧ ¬Disjoint (ℓ.corr l σ₁) (ℓ.corr l σ₂)

Built from ,

Used by Linkage.not_isInjective_iff, Linkage.instDecidableIsSyncreticOfDecidableEq

Used in Stump2006, Stump2012, Stump2016

A linkage is unfaithful (Stump 2012) relative to ι when some content cell's form correspondents carry a property set other than its image under ι, as under deponency and functor-argument reversal.

def Linkage.IsUnfaithful L147–150

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} (ℓ : Linkage L Z S M) (ι : S → M) :

Prop

ℓ.IsUnfaithful ι = ∃ (l : L) (σ : S), ℓ.pm l σ ≠ ι σ

Built from

Used by Linkage.not_isPropertyPreserving_iff, Linkage.instDecidableIsUnfaithfulOfDecidableEq

Used in Stump2006, Stump2012

Invariance along a projection

A lexeme is invariant along p when the stems of all its cells have one image under p; along id this is IsInvariant.

def Linkage.IsInvariantAlong L172–175

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} {X : Type u_6} (ℓ : Linkage L Z S M) (p : Z → X) (l : L) :

Prop

ℓ.IsInvariantAlong p l = ∀ ⦃σ σ' : S⦄, ∀ z ∈ ℓ.realize l σ, ∀ z' ∈ ℓ.realize l σ', p z = p z'

Built from

Used by Linkage.isInvariantAlong_id_iff, Linkage.not_isInvariantAlong_iff, Linkage.IsInvariantAlong.comp, Realization.IsInvariant.isInvariantAlong, Linkage.instDecidableIsInvariantAlongOfDecidableEq, Linkage.ofFun_isInvariantAlong_iff

Used in Stump2006

A lexeme is heteroclite along a classification cls of stems (Stump 2006) when two of its cells draw on stems of distinct classes; along id this is IsSuppletive.

def Linkage.IsHeteroclite L177–180

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} {K : Type u_8} (ℓ : Linkage L Z S M) (cls : Z → K) (l : L) :

Prop

ℓ.IsHeteroclite cls l = ∃ (σ : S) (σ' : S), ∃ z ∈ ℓ.realize l σ, ∃ z' ∈ ℓ.realize l σ', cls z ≠ cls z'

Built from

Used by Linkage.isHeteroclite_id_iff, Linkage.not_isInvariantAlong_iff, Linkage.IsHeteroclite.isSuppletive, Linkage.IsHeteroclite.not_isClassDetermined, Linkage.instDecidableIsHeterocliteOfDecidableEq, Linkage.ofFun_isHeteroclite_iff

Used in Stump2006

Heteroclisis entails suppletion, since stems of two classes are two stems.

theorem Linkage.IsHeteroclite.isSuppletive L200–203

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} {K : Type u_8} {ℓ : Linkage L Z S M} {cls : Z → K} {l : L} (h : ℓ.IsHeteroclite cls l) :

ℓ.IsSuppletive l

Built from ,

When each pattern draws its stems from one class, a heteroclite lexeme's stems are not class-determined, so their alternation is suppletion in Stump 2016's sense.

theorem Linkage.IsHeteroclite.not_isClassDetermined L205–211

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} {K : Type u_8} {ℓ : Linkage L Z S M} {cls : Z → K} {l : L} {A : Set (S → Z)} (hA : ∀ p ∈ A, ∀ (σ σ' : S), cls (p σ) = cls (p σ')) (h : ℓ.IsHeteroclite cls l) :

¬ℓ.IsClassDetermined A l

Built from ,

Decidability

Each instance is inferInstanceAs on the definition's body, so that decide reduces in the kernel. The per-lexeme instances quantify over stem sets and need no Fintype Z.

Realization through correspondents

L263–265

Equal correspondent sets force equal realizations, within a lexeme (the mechanism of syncretism) and across lexemes.

theorem Linkage.realized_eq_of_corr_eq L267–272

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} {W : Type u_5} (ℓ : Linkage L Z S M) [DecidableEq W] (rf : Z → M → W) {l₁ l₂ : L} {σ₁ σ₂ : S} (h : ℓ.corr l₁ σ₁ = ℓ.corr l₂ σ₂) :

ℓ.realized rf l₁ σ₁ = ℓ.realized rf l₂ σ₂

Built from , ,

The inflectional paradigm of a linkage

The inflectional paradigm of a linkage with realization rules rf builds the forms of each content cell from its form correspondents.

def Linkage.toInflectionalParadigm L278–280

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} {W : Type u_5} {ℓ : Linkage L Z S M} (rf : Z → M → W) :

InflectionalParadigm L S Z M W

Linkage.toInflectionalParadigm rf = { parts := { realize := ℓ.corr }, compose := rf }

Built from ,

Used by Linkage.toInflectionalParadigm_stem, Linkage.isStemInvariant_iff_stem_isInvariant, Linkage.toInflectionalParadigm_realization_realize

L286–293

L295–299

L301–305

Linkages of stem-choice functions

The linkage of a stem choice f under an identification ι gives the content cell ⟨l, σ⟩ the single stem f l σ and the form property set ι σ.

def Linkage.ofFun L311–315

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} (ι : S → M) (f : L → S → Z) :

Linkage L Z S M

Linkage.ofFun ι f = { realize := fun (l : L) (σ : S) => {f l σ}, pm := fun (x : L) (σ : S) => ι σ }

Built from

Used by Linkage.ofFun_realize, Linkage.ofFun_pm, Linkage.ofFun_corr, Linkage.ofFun_realized, Linkage.ofFun_isInvariantAlong_iff, Linkage.ofFun_isHeteroclite_iff, Linkage.ofFun_isCanonical_iff, Linkage.canonical, Linkage.ofRules

Under an injective identification, the linkage of a stem choice is canonical exactly when each lexeme's stem is independent of the property set.

theorem Linkage.ofFun_isCanonical_iff L342–349

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} {ι : S → M} {f : L → S → Z} (hι : Function.Injective ι) :

(ofFun ι f).IsCanonical ι ↔ ∀ (l : L) (σ σ' : S), f l σ = f l σ'

Built from ,

The canonical linkage of st under ι gives every cell of the lexeme l the stem st l and the image under ι of its property set. It is the linkage of the universal default rule of paradigm linkage (5) of Stump 2006 with no language-specific rules (ofRules_nil), st l being the root of l.

@[reducible, inline] abbrev Linkage.canonical L353–357

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} (ι : S → M) (st : L → Z) :

Linkage L Z S M

Linkage.canonical ι st = Linkage.ofFun ι fun (l : L) (x : S) => st l

Built from ,

Used by Linkage.canonical_isCanonical, Linkage.ofRules_nil

Used in Stump2012

L359–361

Rules of paradigm linkage

The linkage of rules of paradigm linkage gives each content cell the stem that its lexeme's rules realize, the exponent of an applicable rule that no applicable rule is narrower than under key, or the lexeme's root, by the universal default rule (5) of Stump 2006, where none of its rules applies; its form property set is the image under ι of the cell's.

@[reducible, inline] abbrev Linkage.ofRules L370–376

{L : Type u_1} {Z : Type u_2} {S : Type u_3} {M : Type u_4} {R : Type u_9} [Exponence.Rule R S Z] {κ : Type u_10} [Preorder κ] [DecidableRel fun (x1 x2 : κ) => x1 < x2] [DecidableRel Exponence.Applies] (ι : S → M) (key : R → κ) (rules : L → List R) (root : L → Z) :

Linkage L Z S M

Linkage.ofRules ι key rules root = Linkage.ofFun ι fun (l : L) (σ : S) => Exponence.RuleSet.realizeMinimalD (rules l) key (fun (x : S) => root l) σ

Built from ,

Used by Linkage.ofRules_nil

Used in Stump2006

With no language-specific rules, the linkage of rules is the canonical linkage of the roots.

theorem Linkage.ofRules_nil L378–382

ofRules ι key (fun (x : L) => []) st = canonical ι st

Built from ,