PFM1 worked fragments: Icelandic verbs and Sanskrit nominals

[BS17] [Stu01] [Kip73]

Worked fragments for the PFM1 engine of Morphology/Paradigm/Function.lean, transcribing [BS17]'s own examples.

• Icelandic verbs (their Table 17.1/17.3): the paradigm function derives PF(⟨KALLA, {ind pst 2sg}⟩) = kallaðir by pure suffixation -a, -ði, -r through Blocks I–III. Basic stem choice resolves the greip/grip/gríp conflict for GRÍPA by narrowness (the three-cell rule beats the twelve- and twenty-seven-cell rules); a strong verb's Block I falls through to the Identity Function Default. Umlaut (kall ~ köll) and the other morphophonological metageneralizations are phonological substance and are not modelled here, so only umlaut-free cells are decided.
• Sanskrit (their Table 17.5, (17)): the portmanteau -āna of a consonant-final ninth-conjugation root overrides the -nī/-hi sequence, while a vowel-final root defaults to their composition (the Function Composition Default); the vocative refers to the nominative's Block-i exponent (block-confined syncretism), a schematic case fragment.

All predictions are decide-checked realized values; payload equality is never decided (payloads are form operations).

Icelandic verbs (Table 17.1, Table 17.3)

inductive BonamiStump2016.Verb : Type

The four verbs of the fragment: KALLA weak.4.a, ÆTLA weak.4.b, GRÍPA strong.1.a, FLJÚGA strong.2.b.

• kalla : Verb
• aetla : Verb
• gripa : Verb
• fljuga : Verb

@[implicit_reducible]

instance BonamiStump2016.instDecidableEqVerb : DecidableEq Verb

Equations

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

@[implicit_reducible]

instance BonamiStump2016.instFintypeVerb : Fintype Verb

Equations

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

inductive BonamiStump2016.Feat : Type

Morphosyntactic features (decomposed: person and number separate).

• ind : Feat
• sbjv : Feat
• imp : Feat
• prs : Feat
• pst : Feat
• p1 : Feat
• p2 : Feat
• p3 : Feat
• sg : Feat
• pl : Feat

@[implicit_reducible]

instance BonamiStump2016.instDecidableEqFeat : DecidableEq Feat

Equations

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

@[implicit_reducible]

instance BonamiStump2016.instFintypeFeat : Fintype Feat

Equations

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

def BonamiStump2016.weak : Finset Verb

Weak conjugation 4 (here all weak verbs of the fragment).

Equations

• BonamiStump2016.weak = {BonamiStump2016.Verb.kalla, BonamiStump2016.Verb.aetla}

def BonamiStump2016.weak4b : Finset Verb

Weak conjugation 4.b.

Equations

• BonamiStump2016.weak4b = {BonamiStump2016.Verb.aetla}

def BonamiStump2016.strong : Finset Verb

Strong conjugation.

Equations

• BonamiStump2016.strong = {BonamiStump2016.Verb.gripa, BonamiStump2016.Verb.fljuga}

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

