Stump (2012): The Formal and Functional Architecture of Inflectional Morphology

This file formalizes [Stu12]'s architecture of inflection, in which a lexeme's content paradigm is linked to the form paradigms of its stems, and its account of noncanonical inflection as deviation from canonical paradigm linkage. Canonical linkage is total, univalent, stem-invariant, injective and property-preserving, the five axes of the substrate's Morphology.Linkage.IsCanonical, and the Breton inflecting preposition HERVEZ is the paper's canonical witness (hervez_isCanonical). Each noncanonical phenomenon deviates on one axis: Latin COEPISSE lacks present-system stems and is defective without being suppletive (coepisse_defective_not_suppletive), Latin BELLUM shares form correspondents between the nominative and the accusative and between the dative and the ablative, the directional and nondirectional syncretisms of the paper's rules (24) and (25) (bellum_nom_acc_syncretic, bellum_nom_acc_realize_eq), deponent HORTĀRĪ has passive form correspondents for its active content cells and none for its passive ones (hortari_unfaithful, hortari_defective, hortari_active_form_virtual), the Hungarian pronoun ÉN takes its oblique-case forms from case stems inflected for the pronoun's own person and number, the functor-argument reversal of rule (37) (en_functor_argument_reversal, en_pm_lexeme_sensitive), and Latin FERRE has two stems in complementary distribution under the default rule alone, suppletive yet property-preserving (ferre_suppletive_yet_faithful). The deviations compound: Old Icelandic ÞURFA forms its present as a strong verb forms its past and its past on a weak stem, deponent and suppletive at once (thurfa_suppletive_and_unfaithful).

The forms of the paper's examples are read from the forms data (attested). Where the paper's realization follows from a stem and an ending, the ending is read off an exemplar: COEPISSE's perfect endings are FERRE's (coepisse_perfect_realized), and HORTĀRĪ's passive endings are LAUDĀRE's, which realize the deponent's active content cells (hortari_realizes_hortor, depon_vs_regular).

Implementation notes

The Breton, Latin and Old Icelandic linkages give content and form cells one type of property sets, identified by id; the Hungarian pronouns' content cells carry cases and their form cells person-number sets, a case being identified with the form property set HuProp.case. The merged dative/ablative form cell of rule (25) is represented by the dative, with both content cells mapped there. Deponent HORTĀRĪ's stem is taken as the segments before the personal ending, as is LAUDĀRE's, so that the endings are shared. The Hungarian pronoun's direct-case forms and the full Old Icelandic paradigm of (44) are not represented; the paper's discussion of the later Latin active hortābat as an exploratory expression is described only in the docstring of the virtual form cell.

References

• [Stu12]
• [Hip10]

def Stump2012.attested (pid : String) (c : Forms.Cell) : List String

attested pid c is the segmentation of the first attested form with parameter pid in the cell c, or the empty list when there is none.

Equations

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

inductive Stump2012.Agr : Type

Agr lists the six person-number agreement values that the Latin verb paradigms share.

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

@[instance_reducible]

instance Stump2012.instDecidableEqAgr : DecidableEq Agr

Equations

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

