Stump 2016: paradigm-linkage deviations — deponency and morphomic tense

[Stu16]

Two deviations from the canonical content-to-form isomorphism argued for in [Stu16], run on the paradigm-linkage model of Morphology/Paradigm/Linkage.lean.

Latin deponency (Ch. 12): deponent verbs "inflect by means of the morphology that ordinarily serves to express a verb's passive forms" (§12.1). Deponent cōnārī 'try' realizes its active content cells — cōnor, cōnāris, cōnātur, cōnāmur, cōnāminī, cōnantur (imperfective present indicative, Table 12.2) — with the passive personal endings (-or, -ris, -tur, -mur, -minī, -ntur) that a regular verb like parāre 'prepare' uses only for its passive (paror, parāris, parātur, …, Table 12.1); cōnārī lacks passive-meaning forms entirely. This is a property mapping that crosses the voice axis: a regular verb is subject to the canonical pmc(σ) = σ ∪ {c}, a deponent to pm2c(σ:{active}) = σ[active/passive] ∪ {c} (§12.1), replacing active with passive. Abstracting away the inflection-class index c, the deponent linkage flips voice while the regular verb's preserves it — cōnārī's linkage deviates from IsCanonical on every active cell.

Kashmiri morphomic tense (Ch. 8, pp. 217ff): the recent, indefinite, and remote preterites of intransitive Conjugations II and III are realized through four morphomic properties 'past a'–'past d' via a non-identity property mapping. WUP (Conj II) and WUPH (Conj III) inflect alike in the 'past b' cells — wupyōs (indefinite) and wuphyōs (recent) — because pmII and pmIII send different tenses to the same morphome. The composition exercises the PFM1 block cascade of Morphology/Paradigm/Function.lean as the form-cell realization, with pm ≠ id, so Linkage.realize_eq_paradigmFunction (which needs pm = id) does not apply. Forms are transcribed from Grierson's paradigms as displayed by [Stu16]; block rules are read off the stem+suffix segmentation.

Main declarations

• conariLinkage, parareLinkage — the deponent and regular linkages
• parareLinkage_isCanonical — the regular verb's voice-preserving linkage is canonical
• conari_deviates_on_every_active_cell — the deponent pm moves every active content cell off its own property set
• conari_active_realized_by_passive_form — every active content cell's form correspondent is passive (the deponency claim)
• depon_vs_regular — same active content cell: regular → active form, deponent → passive form
• pmII, pmIII, linkII, linkIII — the two Kashmiri conjugation linkages, their tense-to-morphome property mappings differing by one morphome
• kashmiri_inflect_alike — WUP's indefinite past and WUPH's recent past share the 'past b' form correspondent, the morphomic content-to-form mismatch

inductive Stump2016.Voice : Type

Voice: the axis Latin deponency crosses ([Stu16] §12.1).

• active : Voice
• passive : Voice

@[implicit_reducible]

instance Stump2016.instDecidableEqVoice : DecidableEq Voice

Equations

• Stump2016.instDecidableEqVoice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2016.instReprVoice : Repr Voice

Equations

• Stump2016.instReprVoice = { reprPrec := Stump2016.instReprVoice.repr }

def Stump2016.instReprVoice.repr : Voice → ℕ → Std.Format

Equations

• Stump2016.instReprVoice.repr Stump2016.Voice.active prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.Voice.active")).group prec✝
• Stump2016.instReprVoice.repr Stump2016.Voice.passive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.Voice.passive")).group prec✝

inductive Stump2016.Agr : Type

Person–number agreement: the six cells of the imperfective present indicative ([Stu16] Tables 12.1–12.2).

• s1 : Agr
• s2 : Agr
• s3 : Agr
• p1 : Agr
• p2 : Agr
• p3 : Agr

@[implicit_reducible]

instance Stump2016.instDecidableEqAgr : DecidableEq Agr

Equations

• Stump2016.instDecidableEqAgr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2016.instReprAgr : Repr Agr

Equations

• Stump2016.instReprAgr = { reprPrec := Stump2016.instReprAgr.repr }

def Stump2016.instReprAgr.repr : Agr → ℕ → Std.Format

Equations

• Stump2016.instReprAgr.repr Stump2016.Agr.s1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.Agr.s1")).group prec✝
• Stump2016.instReprAgr.repr Stump2016.Agr.s2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.Agr.s2")).group prec✝
• Stump2016.instReprAgr.repr Stump2016.Agr.s3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.Agr.s3")).group prec✝
• Stump2016.instReprAgr.repr Stump2016.Agr.p1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.Agr.p1")).group prec✝
• Stump2016.instReprAgr.repr Stump2016.Agr.p2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.Agr.p2")).group prec✝
• Stump2016.instReprAgr.repr Stump2016.Agr.p3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.Agr.p3")).group prec✝

structure Stump2016.Cell : Type

A morphosyntactic property set, abstracted to the voice axis and the agreement features relevant to Latin deponency (the inflection-class index and tense/aspect/mood, held constant across the paradigm below, are elided).

• agr : Agr
• voice : Voice

@[implicit_reducible]