Block I: theme-vowel exponence ([BS17]'s Table 17.3).

Equations

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

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

Block II: past-tense exponence.

Equations

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

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

Block III: agreement exponence.

Equations

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

def BonamiStump2016.iceStems : List (Morphology.PFM.Rule Verb (Finset Feat) String)

Rules of basic stem choice ([BS17]'s (7)); the GRÍPA and FLJÚGA alternants list the umlaut/ablaut stems as data, not string operations.

Equations

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

def BonamiStump2016.iceStem : Finset Feat → Verb

Within one lexeme's paradigm the covert lexemic index is constant.

Equations

• BonamiStump2016.iceStem x✝ = BonamiStump2016.Verb.kalla

theorem BonamiStump2016.iceParadigm_hasNonemptyCores : Morphology.Root.HasNonemptyCores (Morphology.PFM.paradigmRealization (fun (x : String) => Verb.kalla) (Morphology.PFM.stemChoiceOf iceStems fun (x : Verb) => "") [blockI, blockII, blockIII]) fun (w : String × Finset Feat) => {w.1}

The Icelandic PFM inventory is atomic-total: as a Realization, the paradigm function realizes every cell (paradigmRealization_isTotal) with a single form (_isUnivalent), and under the stem projection every cell exposes a nonempty core — the lexeme-index stratum certified by Morphology.Root.HasNonemptyCores.

Sanskrit portmanteau and Function Composition Default (Table 17.5)

inductive BonamiStump2016.Root : Type

Two ninth-conjugation roots: AŚ (consonant-final), KRĪ (vowel-final).

• as : Root
• kri : Root

@[implicit_reducible]

instance BonamiStump2016.instDecidableEqRoot : DecidableEq Root

Equations

• BonamiStump2016.instDecidableEqRoot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BonamiStump2016.instFintypeRoot : Fintype Root

Equations

• BonamiStump2016.instFintypeRoot = { elems := { val := ↑BonamiStump2016.Root.enumList, nodup := BonamiStump2016.Root.enumList_nodup }, complete := BonamiStump2016.instFintypeRoot._proof_1 }

inductive BonamiStump2016.SF : Type

Features of the second-person singular imperative active.

• p2 : SF
• sg : SF
• imp : SF
• act : SF

@[implicit_reducible]

instance BonamiStump2016.instDecidableEqSF : DecidableEq SF

Equations

• BonamiStump2016.instDecidableEqSF x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BonamiStump2016.instFintypeSF : Fintype SF

Equations

• BonamiStump2016.instFintypeSF = { elems := { val := ↑BonamiStump2016.SF.enumList, nodup := BonamiStump2016.SF.enumList_nodup }, complete := BonamiStump2016.instFintypeSF._proof_1 }

def BonamiStump2016.blockNi : Morphology.PFM.Block Root String (Finset SF)

Block i: ninth-conjugation -nī ([BS17]'s (20a)).

Equations

• BonamiStump2016.blockNi = [{ klass := Finset.univ, props := ∅, payload := Morphology.PFM.Action.const fun (x : String) => x ++ "nī" }]

def BonamiStump2016.blockHi : Morphology.PFM.Block Root String (Finset SF)

Block ii: subject-agreement -hi ([BS17]'s (20b)).

Equations

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

def BonamiStump2016.blockAna : Morphology.PFM.Block Root String (Finset SF)

Portmanteau Block [ii,i]: consonant-final -āna ([BS17]'s (20c)); consonant-finality is carried by the singleton class {AŚ}.

Equations

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

Sanskrit vocative referral (schematic, (17))

inductive BonamiStump2016.Noun : Type

A schematic nominal declension.

• dana : Noun

@[implicit_reducible]

instance BonamiStump2016.instDecidableEqNoun : DecidableEq Noun

Equations

• BonamiStump2016.instDecidableEqNoun x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BonamiStump2016.instFintypeNoun : Fintype Noun

Equations

• BonamiStump2016.instFintypeNoun = { elems := { val := ↑BonamiStump2016.Noun.enumList, nodup := BonamiStump2016.Noun.enumList_nodup }, complete := BonamiStump2016.instFintypeNoun._proof_1 }

inductive BonamiStump2016.NF : Type

Case and number features.

• nom : NF
• voc : NF
• du : NF

@[implicit_reducible]

instance BonamiStump2016.instDecidableEqNF : DecidableEq NF

Equations

• BonamiStump2016.instDecidableEqNF x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BonamiStump2016.instFintypeNF : Fintype NF

Equations

• BonamiStump2016.instFintypeNF = { elems := { val := ↑BonamiStump2016.NF.enumList, nodup := BonamiStump2016.NF.enumList_nodup }, complete := BonamiStump2016.instFintypeNF._proof_1 }

def BonamiStump2016.vocToNom (σ : Finset NF) : Finset NF

Retarget a vocative property set to the corresponding nominative.

Equations

• BonamiStump2016.vocToNom σ = insert BonamiStump2016.NF.nom (σ.erase BonamiStump2016.NF.voc)

def BonamiStump2016.caseBlock : Morphology.PFM.Block Noun String (Finset NF)

The case block: a nominative exponence rule and a vocative rule of referral ([BS17]'s (17)), the referral re-consulting the block at the nominative cell.

Equations

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