Stump (2020): Paradigm Function Morphology

This file formalizes the Old English paradigm with which [Stu20]'s survey of Paradigm Function Morphology illustrates the framework: the finite forms of the weak verb HIERAN 'hear', run on the PFM engine of Morphology.Paradigm.Function. The paradigm's exploded segmentation is three affix blocks, the past formative, the theme vowel and agreement (blockI, blockII, blockIII), with the Identity Function Default filling empty positions, so that the bare imperative is the default firing through every block and the past forms compose the past formative, the theme vowel and the agreement suffix (hieranPF).

Implementation notes

Only the past cells and the agreement-suffixed present plural are decided; the present theme-vowel conditioning across the full paradigm needs block rules the survey's figure does not legibly give, and the elision of the theme vowel before the present plural suffix is phonological and not modelled. The survey's Kashmiri morphomic tense is formalized with its originating work in Studies/Stump2016.lean, and its Swahili rule conflation is left to future work.

References

• [Stu20]
• [BS17]

Old English HIERAN 'hear' (§2.2, Table 3)

inductive Stump2020.Verb : Type

The weak verb HIERAN.

• hieran : Verb

@[instance_reducible]

instance Stump2020.instDecidableEqVerb : DecidableEq Verb

Equations

• Stump2020.instDecidableEqVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2020.instFintypeVerb : Fintype Verb

Equations

• Stump2020.instFintypeVerb = { elems := { val := ↑Stump2020.Verb.enumList, nodup := Stump2020.Verb.enumList_nodup }, complete := Stump2020.instFintypeVerb._proof_1 }

inductive Stump2020.Feat : Type

Mood, tense, person, and number features (decomposed).

• ind : Feat
• sbj : Feat
• imp : Feat
• pres : Feat
• past : Feat
• p1 : Feat
• p2 : Feat
• p3 : Feat
• sg : Feat
• pl : Feat

@[instance_reducible]

instance Stump2020.instDecidableEqFeat : DecidableEq Feat

Equations

• Stump2020.instDecidableEqFeat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2020.instFintypeFeat : Fintype Feat

Equations

• Stump2020.instFintypeFeat = { elems := { val := ↑Stump2020.Feat.enumList, nodup := Stump2020.Feat.enumList_nodup }, complete := Stump2020.instFintypeFeat._proof_1 }

def Stump2020.blockI : Morphology.PFM.Block Verb String (Finset Feat)

Block I (position i): the past-tense formative -d-.

Equations

• Stump2020.blockI = [{ klass := Finset.univ, props := {Stump2020.Feat.past}, payload := Morphology.PFM.Action.const fun (x : String) => x ++ "d" }, Morphology.PFM.identityDefault]

def Stump2020.blockII : Morphology.PFM.Block Verb String (Finset Feat)

Block II (position ii): the theme vowel — -o- in the past plural, -e- elsewhere in the past (the present-tense conditioning is not modelled).

Equations

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

def Stump2020.blockIII : Morphology.PFM.Block Verb String (Finset Feat)

Block III (position iii): agreement and mood — -st (2sg indicative, [Stu20]'s rule (7)), -þ (3sg present indicative), -aþ (present plural), -n (past plural).

Equations

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

def Stump2020.hieranPF (σ : Finset Feat) : String × Finset Feat

The HIERAN paradigm function: stem hīer through Blocks I–III.

Equations

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