Stump 2012: canonical paradigm linkage and its deviations

[Stu12]

The paper's four axes of canonical paradigm linkage — totality, stem invariance, injectivity, property preservation, per Morphology/Paradigm/Linkage.lean ([Stu12]) — each anchored by the paper's own witness: a near-canonical baseline and one deviation per axis, plus the two compound cases that show the axes are independent. Content and form paradigms, the correspondence relation, and the deviation typology are the paper's; the forms are transcribed from its numbered tables.

• Breton HERVEZ (Table (2)) — the near-canonical baseline: total, stem-invariant, injective, property-preserving.
• Latin COEPISSE ((17)–(19)) — defectiveness: a present-system stem gap, yet a single stem, so defective without being suppletive.
• Latin BELLUM ((22)–(26)) — syncretism: neuter nominative patterning after the accusative (directional) and a merged dative/ablative cell (nondirectional).
• Latin HORTĀRĪ ((27)–(31), §4) — deponency: active content cells with passive form correspondents, compounded with defectiveness on the passive cells, and a virtual active form cell.
• Hungarian ÉN ((33)–(38)) — functor-argument reversal: a form correspondent's property set computed from the lexeme.
• Latin FERRE ((41)–(43)) — suppletion under the default rule: two stems in complementary distribution, yet property-preserving.
• Old Icelandic ÞURFA ((44)–(46)) — a compound deviation: suppletion and deponent tense mapping in one linkage.

inductive Stump2012.Agr : Type

Person-number agreement, the six cells shared across the Latin verb paradigms.

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

@[implicit_reducible]

instance Stump2012.instDecidableEqAgr : DecidableEq Agr

Equations

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

@[implicit_reducible]

instance Stump2012.instFintypeAgr : Fintype Agr

Equations

• Stump2012.instFintypeAgr = { elems := { val := ↑Stump2012.Agr.enumList, nodup := Stump2012.Agr.enumList_nodup }, complete := Stump2012.instFintypeAgr._proof_1 }

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

Equations

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

@[implicit_reducible]

instance Stump2012.instReprAgr : Repr Agr

Equations

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

inductive Stump2012.System : Type

The Latin tense-system split: present-system versus perfect-system cells.

• pres : System
• perf : System

@[implicit_reducible]

instance Stump2012.instDecidableEqSystem : DecidableEq System

Equations

• Stump2012.instDecidableEqSystem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeSystem : Fintype System

Equations

• Stump2012.instFintypeSystem = { elems := { val := ↑Stump2012.System.enumList, nodup := Stump2012.System.enumList_nodup }, complete := Stump2012.instFintypeSystem._proof_1 }

def Stump2012.instReprSystem.repr : System → ℕ → Std.Format

Equations

• Stump2012.instReprSystem.repr Stump2012.System.pres prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.System.pres")).group prec✝
• Stump2012.instReprSystem.repr Stump2012.System.perf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.System.perf")).group prec✝

@[implicit_reducible]

instance Stump2012.instReprSystem : Repr System

Equations

• Stump2012.instReprSystem = { reprPrec := Stump2012.instReprSystem.repr }

Breton HERVEZ: the near-canonical baseline (Table (2))

inductive Stump2012.HervezLex : Type

The inflecting preposition HERVEZ 'according to'.

• hervez : HervezLex

@[implicit_reducible]

instance Stump2012.instDecidableEqHervezLex : DecidableEq HervezLex

Equations

• Stump2012.instDecidableEqHervezLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeHervezLex : Fintype HervezLex

Equations

• Stump2012.instFintypeHervezLex = { elems := { val := ↑Stump2012.HervezLex.enumList, nodup := Stump2012.HervezLex.enumList_nodup }, complete := Stump2012.instFintypeHervezLex._proof_1 }

def Stump2012.instReprHervezLex.repr : HervezLex → ℕ → Std.Format

Equations

• Stump2012.instReprHervezLex.repr Stump2012.HervezLex.hervez prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.HervezLex.hervez")).group prec✝

@[implicit_reducible]

instance Stump2012.instReprHervezLex : Repr HervezLex

Equations

• Stump2012.instReprHervezLex = { reprPrec := Stump2012.instReprHervezLex.repr }

inductive Stump2012.HervezStem : Type

Its sole stem hervez[Cl.1].

• hervez : HervezStem

@[implicit_reducible]

instance Stump2012.instDecidableEqHervezStem : DecidableEq HervezStem

Equations

• Stump2012.instDecidableEqHervezStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeHervezStem : Fintype HervezStem

Equations