instance Stump2016.instDecidableEqCell : DecidableEq Cell

Equations

• Stump2016.instDecidableEqCell = Stump2016.instDecidableEqCell.decEq

def Stump2016.instDecidableEqCell.decEq (x✝ x✝¹ : Cell) : Decidable (x✝ = x✝¹)

Equations

• Stump2016.instDecidableEqCell.decEq { agr := a, voice := a_1 } { agr := b, voice := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Stump2016.instReprCell.repr : Cell → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Stump2016.instReprCell : Repr Cell

Equations

• Stump2016.instReprCell = { reprPrec := Stump2016.instReprCell.repr }

inductive Stump2016.LatinVerb : Type

The two Latin lexemes contrasted: the deponent cōnārī and the regular parāre.

• conari : LatinVerb
• parare : LatinVerb

@[implicit_reducible]

instance Stump2016.instDecidableEqLatinVerb : DecidableEq LatinVerb

Equations

• Stump2016.instDecidableEqLatinVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Stump2016.instReprLatinVerb.repr : LatinVerb → ℕ → Std.Format

Equations

• Stump2016.instReprLatinVerb.repr Stump2016.LatinVerb.conari prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.LatinVerb.conari")).group prec✝
• Stump2016.instReprLatinVerb.repr Stump2016.LatinVerb.parare prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.LatinVerb.parare")).group prec✝

@[implicit_reducible]

instance Stump2016.instReprLatinVerb : Repr LatinVerb

Equations

• Stump2016.instReprLatinVerb = { reprPrec := Stump2016.instReprLatinVerb.repr }

inductive Stump2016.LatinStem : Type

Their stems.

• cona : LatinStem
• para : LatinStem

@[implicit_reducible]

instance Stump2016.instDecidableEqLatinStem : DecidableEq LatinStem

Equations

• Stump2016.instDecidableEqLatinStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Stump2016.instReprLatinStem.repr : LatinStem → ℕ → Std.Format

Equations

• Stump2016.instReprLatinStem.repr Stump2016.LatinStem.cona prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.LatinStem.cona")).group prec✝
• Stump2016.instReprLatinStem.repr Stump2016.LatinStem.para prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2016.LatinStem.para")).group prec✝

@[implicit_reducible]

instance Stump2016.instReprLatinStem : Repr LatinStem

Equations

• Stump2016.instReprLatinStem = { reprPrec := Stump2016.instReprLatinStem.repr }

def Stump2016.conariLinkage : Morphology.Linkage LatinVerb LatinStem Cell

The deponent linkage of cōnārī: a single stem and the voice-flipping property mapping pm2c ([Stu16] §12.1), which sends an active content cell to a passive form cell.

Equations

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

def Stump2016.parareLinkage : Morphology.Linkage LatinVerb LatinStem Cell

The regular linkage of parāre: a single stem and the identity property mapping, canonical on the voice axis ([Stu16] §7.1).

Equations

• Stump2016.parareLinkage = { stems := fun (x : Stump2016.LatinVerb) (x_1 : Stump2016.Cell) => {Stump2016.LatinStem.para}, pm := fun (x : Stump2016.LatinVerb) (σ : Stump2016.Cell) => σ }

def Stump2016.conariContentCells : List Cell

cōnārī's six active content cells ([Stu16] Table 12.2).

Equations

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

theorem Stump2016.parareLinkage_isCanonical : parareLinkage.IsCanonical

The regular verb's linkage is canonical: property-set preserving (pm = id) and stem invariant ([Stu16] §7.1, characteristics (2a)–(2b)).

theorem Stump2016.conari_pm_flips_voice (l : LatinVerb) (σ : Cell) : (conariLinkage.pm l σ).voice = Voice.passive

The deponent property mapping flips voice on every active cell.

theorem Stump2016.conari_deviates_on_every_active_cell (l : LatinVerb) (σ : Cell) (h : σ.voice = Voice.active) : conariLinkage.pm l σ ≠ σ

The deponent linkage deviates from the canonical isomorphism on every active content cell: its property mapping moves the cell off its own property set.

theorem Stump2016.conariLinkage_not_canonical : ¬conariLinkage.IsCanonical

Hence the deponent linkage is not property-preserving, so not canonical.

theorem Stump2016.conari_active_realized_by_passive_form (l : LatinVerb) (σ : Cell) : Finset.image (fun (x : LatinStem × Cell) => x.2.voice) (conariLinkage.corr l σ) = {Voice.passive}

The deponency claim: every active content cell of cōnārī has a passive form correspondent — active content realized by passive morphology ([Stu16] §12.1).

theorem Stump2016.conari_all_cells_cross_voice (σ : Cell) : σ ∈ conariContentCells → conariLinkage.pm LatinVerb.conari σ ≠ σ

Every one of cōnārī's six active content cells crosses the voice axis.

theorem Stump2016.depon_vs_regular (σ : Cell) (h : σ.voice = Voice.active) : Finset.image (fun (x : LatinStem × Cell) => x.2.voice) (parareLinkage.corr LatinVerb.parare σ) = {Voice.active} ∧ Finset.image (fun (x : LatinStem × Cell) => x.2.voice) (conariLinkage.corr LatinVerb.conari σ) = {Voice.passive}

The crisp contrast: on the same active content cell, the regular verb's form correspondent stays active while the deponent's becomes passive — deviation without any difference in the content-cell space.

Kashmiri morphomic tense (Ch. 8, pp. 217ff)

inductive Stump2016.KVerb : Type

The two intransitive verbs: WUP 'burn inside' (Conj II) and WUPH 'fly' (Conj III).

• wup : KVerb
• wuph : KVerb

@[implicit_reducible]

instance Stump2016.instDecidableEqKVerb : DecidableEq KVerb

Equations

• Stump2016.instDecidableEqKVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2016.instFintypeKVerb : Fintype KVerb

Equations

• Stump2016.instFintypeKVerb = { elems := { val := ↑Stump2016.KVerb.enumList, nodup := Stump2016.KVerb.enumList_nodup }, complete := Stump2016.instFintypeKVerb._proof_1 }

inductive Stump2016.KFeat : Type

Content tenses (recent, indefinite, remote preterite), morphomic form properties ('past a'–'past d'), and 1sg masculine agreement.

• recentPast : KFeat
• indefPast : KFeat
• remotePast : KFeat
• pastA : KFeat
• pastB : KFeat
• pastC : KFeat
• pastD : KFeat
• p1 : KFeat
• sg : KFeat
• masc : KFeat

@[implicit_reducible]

instance Stump2016.instDecidableEqKFeat : DecidableEq KFeat

Equations

• Stump2016.instDecidableEqKFeat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2016.instFintypeKFeat : Fintype KFeat

Equations

• Stump2016.instFintypeKFeat = { elems := { val := ↑Stump2016.KFeat.enumList, nodup := Stump2016.KFeat.enumList_nodup }, complete := Stump2016.instFintypeKFeat._proof_1 }

def Stump2016.stemOf : KVerb → String

The stem of each verb.

Equations

• Stump2016.stemOf Stump2016.KVerb.wup = "wup"
• Stump2016.stemOf Stump2016.KVerb.wuph = "wuph"

def Stump2016.pmII (σ : Finset KFeat) : Finset KFeat

Property mapping for Conjugation II ([Stu16] Ch. 8): recent → 'past a', indefinite → 'past b', remote → 'past c'.

Equations

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

def Stump2016.pmIII (σ : Finset KFeat) : Finset KFeat

Property mapping for Conjugation III ([Stu16] Ch. 8): recent → 'past b', indefinite → 'past c', remote → 'past d'. The one-morphome shift from pmII is what makes the two conjugations' preterites interleave.

Equations

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

def Stump2016.formBlock : Morphology.PFM.Block KVerb String (Finset KFeat)

The form paradigm: 1sg masculine exponents for each morphome, read off the stem+suffix segmentation (wupus, wupyōs, wupyās, wuphiyās).

Equations

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

def Stump2016.realizeForm (z : String) (τ : Finset KFeat) : String

Realization of a form cell ⟨Z, τ⟩: the PFM1 paradigm function on the stem Z at the morphomic property set τ.

Equations

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

def Stump2016.linkII : Morphology.Linkage KVerb String (Finset KFeat)

Conjugation II linkage: the single stem, mapped by pmII.

Equations

• Stump2016.linkII = { stems := fun (l : Stump2016.KVerb) (x : Finset Stump2016.KFeat) => {Stump2016.stemOf l}, pm := fun (x : Stump2016.KVerb) => Stump2016.pmII }

def Stump2016.linkIII : Morphology.Linkage KVerb String (Finset KFeat)

Conjugation III linkage: the single stem, mapped by pmIII.

Equations

• Stump2016.linkIII = { stems := fun (l : Stump2016.KVerb) (x : Finset Stump2016.KFeat) => {Stump2016.stemOf l}, pm := fun (x : Stump2016.KVerb) => Stump2016.pmIII }

theorem Stump2016.kashmiri_inflect_alike : Finset.image Prod.snd (linkII.corr KVerb.wup {KFeat.indefPast, KFeat.p1, KFeat.sg, KFeat.masc}) = Finset.image Prod.snd (linkIII.corr KVerb.wuph {KFeat.recentPast, KFeat.p1, KFeat.sg, KFeat.masc})

The morphomic mediation ([Stu16] Ch. 8): WUP's indefinite past and WUPH's recent past have the same form correspondent property set — both 'past b', 1sg masc — even though their tenses differ. This is why they inflect alike (-yōs), the content-to-form mismatch the paradigm-linkage model captures.

theorem Stump2016.kashmiri_inflect_alike_pastC : Finset.image Prod.snd (linkII.corr KVerb.wup {KFeat.remotePast, KFeat.p1, KFeat.sg, KFeat.masc}) = Finset.image Prod.snd (linkIII.corr KVerb.wuph {KFeat.indefPast, KFeat.p1, KFeat.sg, KFeat.masc})

The second interleaving: WUP's remote past and WUPH's indefinite past share the 'past c' correspondent, inflecting alike (-yās).