@[instance_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✝

@[instance_reducible]

instance Stump2012.instReprAgr : Repr Agr

Equations

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

def Stump2012.Agr.person : Agr → UD.Person

The person of an agreement value.

Equations

• Stump2012.Agr.s1.person = UD.Person.first
• Stump2012.Agr.p1.person = UD.Person.first
• Stump2012.Agr.s2.person = UD.Person.second
• Stump2012.Agr.p2.person = UD.Person.second
• Stump2012.Agr.s3.person = UD.Person.third
• Stump2012.Agr.p3.person = UD.Person.third

def Stump2012.Agr.number : Agr → UD.Number

The number of an agreement value.

Equations

• Stump2012.Agr.s1.number = UD.Number.Sing
• Stump2012.Agr.s2.number = UD.Number.Sing
• Stump2012.Agr.s3.number = UD.Number.Sing
• Stump2012.Agr.p1.number = UD.Number.Plur
• Stump2012.Agr.p2.number = UD.Number.Plur
• Stump2012.Agr.p3.number = UD.Number.Plur

def Stump2012.Agr.cell (a : Agr) (c : Forms.Cell := { }) : Forms.Cell

a.cell c is the cell c with the person and number of the agreement value a.

Equations

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

inductive Stump2012.System : Type

System splits the Latin verb cells into present-system and perfect-system cells.

• pres : System
• perf : System

@[instance_reducible]

instance Stump2012.instDecidableEqSystem : DecidableEq System

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeSystem : Fintype System

Equations

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

@[instance_reducible]

instance Stump2012.instReprSystem : Repr System

Equations

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

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✝

Breton HERVEZ: the canonical baseline

inductive Stump2012.HervezLex : Type

HervezLex has the single lexeme HERVEZ 'according to', an inflecting preposition.

• hervez : HervezLex

@[instance_reducible]

instance Stump2012.instDecidableEqHervezLex : DecidableEq HervezLex

Equations

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

@[instance_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✝

@[instance_reducible]

instance Stump2012.instReprHervezLex : Repr HervezLex

Equations

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

inductive Stump2012.HervezStem : Type

HERVEZ has a single stem.

• hervez : HervezStem

@[instance_reducible]

instance Stump2012.instDecidableEqHervezStem : DecidableEq HervezStem

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeHervezStem : Fintype HervezStem

Equations

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

@[instance_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 Agr

HERVEZ's linkage has one stem and the identity property mapping, the canonical pattern of the paper's (14).

Equations

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

theorem Stump2012.hervez_isCanonical : hervezLinkage.IsCanonical id

HERVEZ is canonical on all five axes.

Latin COEPISSE: defectiveness

inductive Stump2012.CoepLex : Type

• coepisse : CoepLex

@[instance_reducible]

instance Stump2012.instDecidableEqCoepLex : DecidableEq CoepLex

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeCoepLex : Fintype CoepLex

Equations

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

@[instance_reducible]

instance Stump2012.instReprCoepLex : Repr CoepLex

Equations

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

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✝

inductive Stump2012.CoepStem : Type

• coep : CoepStem

@[instance_reducible]

instance Stump2012.instDecidableEqCoepStem : DecidableEq CoepStem

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeCoepStem : Fintype CoepStem

Equations

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

@[instance_reducible]

instance Stump2012.instReprCoepStem : Repr CoepStem

Equations

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

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✝

structure Stump2012.SysCell : Type

A Latin verb content cell pairs a tense system with an agreement feature.

• sys : System
• agr : Agr

@[instance_reducible]

instance Stump2012.instDecidableEqSysCell : DecidableEq SysCell

Equations

• Stump2012.instDecidableEqSysCell = Stump2012.instDecidableEqSysCell.decEq

def Stump2012.instDecidableEqSysCell.decEq (x✝ x✝¹ : SysCell) : Decidable (x✝ = x✝¹)

Equations

• Stump2012.instDecidableEqSysCell.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 ⋯

@[instance_reducible]

instance Stump2012.instReprSysCell : Repr SysCell

Equations

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

def Stump2012.instReprSysCell.repr : SysCell → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeSysCell : Fintype SysCell

Equations

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

def Stump2012.coepisseLinkage : Morphology.Linkage CoepLex CoepStem SysCell SysCell

COEPISSE's linkage follows the stem specification (18), which gives the perfect-system cells the stem coep and the present-system cells no stem.

Equations

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

def Stump2012.perfEnding (a : Agr) : List String

perfEnding a is the perfect ending for the agreement a, read off FERRE's perfect form of (41) after its stem tul.

Equations

• Stump2012.perfEnding a = List.drop 3 (Stump2012.attested "carry" (a.cell { system := ↑Stump2012.Forms.System.perf }))

def Stump2012.coepRealize : CoepStem → SysCell → List String

A form cell of coep realizes as the stem followed by the perfect ending.

Equations

• Stump2012.coepRealize x✝¹ x✝ = ["c", "o", "e", "p"] ++ Stump2012.perfEnding x✝.agr

theorem Stump2012.coepisse_defective : coepisseLinkage.IsDefective

COEPISSE is defective because its present-system cells lack a stem.

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

The third singular present-system content cell has no realization.

theorem Stump2012.coepisse_perfect_realized (a : Agr) : coepisseLinkage.realized coepRealize CoepLex.coepisse { sys := System.perf, agr := a } = {(attested "begin" (a.cell { system := ↑Forms.System.perf }), { sys := System.perf, agr := a })}

Every perfect-system content cell realizes through its coep correspondent as the paper's (17) lists, with FERRE's perfect endings.

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 CoepLex.coepisse

COEPISSE is defective without being suppletive, deviating on totality but not on stem invariance.

Latin BELLUM: syncretism

inductive Stump2012.BellumLex : Type

• bellum : BellumLex

@[instance_reducible]

instance Stump2012.instDecidableEqBellumLex : DecidableEq BellumLex

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeBellumLex : Fintype BellumLex

Equations

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

@[instance_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

@[instance_reducible]

instance Stump2012.instDecidableEqBellumStem : DecidableEq BellumStem

Equations

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

@[instance_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✝

@[instance_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

@[instance_reducible]

instance Stump2012.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_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✝

@[instance_reducible]

instance Stump2012.instReprCase : Repr Case

Equations

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

def Stump2012.Case.ud : Case → UD.Case

c.ud is the case c in the forms data.

Equations

• Stump2012.Case.nom.ud = UD.Case.Nom
• Stump2012.Case.gen.ud = UD.Case.Gen
• Stump2012.Case.dat.ud = UD.Case.Dat
• Stump2012.Case.acc.ud = UD.Case.Acc
• Stump2012.Case.abl.ud = UD.Case.Abl

inductive Stump2012.Num : Type

• sg : Num
• pl : Num

@[instance_reducible]

instance Stump2012.instDecidableEqNum : DecidableEq Num

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeNum : Fintype Num

Equations

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

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✝

@[instance_reducible]

instance Stump2012.instReprNum : Repr Num

Equations

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

def Stump2012.Num.ud : Num → UD.Number

n.ud is the number n in the forms data.

Equations

• Stump2012.Num.sg.ud = UD.Number.Sing
• Stump2012.Num.pl.ud = UD.Number.Plur

structure Stump2012.BellumCell : Type

A BELLUM content cell pairs a case with a number.

• case : Case
• num : Num

@[instance_reducible]

instance Stump2012.instDecidableEqBellumCell : DecidableEq BellumCell

Equations

• Stump2012.instDecidableEqBellumCell = Stump2012.instDecidableEqBellumCell.decEq

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 ⋯

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

Equations

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

@[instance_reducible]

instance Stump2012.instReprBellumCell : Repr BellumCell

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeBellumCell : Fintype BellumCell

Equations

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

def Stump2012.bellumPm (σ : BellumCell) : BellumCell

The property mapping sends the nominative to the accusative, the directional neuter syncretism of rule (24), and the ablative to the dative, which represents the merged dative/ablative cell of rule (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 BellumCell

BELLUM's linkage has one stem and the syncretizing property mapping.

Equations

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

def Stump2012.bellRealize : BellumStem → BellumCell → List String

bellRealize reads the realization of each form cell of bell off the attested forms, the paper's (22).

Equations

• Stump2012.bellRealize x✝¹ x✝ = Stump2012.attested "war" { number := ↑x✝.num.ud, case_ := ↑x✝.case.ud }

theorem Stump2012.bellum_nom_acc_syncretic : bellumLinkage.IsSyncretic

The nominative and accusative singular share a form correspondent, a directional syncretism.

theorem Stump2012.bellum_dat_abl_syncretic : bellumLinkage.IsSyncretic

The dative and ablative singular share a form correspondent, a nondirectional syncretism.

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

The nominative and accusative singular have the same realization because they share a form correspondent, the paper's (26).

theorem Stump2012.bellum_nom_realizes_acc : bellumLinkage.realized bellRealize BellumLex.bellum { case := Case.nom, num := Num.sg } = {(attested "war" { number := ↑UD.Number.Sing, case_ := ↑UD.Case.Acc }, { case := Case.acc, num := Num.sg })}

The nominative singular realizes through the accusative form cell.

theorem Stump2012.bellum_not_injective : ¬bellumLinkage.IsInjective

BELLUM's linkage is not injective, since syncretism is a failure of injectivity.

Latin HORTĀRĪ: deponency, defectiveness and virtual cells

inductive Stump2012.LatinVerb : Type

• hortari : LatinVerb
• laudare : LatinVerb

@[instance_reducible]

instance Stump2012.instDecidableEqLatinVerb : DecidableEq LatinVerb

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeLatinVerb : Fintype LatinVerb

Equations

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

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

Equations

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

@[instance_reducible]

instance Stump2012.instReprLatinVerb : Repr LatinVerb

Equations

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

inductive Stump2012.VerbStem : Type

• hort : VerbStem
• laud : VerbStem

@[instance_reducible]

instance Stump2012.instDecidableEqVerbStem : DecidableEq VerbStem

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeVerbStem : Fintype VerbStem

Equations

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

def Stump2012.instReprVerbStem.repr : VerbStem → ℕ → Std.Format

Equations

• Stump2012.instReprVerbStem.repr Stump2012.VerbStem.hort prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.VerbStem.hort")).group prec✝
• Stump2012.instReprVerbStem.repr Stump2012.VerbStem.laud prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2012.VerbStem.laud")).group prec✝

@[instance_reducible]

instance Stump2012.instReprVerbStem : Repr VerbStem

Equations

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

inductive Stump2012.Voice : Type

• active : Voice
• passive : Voice

@[instance_reducible]

instance Stump2012.instDecidableEqVoice : DecidableEq Voice

Equations

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

@[instance_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✝

@[instance_reducible]

instance Stump2012.instReprVoice : Repr Voice

Equations

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

def Stump2012.Voice.ud : Voice → UD.Voice

v.ud is the voice v in the forms data.

Equations

• Stump2012.Voice.active.ud = UD.Voice.Act
• Stump2012.Voice.passive.ud = UD.Voice.Pass

structure Stump2012.VCell : Type

A finite content cell pairs a voice with an agreement feature.

• voice : Voice
• agr : Agr

@[instance_reducible]

instance Stump2012.instDecidableEqVCell : DecidableEq VCell

Equations

• Stump2012.instDecidableEqVCell = Stump2012.instDecidableEqVCell.decEq

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 ⋯

@[instance_reducible]

instance Stump2012.instReprVCell : Repr VCell

Equations

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

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

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeVCell : Fintype VCell

Equations

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

def Stump2012.latinLinkage : Morphology.Linkage LatinVerb VerbStem VCell VCell

In the linkage of the two verbs, deponent HORTĀRĪ has a stem on its active cells only and the voice-flipping property mapping of rule (29), the stem specification (30a), while regular LAUDĀRE is canonical, (30b).

Equations

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

def Stump2012.personalEnding (v : Voice) (a : Agr) : List String

personalEnding v a is the personal ending for the voice v and the agreement a, read off LAUDĀRE's forms of (28) after its stem.

Equations

• Stump2012.personalEnding v a = List.drop 4 (Stump2012.attested "praise" (a.cell { voice := ↑v.ud }))

def Stump2012.verbRealize : VerbStem → VCell → List String

A form cell realizes as its stem followed by the ending of the form cell's voice.

Equations

• Stump2012.verbRealize Stump2012.VerbStem.hort x✝ = ["h", "o", "r", "t"] ++ Stump2012.personalEnding x✝.voice x✝.agr
• Stump2012.verbRealize Stump2012.VerbStem.laud x✝ = ["l", "a", "u", "d"] ++ Stump2012.personalEnding x✝.voice x✝.agr

theorem Stump2012.hortari_unfaithful : latinLinkage.IsUnfaithful id

HORTĀRĪ's deponency makes the linkage unfaithful, since the property mapping flips its active content cells to passive.

theorem Stump2012.hortari_active_realized_by_passive (a : Agr) : Finset.image (fun (x : VerbStem × VCell) => x.2.voice) (latinLinkage.corr LatinVerb.hortari { voice := Voice.active, agr := a }) = {Voice.passive}

Every active content cell of HORTĀRĪ has a passive form correspondent.

theorem Stump2012.hortari_realizes_hortor (a : Agr) : latinLinkage.realized verbRealize LatinVerb.hortari { voice := Voice.active, agr := a } = {(attested "urge" (a.cell { voice := ↑UD.Voice.Pass }), { voice := Voice.passive, agr := a })}

The active content cells of HORTĀRĪ realize with LAUDĀRE's passive endings, as the paper's (28) lists.

theorem Stump2012.depon_vs_regular (a : Agr) : latinLinkage.realized verbRealize LatinVerb.laudare { voice := Voice.active, agr := a } = {(attested "praise" (a.cell { voice := ↑UD.Voice.Act }), { voice := Voice.active, agr := a })} ∧ latinLinkage.realized verbRealize LatinVerb.hortari { voice := Voice.active, agr := a } = {(attested "urge" (a.cell { voice := ↑UD.Voice.Pass }), { voice := Voice.passive, agr := a })}

On the same active content cell, LAUDĀRE realizes through an active form cell and HORTĀRĪ through a passive one.

theorem Stump2012.hortari_defective : latinLinkage.IsDefective

Deponency compounds with defectiveness, since the passive content cells of HORTĀRĪ lack a stem.

theorem Stump2012.hortari_active_form_virtual : latinLinkage.IsVirtual (VerbStem.hort, { voice := Voice.active, agr := Agr.s1 })

The first singular active form cell of hort is virtual. No content cell corresponds to it, since active content maps to passive form and passive content has no correspondent. The later Latin active hortābat, as [Hip10] describes, releases it.

Hungarian ÉN: functor-argument reversal

inductive Stump2012.Pron : Type

Pron has the personal pronouns ÉN '1sg' and TE '2sg'.

• en : Pron
• te : Pron

@[instance_reducible]

instance Stump2012.instDecidableEqPron : DecidableEq Pron

Equations

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

@[instance_reducible]

instance Stump2012.instFintypePron : Fintype Pron

Equations

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

@[instance_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

HuCase lists the oblique cases of (38) represented here.

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

@[instance_reducible]

instance Stump2012.instDecidableEqHuCase : DecidableEq HuCase

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeHuCase : Fintype HuCase

Equations

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

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✝

@[instance_reducible]

instance Stump2012.instReprHuCase : Repr HuCase

Equations

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

inductive Stump2012.PersNum : Type

PersNum lists the pronominal person-number properties that a form cell carries.

• p1sg : PersNum
• p2sg : PersNum

@[instance_reducible]

instance Stump2012.instDecidableEqPersNum : DecidableEq PersNum

Equations

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

@[instance_reducible]

instance Stump2012.instFintypePersNum : Fintype PersNum

Equations

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

@[instance_reducible]

instance Stump2012.instReprPersNum : Repr PersNum

Equations

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

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✝

def Stump2012.PersNum.cell : PersNum → Forms.Cell

pn.cell is the cell of the person-number property pn in the forms data.

Equations

• Stump2012.PersNum.p1sg.cell = { number := ↑UD.Number.Sing, person := ↑UD.Person.first }
• Stump2012.PersNum.p2sg.cell = { number := ↑UD.Number.Sing, person := ↑UD.Person.second }

inductive Stump2012.HuProp : Type

A form property set of a Hungarian case stem is a case, the property set that a faithful correspondent of a case content cell would carry, or a person-number set.

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

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 ⋯

@[instance_reducible]

instance Stump2012.instDecidableEqHuProp : DecidableEq HuProp

Equations

• Stump2012.instDecidableEqHuProp = Stump2012.instDecidableEqHuProp.decEq

@[instance_reducible]

instance Stump2012.instFintypeHuProp : Fintype HuProp

Equations

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

@[instance_reducible]

instance Stump2012.instReprHuProp : Repr HuProp

Equations

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

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

Equations

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

inductive Stump2012.CaseStem : Type

CaseStem lists the case postposition stems nek, benn and rajt.

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

@[instance_reducible]

instance Stump2012.instDecidableEqCaseStem : DecidableEq CaseStem

Equations

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

@[instance_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✝

@[instance_reducible]

instance Stump2012.instReprCaseStem : Repr CaseStem

Equations

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

def Stump2012.CaseStem.pid : CaseStem → String

Equations

• Stump2012.CaseStem.nek.pid = "nek"
• Stump2012.CaseStem.benn.pid = "benn"
• Stump2012.CaseStem.rajt.pid = "rajt"

def Stump2012.enStems : Pron → HuCase → Finset CaseStem

In the stem selection of rule (37), the case picks the postpositional stem.

Equations

• Stump2012.enStems x✝ Stump2012.HuCase.dative = {Stump2012.CaseStem.nek}
• Stump2012.enStems x✝ Stump2012.HuCase.inessive = {Stump2012.CaseStem.benn}
• Stump2012.enStems x✝ Stump2012.HuCase.superessive = {Stump2012.CaseStem.rajt}

def Stump2012.enPm : Pron → HuCase → HuProp

The property mapping computes the form property set from the lexeme, the functor-argument reversal of (32) and (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 HuCase HuProp

The pronouns' linkage selects the stem by case and the form property set by lexeme; its content cells carry cases and its form cells person-number sets.

Equations

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

def Stump2012.enRealize : CaseStem → HuProp → List String

A person-number form cell of a case stem realizes as the inflected postposition of (36).

Equations

• Stump2012.enRealize x✝ (Stump2012.HuProp.agr pn) = Stump2012.attested x✝.pid pn.cell
• Stump2012.enRealize x✝¹ x✝ = []

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

The inessive of ÉN corresponds to the 1sg form cell of benn, the paper's (38).

theorem Stump2012.en_isTotal : enLinkage.IsTotal

Every oblique case content cell has the case's postpositional stem, so the pronouns' linkage is total.

theorem Stump2012.en_functor_argument_reversal : enLinkage.IsUnfaithful HuProp.case

The reversal is unfaithful, since the correspondent's property set is the pronoun's, not the case's.

theorem Stump2012.en_pm_lexeme_sensitive : enLinkage.pm Pron.en HuCase.inessive ≠ enLinkage.pm Pron.te HuCase.inessive

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

theorem Stump2012.inessive_realizes : enLinkage.realized enRealize Pron.en HuCase.inessive = {(attested "benn" PersNum.p1sg.cell, HuProp.agr PersNum.p1sg)} ∧ enLinkage.realized enRealize Pron.te HuCase.inessive = {(attested "benn" PersNum.p2sg.cell, HuProp.agr PersNum.p2sg)}

The inessive of ÉN and of TE realize as the first and second person forms of benn.

Latin FERRE: suppletion under the default rule

inductive Stump2012.FerreLex : Type

• ferre : FerreLex

@[instance_reducible]

instance Stump2012.instDecidableEqFerreLex : DecidableEq FerreLex

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeFerreLex : Fintype FerreLex

Equations

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

@[instance_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

@[instance_reducible]

instance Stump2012.instDecidableEqFerreStem : DecidableEq FerreStem

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeFerreStem : Fintype FerreStem

Equations

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

@[instance_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✝

def Stump2012.ferreLinkage : Morphology.Linkage FerreLex FerreStem SysCell SysCell

In FERRE's linkage, the stem specification (42) gives two suppletive stems in complementary distribution, and the default rule supplies the identity property mapping.

Equations

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

theorem Stump2012.ferre_suppletive : ferreLinkage.IsSuppletive FerreLex.ferre

FERRE is suppletive because its present- and perfect-system cells draw on different stems.

theorem Stump2012.ferre_propertyPreserving : ferreLinkage.IsPropertyPreserving id

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

theorem Stump2012.ferre_suppletive_yet_faithful : ferreLinkage.IsSuppletive FerreLex.ferre ∧ ferreLinkage.IsPropertyPreserving id

FERRE is suppletive yet property-preserving, so the two axes are independent.

Old Icelandic ÞURFA: a compound deviation

inductive Stump2012.ThurfaLex : Type

• thurfa : ThurfaLex

@[instance_reducible]

instance Stump2012.instDecidableEqThurfaLex : DecidableEq ThurfaLex

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeThurfaLex : Fintype ThurfaLex

Equations

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

@[instance_reducible]

instance Stump2012.instReprThurfaLex : Repr ThurfaLex

Equations

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

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✝

inductive Stump2012.ThurfaStem : Type

ÞURFA has the strong stem þarf and the weak stem þurf.

• strong : ThurfaStem
• weak : ThurfaStem

@[instance_reducible]

instance Stump2012.instDecidableEqThurfaStem : DecidableEq ThurfaStem

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeThurfaStem : Fintype ThurfaStem

Equations

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

@[instance_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

@[instance_reducible]

instance Stump2012.instDecidableEqTense : DecidableEq Tense

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeTense : Fintype Tense

Equations

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

@[instance_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 pairs a tense with an agreement feature.

• tense : Tense
• agr : Agr

@[instance_reducible]

instance Stump2012.instDecidableEqTCell : DecidableEq TCell

Equations

• Stump2012.instDecidableEqTCell = Stump2012.instDecidableEqTCell.decEq

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 ⋯

@[instance_reducible]

instance Stump2012.instReprTCell : Repr TCell

Equations

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

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

Equations

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

@[instance_reducible]

instance Stump2012.instFintypeTCell : Fintype TCell

Equations

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

def Stump2012.thurfaLinkage : Morphology.Linkage ThurfaLex ThurfaStem TCell TCell

ÞURFA's linkage, the paper's (45) and (46), gives the present the strong stem and the past the weak stem, a suppletion, and its property mapping sends every cell to the past, the deponent tense.

Equations

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

def Stump2012.thurfaRealize : ThurfaStem → TCell → List String

In the realizations of (46), the strong stem at a past form cell gives the present forms and the weak stem the past forms.

Equations

• Stump2012.thurfaRealize Stump2012.ThurfaStem.strong x✝ = Stump2012.attested "need" (x✝.agr.cell { tense := ↑UD.Tense.Pres })
• Stump2012.thurfaRealize Stump2012.ThurfaStem.weak x✝ = Stump2012.attested "need" (x✝.agr.cell { tense := ↑UD.Tense.Past })

theorem Stump2012.thurfa_suppletive : thurfaLinkage.IsSuppletive ThurfaLex.thurfa

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

theorem Stump2012.thurfa_unfaithful : thurfaLinkage.IsUnfaithful id

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

theorem Stump2012.thurfa_suppletive_and_unfaithful : thurfaLinkage.IsSuppletive ThurfaLex.thurfa ∧ thurfaLinkage.IsUnfaithful id

ÞURFA's linkage compounds suppletion with a deponent tense mapping.

theorem Stump2012.thurfa_realizes : thurfaLinkage.realized thurfaRealize ThurfaLex.thurfa { tense := Tense.pres, agr := Agr.s1 } = {(attested "need" (Agr.s1.cell { tense := ↑UD.Tense.Pres }), { tense := Tense.past, agr := Agr.s1 })} ∧ thurfaLinkage.realized thurfaRealize ThurfaLex.thurfa { tense := Tense.past, agr := Agr.s1 } = {(attested "need" (Agr.s1.cell { tense := ↑UD.Tense.Past }), { tense := Tense.past, agr := Agr.s1 })}

The present content cell realizes as þarf through the strong stem at the past form cell, and the past content cell as þurfta through the weak stem.