• Stump2012.instFintypeHervezStem = { elems := { val := ↑Stump2012.HervezStem.enumList, nodup := Stump2012.HervezStem.enumList_nodup }, complete := Stump2012.instFintypeHervezStem._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprHervezStem : Repr HervezStem

Equations

• Stump2012.instReprHervezStem = { reprPrec := Stump2012.instReprHervezStem.repr }

def Stump2012.instReprHervezStem.repr : HervezStem → ℕ → Std.Format

Equations

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

def Stump2012.hervezLinkage : Morphology.Linkage HervezLex HervezStem Agr

HERVEZ's linkage: one stem, identity property mapping — the canonical pattern. Its realizations hervezon, hervezout, hervezi, hervezomp, hervezo are based on the single stem with the content cell's own property set.

Equations

• Stump2012.hervezLinkage = Morphology.Linkage.canonical fun (x : Stump2012.HervezLex) => Stump2012.HervezStem.hervez

theorem Stump2012.hervez_isCanonical : hervezLinkage.IsCanonical

HERVEZ is canonical on all four axes ([Stu12] Table (2)).

theorem Stump2012.hervez_not_defective : ¬hervezLinkage.IsDefective

theorem Stump2012.hervez_not_suppletive : ¬hervezLinkage.IsSuppletive

theorem Stump2012.hervez_not_syncretic : ¬hervezLinkage.IsSyncretic

theorem Stump2012.hervez_not_unfaithful : ¬hervezLinkage.IsUnfaithful

Latin COEPISSE: defectiveness ((17)–(19))

The present-system cells lack a stem, so they lack form correspondents and realizations; the perfect-system cells have the stem coep. Defectiveness sits in the stem specification, and COEPISSE keeps a single stem — defective without being suppletive.

inductive Stump2012.CoepLex : Type

• coepisse : CoepLex

@[implicit_reducible]

instance Stump2012.instDecidableEqCoepLex : DecidableEq CoepLex

Equations

• Stump2012.instDecidableEqCoepLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeCoepLex : Fintype CoepLex

Equations

• Stump2012.instFintypeCoepLex = { elems := { val := ↑Stump2012.CoepLex.enumList, nodup := Stump2012.CoepLex.enumList_nodup }, complete := Stump2012.instFintypeCoepLex._proof_1 }

def Stump2012.instReprCoepLex.repr : CoepLex → ℕ → Std.Format

Equations

• Stump2012.instReprCoepLex.repr Stump2012.CoepLex.coepisse prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.CoepLex.coepisse")).group prec✝

@[implicit_reducible]

instance Stump2012.instReprCoepLex : Repr CoepLex

Equations

• Stump2012.instReprCoepLex = { reprPrec := Stump2012.instReprCoepLex.repr }

inductive Stump2012.CoepStem : Type

• coep : CoepStem

@[implicit_reducible]

instance Stump2012.instDecidableEqCoepStem : DecidableEq CoepStem

Equations

• Stump2012.instDecidableEqCoepStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeCoepStem : Fintype CoepStem

Equations

• Stump2012.instFintypeCoepStem = { elems := { val := ↑Stump2012.CoepStem.enumList, nodup := Stump2012.CoepStem.enumList_nodup }, complete := Stump2012.instFintypeCoepStem._proof_1 }

def Stump2012.instReprCoepStem.repr : CoepStem → ℕ → Std.Format

Equations

• Stump2012.instReprCoepStem.repr Stump2012.CoepStem.coep prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.CoepStem.coep")).group prec✝

@[implicit_reducible]

instance Stump2012.instReprCoepStem : Repr CoepStem

Equations

• Stump2012.instReprCoepStem = { reprPrec := Stump2012.instReprCoepStem.repr }

structure Stump2012.CoepCell : Type

A COEPISSE content cell: a tense system and an agreement feature.

• sys : System
• agr : Agr

def Stump2012.instDecidableEqCoepCell.decEq (x✝ x✝¹ : CoepCell) : Decidable (x✝ = x✝¹)

Equations

• Stump2012.instDecidableEqCoepCell.decEq { sys := a, agr := a_1 } { sys := b, agr := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instDecidableEqCoepCell : DecidableEq CoepCell

Equations

• Stump2012.instDecidableEqCoepCell = Stump2012.instDecidableEqCoepCell.decEq

@[implicit_reducible]

instance Stump2012.instFintypeCoepCell : Fintype CoepCell

Equations

• Stump2012.instFintypeCoepCell = Fintype.ofEquiv ((_ : Stump2012.System) × Stump2012.Agr) Stump2012.CoepCell.proxyTypeEquiv

def Stump2012.instReprCoepCell.repr : CoepCell → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Stump2012.instReprCoepCell : Repr CoepCell

Equations

• Stump2012.instReprCoepCell = { reprPrec := Stump2012.instReprCoepCell.repr }

def Stump2012.coepisseLinkage : Morphology.Linkage CoepLex CoepStem CoepCell

COEPISSE's linkage: coep on perfect-system cells, no stem on present-system cells ([Stu12] (18)).

Equations

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

def Stump2012.coepRealize : CoepStem → CoepCell → String

The perfect-system realizations coepī, coepistī, coepit, coepimus, coepistis, coepērunt ([Stu12] (17)).

Equations

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

theorem Stump2012.coepisse_defective : coepisseLinkage.IsDefective

COEPISSE is defective: the present-system cells lack a stem ([Stu12] §3.1).

theorem Stump2012.coepisse_present_no_realization : coepisseLinkage.realize coepRealize CoepLex.coepisse { sys := System.pres, agr := Agr.s3 } = ∅

A present-system content cell has no realization.

theorem Stump2012.coepisse_perfect_realized : coepisseLinkage.realize coepRealize CoepLex.coepisse { sys := System.perf, agr := Agr.s3 } = {("coepit", { sys := System.perf, agr := Agr.s3 })}

A perfect-system content cell realizes through its coep correspondent (coepit, 3sg).

theorem Stump2012.coepisse_stemInvariant : coepisseLinkage.IsStemInvariant

COEPISSE keeps a single stem, so it is stem-invariant.

theorem Stump2012.coepisse_defective_not_suppletive : coepisseLinkage.IsDefective ∧ ¬coepisseLinkage.IsSuppletive

Defectiveness without suppletion: COEPISSE deviates on totality alone ([Stu12] §3.1).

Latin BELLUM: syncretism ((22)–(26))

Two content cells share a form correspondent. The neuter nominative patterns after the accusative (directional), and the dative and ablative share one form cell (nondirectional). The merged dative/ablative form cell is a coarsening of the form-property space; it is modeled here by the dative as its representative, with both content cells mapped there.

inductive Stump2012.BellumLex : Type

• bellum : BellumLex

@[implicit_reducible]

instance Stump2012.instDecidableEqBellumLex : DecidableEq BellumLex

Equations

• Stump2012.instDecidableEqBellumLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeBellumLex : Fintype BellumLex

Equations

• Stump2012.instFintypeBellumLex = { elems := { val := ↑Stump2012.BellumLex.enumList, nodup := Stump2012.BellumLex.enumList_nodup }, complete := Stump2012.instFintypeBellumLex._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprBellumLex : Repr BellumLex

Equations

• Stump2012.instReprBellumLex = { reprPrec := Stump2012.instReprBellumLex.repr }

def Stump2012.instReprBellumLex.repr : BellumLex → ℕ → Std.Format

Equations

• Stump2012.instReprBellumLex.repr Stump2012.BellumLex.bellum prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.BellumLex.bellum")).group prec✝

inductive Stump2012.BellumStem : Type

• bell : BellumStem

@[implicit_reducible]

instance Stump2012.instDecidableEqBellumStem : DecidableEq BellumStem

Equations

• Stump2012.instDecidableEqBellumStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeBellumStem : Fintype BellumStem

Equations

• Stump2012.instFintypeBellumStem = { elems := { val := ↑Stump2012.BellumStem.enumList, nodup := Stump2012.BellumStem.enumList_nodup }, complete := Stump2012.instFintypeBellumStem._proof_1 }

def Stump2012.instReprBellumStem.repr : BellumStem → ℕ → Std.Format

Equations

• Stump2012.instReprBellumStem.repr Stump2012.BellumStem.bell prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.BellumStem.bell")).group prec✝

@[implicit_reducible]

instance Stump2012.instReprBellumStem : Repr BellumStem

Equations

• Stump2012.instReprBellumStem = { reprPrec := Stump2012.instReprBellumStem.repr }

inductive Stump2012.Case : Type

• nom : Case
• gen : Case
• dat : Case
• acc : Case
• abl : Case

@[implicit_reducible]

instance Stump2012.instDecidableEqCase : DecidableEq Case

Equations

• Stump2012.instDecidableEqCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeCase : Fintype Case

Equations

• Stump2012.instFintypeCase = { elems := { val := ↑Stump2012.Case.enumList, nodup := Stump2012.Case.enumList_nodup }, complete := Stump2012.instFintypeCase._proof_1 }

def Stump2012.instReprCase.repr : Case → ℕ → Std.Format

Equations

• Stump2012.instReprCase.repr Stump2012.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Case.nom")).group prec✝
• Stump2012.instReprCase.repr Stump2012.Case.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Case.gen")).group prec✝
• Stump2012.instReprCase.repr Stump2012.Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Case.dat")).group prec✝
• Stump2012.instReprCase.repr Stump2012.Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Case.acc")).group prec✝
• Stump2012.instReprCase.repr Stump2012.Case.abl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Case.abl")).group prec✝

@[implicit_reducible]

instance Stump2012.instReprCase : Repr Case

Equations

• Stump2012.instReprCase = { reprPrec := Stump2012.instReprCase.repr }

inductive Stump2012.Num : Type

• sg : Num
• pl : Num

@[implicit_reducible]

instance Stump2012.instDecidableEqNum : DecidableEq Num

Equations

• Stump2012.instDecidableEqNum x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeNum : Fintype Num

Equations

• Stump2012.instFintypeNum = { elems := { val := ↑Stump2012.Num.enumList, nodup := Stump2012.Num.enumList_nodup }, complete := Stump2012.instFintypeNum._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprNum : Repr Num

Equations

• Stump2012.instReprNum = { reprPrec := Stump2012.instReprNum.repr }

def Stump2012.instReprNum.repr : Num → ℕ → Std.Format

Equations

• Stump2012.instReprNum.repr Stump2012.Num.sg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Num.sg")).group prec✝
• Stump2012.instReprNum.repr Stump2012.Num.pl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Num.pl")).group prec✝

structure Stump2012.BellumCell : Type

A BELLUM content cell: a case and a number.

• case : Case
• num : Num

def Stump2012.instDecidableEqBellumCell.decEq (x✝ x✝¹ : BellumCell) : Decidable (x✝ = x✝¹)

Equations

• Stump2012.instDecidableEqBellumCell.decEq { case := a, num := a_1 } { case := b, num := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instDecidableEqBellumCell : DecidableEq BellumCell

Equations

• Stump2012.instDecidableEqBellumCell = Stump2012.instDecidableEqBellumCell.decEq

@[implicit_reducible]

instance Stump2012.instFintypeBellumCell : Fintype BellumCell

Equations

• Stump2012.instFintypeBellumCell = Fintype.ofEquiv ((_ : Stump2012.Case) × Stump2012.Num) Stump2012.BellumCell.proxyTypeEquiv

@[implicit_reducible]

instance Stump2012.instReprBellumCell : Repr BellumCell

Equations

• Stump2012.instReprBellumCell = { reprPrec := Stump2012.instReprBellumCell.repr }

def Stump2012.instReprBellumCell.repr : BellumCell → ℕ → Std.Format

Equations

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

def Stump2012.bellumPm (σ : BellumCell) : BellumCell

The property mapping: nominative to accusative (directional neuter syncretism, (24)) and ablative to dative as the merged {dat/abl} representative (nondirectional, (25)).

Equations

• Stump2012.bellumPm σ = match σ.case with | Stump2012.Case.nom => { case := Stump2012.Case.acc, num := σ.num } | Stump2012.Case.abl => { case := Stump2012.Case.dat, num := σ.num } | x => σ

def Stump2012.bellumLinkage : Morphology.Linkage BellumLex BellumStem BellumCell

BELLUM's linkage: one stem, the syncretizing property mapping.

Equations

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

def Stump2012.bellRealize : BellumStem → BellumCell → String

The realizations bellum, bellī, bellō, bella, bellōrum, bellīs on the form cells ([Stu12] (22)).

Equations

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

theorem Stump2012.bellum_nom_acc_syncretic : bellumLinkage.IsSyncretic

Directional syncretism: nominative and accusative singular share a form correspondent ([Stu12] (24)).

theorem Stump2012.bellum_dat_abl_syncretic : bellumLinkage.IsSyncretic

Nondirectional syncretism: dative and ablative singular share a form correspondent ([Stu12] (25)).

theorem Stump2012.bellum_nom_acc_realize_eq : bellumLinkage.realize bellRealize BellumLex.bellum { case := Case.nom, num := Num.sg } = bellumLinkage.realize bellRealize BellumLex.bellum { case := Case.acc, num := Num.sg }

The shared form correspondent forces a shared realization: nominative and accusative singular both realize as bellum ([Stu12] (26)).

theorem Stump2012.bellum_nom_realizes_bellum : bellumLinkage.realize bellRealize BellumLex.bellum { case := Case.nom, num := Num.sg } = {("bellum", { case := Case.acc, num := Num.sg })}

theorem Stump2012.bellum_not_injective : ¬bellumLinkage.IsInjective

Syncretism is the failure of injectivity.

Latin HORTĀRĪ: deponency, defectiveness, and virtual cells ((27)–(31), §4)

The active content cells have passive form correspondents (deponency); the passive content cells have none (defectiveness). No content cell corresponds to an active form cell, so an active form cell is virtual — the seat of the [Stu12] §4 point that later Latin hortābat releases by suppressing the deponent override ([Hip10]).

inductive Stump2012.HortariLex : Type

• hortari : HortariLex

@[implicit_reducible]

instance Stump2012.instDecidableEqHortariLex : DecidableEq HortariLex

Equations

• Stump2012.instDecidableEqHortariLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeHortariLex : Fintype HortariLex

Equations

• Stump2012.instFintypeHortariLex = { elems := { val := ↑Stump2012.HortariLex.enumList, nodup := Stump2012.HortariLex.enumList_nodup }, complete := Stump2012.instFintypeHortariLex._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprHortariLex : Repr HortariLex

Equations

• Stump2012.instReprHortariLex = { reprPrec := Stump2012.instReprHortariLex.repr }

def Stump2012.instReprHortariLex.repr : HortariLex → ℕ → Std.Format

Equations

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

inductive Stump2012.HortariStem : Type

• horta : HortariStem

@[implicit_reducible]

instance Stump2012.instDecidableEqHortariStem : DecidableEq HortariStem

Equations

• Stump2012.instDecidableEqHortariStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeHortariStem : Fintype HortariStem

Equations

• Stump2012.instFintypeHortariStem = { elems := { val := ↑Stump2012.HortariStem.enumList, nodup := Stump2012.HortariStem.enumList_nodup }, complete := Stump2012.instFintypeHortariStem._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprHortariStem : Repr HortariStem

Equations

• Stump2012.instReprHortariStem = { reprPrec := Stump2012.instReprHortariStem.repr }

def Stump2012.instReprHortariStem.repr : HortariStem → ℕ → Std.Format

Equations

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

inductive Stump2012.Voice : Type

• active : Voice
• passive : Voice

@[implicit_reducible]

instance Stump2012.instDecidableEqVoice : DecidableEq Voice

Equations

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

@[implicit_reducible]

instance Stump2012.instFintypeVoice : Fintype Voice

Equations

• Stump2012.instFintypeVoice = { elems := { val := ↑Stump2012.Voice.enumList, nodup := Stump2012.Voice.enumList_nodup }, complete := Stump2012.instFintypeVoice._proof_1 }

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

Equations

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

@[implicit_reducible]

instance Stump2012.instReprVoice : Repr Voice

Equations

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

structure Stump2012.VCell : Type

A HORTĀRĪ content cell: a voice and an agreement feature.

• voice : Voice
• agr : Agr

def Stump2012.instDecidableEqVCell.decEq (x✝ x✝¹ : VCell) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Stump2012.instDecidableEqVCell : DecidableEq VCell

Equations

• Stump2012.instDecidableEqVCell = Stump2012.instDecidableEqVCell.decEq

@[implicit_reducible]

instance Stump2012.instFintypeVCell : Fintype VCell

Equations

• Stump2012.instFintypeVCell = Fintype.ofEquiv ((_ : Stump2012.Voice) × Stump2012.Agr) Stump2012.VCell.proxyTypeEquiv

def Stump2012.instReprVCell.repr : VCell → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Stump2012.instReprVCell : Repr VCell

Equations

• Stump2012.instReprVCell = { reprPrec := Stump2012.instReprVCell.repr }

def Stump2012.hortariLinkage : Morphology.Linkage HortariLex HortariStem VCell

HORTĀRĪ's linkage: a stem on the active cells only, and the voice-flipping property mapping ([Stu12] (29)–(30)).

Equations

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

def Stump2012.hoRealize : HortariStem → VCell → String

The passive-morphology realizations of the active content cells (hortor, …, hortantur, (28)).

Equations

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

theorem Stump2012.hortari_unfaithful : hortariLinkage.IsUnfaithful

Deponency: the active content cells' property mapping is unfaithful, flipping to passive ([Stu12] §3.3.1).

theorem Stump2012.hortari_active_realized_by_passive (σ : VCell) : Finset.image (fun (x : HortariStem × VCell) => x.2.voice) (hortariLinkage.corr HortariLex.hortari { voice := Voice.active, agr := σ.agr }) = {Voice.passive}

Every active content cell has a passive form correspondent.

theorem Stump2012.hortari_realizes_hortor : hortariLinkage.realize hoRealize HortariLex.hortari { voice := Voice.active, agr := Agr.s1 } = {("hortor", { voice := Voice.passive, agr := Agr.s1 })}

The active content cell 1sg realizes as hortor through its passive correspondent.

theorem Stump2012.hortari_defective : hortariLinkage.IsDefective

Deponency compounds with defectiveness: the passive content cells lack a stem ([Stu12] (30a)).

theorem Stump2012.hortari_active_form_virtual : hortariLinkage.IsVirtual (HortariStem.horta, { voice := Voice.active, agr := Agr.s1 })

The active form cell ⟨horta, {1sg active}⟩ is virtual: no content cell corresponds to it, since active content maps to passive form and passive content has no correspondent ([Stu12] §4).

Hungarian ÉN: functor-argument reversal ((33)–(38))

The form correspondent of a pronominal oblique-case cell pairs the case stem with the pronoun's own person-number properties — ⟨f(σ), g(L)⟩ with the property set computed from the lexeme ([Stu12] (37)). The inessive of ÉN '1sg' is inflected as the 1sg form of the inessive stem benn.

inductive Stump2012.Pron : Type

The personal pronouns ÉN '1sg' and TE '2sg'.

• en : Pron
• te : Pron

@[implicit_reducible]

instance Stump2012.instDecidableEqPron : DecidableEq Pron

Equations

• Stump2012.instDecidableEqPron x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypePron : Fintype Pron

Equations

• Stump2012.instFintypePron = { elems := { val := ↑Stump2012.Pron.enumList, nodup := Stump2012.Pron.enumList_nodup }, complete := Stump2012.instFintypePron._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprPron : Repr Pron

Equations

• Stump2012.instReprPron = { reprPrec := Stump2012.instReprPron.repr }

def Stump2012.instReprPron.repr : Pron → ℕ → Std.Format

Equations

• Stump2012.instReprPron.repr Stump2012.Pron.en prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Pron.en")).group prec✝
• Stump2012.instReprPron.repr Stump2012.Pron.te prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Pron.te")).group prec✝

inductive Stump2012.HuCase : Type

The oblique cases marked by inflected postpositions.

• dative : HuCase
• inessive : HuCase
• superessive : HuCase

@[implicit_reducible]

instance Stump2012.instDecidableEqHuCase : DecidableEq HuCase

Equations

• Stump2012.instDecidableEqHuCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeHuCase : Fintype HuCase

Equations

• Stump2012.instFintypeHuCase = { elems := { val := ↑Stump2012.HuCase.enumList, nodup := Stump2012.HuCase.enumList_nodup }, complete := Stump2012.instFintypeHuCase._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprHuCase : Repr HuCase

Equations

• Stump2012.instReprHuCase = { reprPrec := Stump2012.instReprHuCase.repr }

def Stump2012.instReprHuCase.repr : HuCase → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Stump2012.instReprHuCase.repr Stump2012.HuCase.dative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.HuCase.dative")).group prec✝
• Stump2012.instReprHuCase.repr Stump2012.HuCase.inessive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.HuCase.inessive")).group prec✝

inductive Stump2012.PersNum : Type

The pronominal person-number properties the form cell carries.

• p1sg : PersNum
• p2sg : PersNum

@[implicit_reducible]

instance Stump2012.instDecidableEqPersNum : DecidableEq PersNum

Equations

• Stump2012.instDecidableEqPersNum x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypePersNum : Fintype PersNum

Equations

• Stump2012.instFintypePersNum = { elems := { val := ↑Stump2012.PersNum.enumList, nodup := Stump2012.PersNum.enumList_nodup }, complete := Stump2012.instFintypePersNum._proof_1 }

def Stump2012.instReprPersNum.repr : PersNum → ℕ → Std.Format

Equations

• Stump2012.instReprPersNum.repr Stump2012.PersNum.p1sg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.PersNum.p1sg")).group prec✝
• Stump2012.instReprPersNum.repr Stump2012.PersNum.p2sg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.PersNum.p2sg")).group prec✝

@[implicit_reducible]

instance Stump2012.instReprPersNum : Repr PersNum

Equations

• Stump2012.instReprPersNum = { reprPrec := Stump2012.instReprPersNum.repr }

inductive Stump2012.HuProp : Type

A Hungarian property set: either a content-side case or a form-side person-number set.

• case (c : HuCase) : HuProp
• agr (pn : PersNum) : HuProp

@[implicit_reducible]

instance Stump2012.instDecidableEqHuProp : DecidableEq HuProp

Equations

• Stump2012.instDecidableEqHuProp = Stump2012.instDecidableEqHuProp.decEq

def Stump2012.instDecidableEqHuProp.decEq (x✝ x✝¹ : HuProp) : Decidable (x✝ = x✝¹)

Equations

• Stump2012.instDecidableEqHuProp.decEq (Stump2012.HuProp.case a) (Stump2012.HuProp.case b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Stump2012.instDecidableEqHuProp.decEq (Stump2012.HuProp.case c) (Stump2012.HuProp.agr pn) = isFalse ⋯
• Stump2012.instDecidableEqHuProp.decEq (Stump2012.HuProp.agr pn) (Stump2012.HuProp.case c) = isFalse ⋯
• Stump2012.instDecidableEqHuProp.decEq (Stump2012.HuProp.agr a) (Stump2012.HuProp.agr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeHuProp : Fintype HuProp

Equations

• Stump2012.instFintypeHuProp = Fintype.ofEquiv (Stump2012.HuCase ⊕ Stump2012.PersNum) Stump2012.HuProp.proxyTypeEquiv

def Stump2012.instReprHuProp.repr : HuProp → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Stump2012.instReprHuProp : Repr HuProp

Equations

• Stump2012.instReprHuProp = { reprPrec := Stump2012.instReprHuProp.repr }

inductive Stump2012.CaseStem : Type

The case postposition stems nek, benn, rajt.

• nek : CaseStem
• benn : CaseStem
• rajt : CaseStem

@[implicit_reducible]

instance Stump2012.instDecidableEqCaseStem : DecidableEq CaseStem

Equations

• Stump2012.instDecidableEqCaseStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeCaseStem : Fintype CaseStem

Equations

• Stump2012.instFintypeCaseStem = { elems := { val := ↑Stump2012.CaseStem.enumList, nodup := Stump2012.CaseStem.enumList_nodup }, complete := Stump2012.instFintypeCaseStem._proof_1 }

def Stump2012.instReprCaseStem.repr : CaseStem → ℕ → Std.Format

Equations

• Stump2012.instReprCaseStem.repr Stump2012.CaseStem.nek prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.CaseStem.nek")).group prec✝
• Stump2012.instReprCaseStem.repr Stump2012.CaseStem.benn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.CaseStem.benn")).group prec✝
• Stump2012.instReprCaseStem.repr Stump2012.CaseStem.rajt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.CaseStem.rajt")).group prec✝

@[implicit_reducible]

instance Stump2012.instReprCaseStem : Repr CaseStem

Equations

• Stump2012.instReprCaseStem = { reprPrec := Stump2012.instReprCaseStem.repr }

def Stump2012.enStems : Pron → HuProp → Finset CaseStem

The stem selection: the case picks the postpositional stem ([Stu12] (37)).

Equations

• Stump2012.enStems x✝ (Stump2012.HuProp.case Stump2012.HuCase.dative) = {Stump2012.CaseStem.nek}
• Stump2012.enStems x✝ (Stump2012.HuProp.case Stump2012.HuCase.inessive) = {Stump2012.CaseStem.benn}
• Stump2012.enStems x✝ (Stump2012.HuProp.case Stump2012.HuCase.superessive) = {Stump2012.CaseStem.rajt}
• Stump2012.enStems x✝¹ x✝ = ∅

def Stump2012.enPm : Pron → HuProp → HuProp

The property mapping computes the form property set from the lexeme — the functor-argument reversal ([Stu12] (32), (37)).

Equations

• Stump2012.enPm Stump2012.Pron.en x✝ = Stump2012.HuProp.agr Stump2012.PersNum.p1sg
• Stump2012.enPm Stump2012.Pron.te x✝ = Stump2012.HuProp.agr Stump2012.PersNum.p2sg

def Stump2012.enLinkage : Morphology.Linkage Pron CaseStem HuProp

ÉN's linkage: case-driven stem, lexeme-driven property mapping.

Equations

• Stump2012.enLinkage = { stems := Stump2012.enStems, pm := Stump2012.enPm }

def Stump2012.enRealize : CaseStem → HuProp → String

The realizations nekem, bennem, rajtam (1sg) and neked, benned, rajtad (2sg) ([Stu12] (36)).

Equations

• Stump2012.enRealize Stump2012.CaseStem.nek (Stump2012.HuProp.agr Stump2012.PersNum.p1sg) = "nekem"
• Stump2012.enRealize Stump2012.CaseStem.nek (Stump2012.HuProp.agr Stump2012.PersNum.p2sg) = "neked"
• Stump2012.enRealize Stump2012.CaseStem.benn (Stump2012.HuProp.agr Stump2012.PersNum.p1sg) = "bennem"
• Stump2012.enRealize Stump2012.CaseStem.benn (Stump2012.HuProp.agr Stump2012.PersNum.p2sg) = "benned"
• Stump2012.enRealize Stump2012.CaseStem.rajt (Stump2012.HuProp.agr Stump2012.PersNum.p1sg) = "rajtam"
• Stump2012.enRealize Stump2012.CaseStem.rajt (Stump2012.HuProp.agr Stump2012.PersNum.p2sg) = "rajtad"
• Stump2012.enRealize x✝¹ x✝ = ""

theorem Stump2012.en_inessive_corr : enLinkage.corr Pron.en (HuProp.case HuCase.inessive) = {(CaseStem.benn, HuProp.agr PersNum.p1sg)}

The inessive of ÉN corresponds to the 1sg form of benn ([Stu12] (38)).

theorem Stump2012.en_functor_argument_reversal : enLinkage.IsUnfaithful

The correspondent's property set is the pronoun's, not the case's — the reversal is unfaithful ([Stu12] (37)).

theorem Stump2012.en_pm_lexeme_sensitive : enLinkage.pm Pron.en (HuProp.case HuCase.inessive) ≠ enLinkage.pm Pron.te (HuProp.case HuCase.inessive)

The property mapping consults the lexeme: ÉN and TE send the same inessive content cell to different form property sets.

theorem Stump2012.en_realizes_nekem_bennem : enLinkage.realize enRealize Pron.en (HuProp.case HuCase.dative) = {("nekem", HuProp.agr PersNum.p1sg)} ∧ enLinkage.realize enRealize Pron.en (HuProp.case HuCase.inessive) = {("bennem", HuProp.agr PersNum.p1sg)}

The nekem/bennem row of (38): the dative and inessive of ÉN realize as nekem and bennem.

Latin FERRE: suppletion under the default rule ((41)–(43))

Present-system cells take the stem fer, perfect-system cells the stem tul, in complementary distribution under the default linkage rule — no override. The linkage is suppletive yet property-preserving, showing the two axes are independent.

inductive Stump2012.FerreLex : Type

• ferre : FerreLex

@[implicit_reducible]

instance Stump2012.instDecidableEqFerreLex : DecidableEq FerreLex

Equations

• Stump2012.instDecidableEqFerreLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeFerreLex : Fintype FerreLex

Equations

• Stump2012.instFintypeFerreLex = { elems := { val := ↑Stump2012.FerreLex.enumList, nodup := Stump2012.FerreLex.enumList_nodup }, complete := Stump2012.instFintypeFerreLex._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprFerreLex : Repr FerreLex

Equations

• Stump2012.instReprFerreLex = { reprPrec := Stump2012.instReprFerreLex.repr }

def Stump2012.instReprFerreLex.repr : FerreLex → ℕ → Std.Format

Equations

• Stump2012.instReprFerreLex.repr Stump2012.FerreLex.ferre prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.FerreLex.ferre")).group prec✝

inductive Stump2012.FerreStem : Type

• fer : FerreStem
• tul : FerreStem

@[implicit_reducible]

instance Stump2012.instDecidableEqFerreStem : DecidableEq FerreStem

Equations

• Stump2012.instDecidableEqFerreStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeFerreStem : Fintype FerreStem

Equations

• Stump2012.instFintypeFerreStem = { elems := { val := ↑Stump2012.FerreStem.enumList, nodup := Stump2012.FerreStem.enumList_nodup }, complete := Stump2012.instFintypeFerreStem._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprFerreStem : Repr FerreStem

Equations

• Stump2012.instReprFerreStem = { reprPrec := Stump2012.instReprFerreStem.repr }

def Stump2012.instReprFerreStem.repr : FerreStem → ℕ → Std.Format

Equations

• Stump2012.instReprFerreStem.repr Stump2012.FerreStem.fer prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.FerreStem.fer")).group prec✝
• Stump2012.instReprFerreStem.repr Stump2012.FerreStem.tul prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.FerreStem.tul")).group prec✝

structure Stump2012.FerreCell : Type

A FERRE content cell: a tense system and an agreement feature.

• sys : System
• agr : Agr

@[implicit_reducible]

instance Stump2012.instDecidableEqFerreCell : DecidableEq FerreCell

Equations

• Stump2012.instDecidableEqFerreCell = Stump2012.instDecidableEqFerreCell.decEq

def Stump2012.instDecidableEqFerreCell.decEq (x✝ x✝¹ : FerreCell) : Decidable (x✝ = x✝¹)

Equations

• Stump2012.instDecidableEqFerreCell.decEq { sys := a, agr := a_1 } { sys := b, agr := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeFerreCell : Fintype FerreCell

Equations

• Stump2012.instFintypeFerreCell = Fintype.ofEquiv ((_ : Stump2012.System) × Stump2012.Agr) Stump2012.FerreCell.proxyTypeEquiv

@[implicit_reducible]

instance Stump2012.instReprFerreCell : Repr FerreCell

Equations

• Stump2012.instReprFerreCell = { reprPrec := Stump2012.instReprFerreCell.repr }

def Stump2012.instReprFerreCell.repr : FerreCell → ℕ → Std.Format

Equations

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

def Stump2012.ferreLinkage : Morphology.Linkage FerreLex FerreStem FerreCell

FERRE's linkage: two suppletive stems in complementary distribution, identity property mapping ([Stu12] (42)).

Equations

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

def Stump2012.ferRealize : FerreStem → FerreCell → String

The realizations ferō, fers, fert, … and tulī, …, tulit, … ([Stu12] (41)).

Equations

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

theorem Stump2012.ferre_suppletive : ferreLinkage.IsSuppletive

FERRE is suppletive: the present- and perfect-system cells draw on different stems ([Stu12] §3.4).

theorem Stump2012.ferre_propertyPreserving : ferreLinkage.IsPropertyPreserving

FERRE is property-preserving: no override, the default rule preserves the content cell's property set.

theorem Stump2012.ferre_suppletive_yet_faithful : ferreLinkage.IsSuppletive ∧ ferreLinkage.IsPropertyPreserving

The independence showcase: suppletive yet property-preserving ([Stu12] §3.4).

theorem Stump2012.ferre_present_realized : ferreLinkage.realize ferRealize FerreLex.ferre { sys := System.pres, agr := Agr.s3 } = {("fert", { sys := System.pres, agr := Agr.s3 })}

theorem Stump2012.ferre_perfect_realized : ferreLinkage.realize ferRealize FerreLex.ferre { sys := System.perf, agr := Agr.s3 } = {("tulit", { sys := System.perf, agr := Agr.s3 })}

Old Icelandic ÞURFA: a compound deviation ((44)–(46))

A preterite-present verb forms its present as a strong verb forms its past (deponent tense mapping) and its past with a separate weak stem (suppletion). Suppletion and unfaithfulness coincide in a single linkage.

inductive Stump2012.ThurfaLex : Type

• thurfa : ThurfaLex

@[implicit_reducible]

instance Stump2012.instDecidableEqThurfaLex : DecidableEq ThurfaLex

Equations

• Stump2012.instDecidableEqThurfaLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeThurfaLex : Fintype ThurfaLex

Equations

• Stump2012.instFintypeThurfaLex = { elems := { val := ↑Stump2012.ThurfaLex.enumList, nodup := Stump2012.ThurfaLex.enumList_nodup }, complete := Stump2012.instFintypeThurfaLex._proof_1 }

def Stump2012.instReprThurfaLex.repr : ThurfaLex → ℕ → Std.Format

Equations

• Stump2012.instReprThurfaLex.repr Stump2012.ThurfaLex.thurfa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.ThurfaLex.thurfa")).group prec✝

@[implicit_reducible]

instance Stump2012.instReprThurfaLex : Repr ThurfaLex

Equations

• Stump2012.instReprThurfaLex = { reprPrec := Stump2012.instReprThurfaLex.repr }

inductive Stump2012.ThurfaStem : Type

• strong : ThurfaStem
• weak : ThurfaStem

@[implicit_reducible]

instance Stump2012.instDecidableEqThurfaStem : DecidableEq ThurfaStem

Equations

• Stump2012.instDecidableEqThurfaStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeThurfaStem : Fintype ThurfaStem

Equations

• Stump2012.instFintypeThurfaStem = { elems := { val := ↑Stump2012.ThurfaStem.enumList, nodup := Stump2012.ThurfaStem.enumList_nodup }, complete := Stump2012.instFintypeThurfaStem._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprThurfaStem : Repr ThurfaStem

Equations

• Stump2012.instReprThurfaStem = { reprPrec := Stump2012.instReprThurfaStem.repr }

def Stump2012.instReprThurfaStem.repr : ThurfaStem → ℕ → Std.Format

Equations

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

inductive Stump2012.Tense : Type

• pres : Tense
• past : Tense

@[implicit_reducible]

instance Stump2012.instDecidableEqTense : DecidableEq Tense

Equations

• Stump2012.instDecidableEqTense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instFintypeTense : Fintype Tense

Equations

• Stump2012.instFintypeTense = { elems := { val := ↑Stump2012.Tense.enumList, nodup := Stump2012.Tense.enumList_nodup }, complete := Stump2012.instFintypeTense._proof_1 }

@[implicit_reducible]

instance Stump2012.instReprTense : Repr Tense

Equations

• Stump2012.instReprTense = { reprPrec := Stump2012.instReprTense.repr }

def Stump2012.instReprTense.repr : Tense → ℕ → Std.Format

Equations

• Stump2012.instReprTense.repr Stump2012.Tense.pres prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Tense.pres")).group prec✝
• Stump2012.instReprTense.repr Stump2012.Tense.past prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.Tense.past")).group prec✝

structure Stump2012.TCell : Type

A ÞURFA content cell: a tense and an agreement feature.

• tense : Tense
• agr : Agr

def Stump2012.instDecidableEqTCell.decEq (x✝ x✝¹ : TCell) : Decidable (x✝ = x✝¹)

Equations

• Stump2012.instDecidableEqTCell.decEq { tense := a, agr := a_1 } { tense := b, agr := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stump2012.instDecidableEqTCell : DecidableEq TCell

Equations

• Stump2012.instDecidableEqTCell = Stump2012.instDecidableEqTCell.decEq

@[implicit_reducible]

instance Stump2012.instFintypeTCell : Fintype TCell

Equations

• Stump2012.instFintypeTCell = Fintype.ofEquiv ((_ : Stump2012.Tense) × Stump2012.Agr) Stump2012.TCell.proxyTypeEquiv

def Stump2012.instReprTCell.repr : TCell → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Stump2012.instReprTCell : Repr TCell

Equations

• Stump2012.instReprTCell = { reprPrec := Stump2012.instReprTCell.repr }

def Stump2012.thurfaLinkage : Morphology.Linkage ThurfaLex ThurfaStem TCell

ÞURFA's linkage: the strong stem for the present, the weak stem for the past (suppletion), and a property mapping sending every cell to the past (deponent tense) ([Stu12] (45)–(46)).

Equations

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

theorem Stump2012.thurfa_suppletive : thurfaLinkage.IsSuppletive

ÞURFA is suppletive: present and past draw on different stems.

theorem Stump2012.thurfa_unfaithful : thurfaLinkage.IsUnfaithful

ÞURFA is unfaithful: the present content cell maps to a past form cell.

theorem Stump2012.thurfa_suppletive_and_unfaithful : thurfaLinkage.IsSuppletive ∧ thurfaLinkage.IsUnfaithful

The compound deviation: suppletion and deponent tense mapping in one linkage ([Stu12] §3.4).

theorem Stump2012.thurfa_pres_corr : thurfaLinkage.corr ThurfaLex.thurfa { tense := Tense.pres, agr := Agr.s1 } = {(ThurfaStem.strong, { tense := Tense.past, agr := Agr.s1 })}

The present content cell's form correspondent is the strong stem at the past property set ([Stu12] (46)).

theorem Stump2012.thurfa_past_corr : thurfaLinkage.corr ThurfaLex.thurfa { tense := Tense.past, agr := Agr.s1 } = {(ThurfaStem.weak, { tense := Tense.past, agr := Agr.s1 })}

The past content cell's form correspondent is the weak stem at the past property set ([Stu12] (46)).