Bonami and Stump 2016: Paradigm Function Morphology

This file formalizes the worked PFM1 fragments of [BS17] on the engine of Morphology/Paradigm/Function.lean: the finite paradigm of four Icelandic verbs (rules of basic stem choice, three blocks of rules of exponence, the Identity Function Default), the Sanskrit ninth-conjugation portmanteau with the Function Composition Default, and the Sanskrit vocative rule of referral.

Morphophonological metageneralizations (umlaut, vowel loss, coalescence) are phonological substance outside the engine, so only cells they leave untouched are decided; the strong verbs' ablaut alternants enter as basic stems, as in the chapter.

Main definitions

• iceStems, stemChoice, blockI, blockII, blockIII, pf — the Icelandic rules of basic stem choice, basic stem choice, rules of exponence, and paradigm function
• blockNi, blockHi, blockAna — the Sanskrit -nī, -hi and portmanteau -āna blocks
• caseBlock — a Sanskrit case block with the vocative rule of referral

Main results

• pf_kalla, pf_gripa_imp, pf_fljuga, pf_gripa_pst — the chapter's flagship realizations
• stem_gripa_pst — narrowness resolves the greip/grip/gríp stem conflict
• blockIII_narrowness — the three competing second-singular rules are strictly ordered
• as_portmanteau, kri_composition — -āna overrides -nī-hi; a vowel-final root defaults to the composition of Blocks ii and i
• voc_refers_to_nom — the vocative dual takes the nominative dual's exponent

References

• [BS17]
• [Stu01]

Icelandic verbs

inductive BonamiStump2016.Verb : Type

The four verbs of Table 17.1 are KALLA (weak.4.a), ÆTLA (weak.4.b), GRÍPA (strong.1.a) and FLJÚGA (strong.2.b).

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

@[instance_reducible]

instance BonamiStump2016.instDecidableEqVerb : DecidableEq Verb

Equations

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

@[instance_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 properties; person and number are separate properties, as in the chapter's {pst sg}.

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

@[instance_reducible]

instance BonamiStump2016.instDecidableEqFeat : DecidableEq Feat

Equations

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

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

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

The strong conjugations.

Equations

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

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

Block I of Table 17.3 realizes the theme vowels.

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 of Table 17.3 realizes past tense.

Equations

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

def BonamiStump2016.weak4bImp : Morphology.PFM.Rule Verb (Finset Feat) (Morphology.PFM.Action String (Finset Feat))

The weak.4.b imperative -ðu.

Equations

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

def BonamiStump2016.zeroImp : Morphology.PFM.Rule Verb (Finset Feat) (Morphology.PFM.Action String (Finset Feat))

The zero exponent of the second-singular imperative.

Equations

• BonamiStump2016.zeroImp = { klass := Finset.univ, props := {BonamiStump2016.Feat.imp, BonamiStump2016.Feat.p2, BonamiStump2016.Feat.sg}, payload := Morphology.PFM.Action.const id }

def BonamiStump2016.rSg2 : Morphology.PFM.Rule Verb (Finset Feat) (Morphology.PFM.Action String (Finset Feat))

The general second-singular -r.

Equations

• BonamiStump2016.rSg2 = { klass := Finset.univ, props := {BonamiStump2016.Feat.p2, BonamiStump2016.Feat.sg}, payload := Morphology.PFM.Action.const fun (x : String) => x ++ "r" }

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

Block III of Table 17.3 realizes agreement and mood.

Equations

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

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

Rules of basic stem choice (7); the strong verbs' ablaut alternants are listed as stems.

Equations

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

def BonamiStump2016.lindex (v : Verb) : String → Verb

The covert lexemic index (11) indexes every stem in v's paradigm with v.

Equations

• BonamiStump2016.lindex v x✝ = v

def BonamiStump2016.stemChoice : Verb × Finset Feat → String

Bonami and Stump's basic stem choice (7) gives a cell the stem of its narrowest applicable rule of basic stem choice, the narrowness order of the rules of exponence resolving conflicts.

Equations

• BonamiStump2016.stemChoice = BonamiStump2016.iceStems.realizeMinimalD fun (x : BonamiStump2016.Verb × Finset BonamiStump2016.Feat) => ""

def BonamiStump2016.pf (v : Verb) (σ : Finset Feat) : String × Finset Feat

The Icelandic paradigm function (13) applies basic stem choice and then Blocks I–III.

Equations

• BonamiStump2016.pf v σ = Morphology.PFM.paradigmFunction (BonamiStump2016.lindex v) BonamiStump2016.stemChoice [BonamiStump2016.blockI, BonamiStump2016.blockII, BonamiStump2016.blockIII] (v, σ)

theorem BonamiStump2016.pf_kalla : pf Verb.kalla {Feat.ind, Feat.pst, Feat.p2, Feat.sg} = ("kallaðir", {Feat.ind, Feat.pst, Feat.p2, Feat.sg})

The form kallaðir of (4a) is derived by (6) as kall + -a + -ði + -r.

theorem BonamiStump2016.pf_gripa_imp : pf Verb.gripa {Feat.imp, Feat.p2, Feat.sg} = ("gríp", {Feat.imp, Feat.p2, Feat.sg})

The bare imperative gríp of (4c) arises as the IFD fires in Blocks I and II and the zero imperative exponent preempts -r in Block III.

theorem BonamiStump2016.pf_fljuga : pf Verb.fljuga {Feat.ind, Feat.pst, Feat.p1, Feat.sg} = ("flaug", {Feat.ind, Feat.pst, Feat.p1, Feat.sg})

The form flaug of (4d) is the stem of the narrowest stem-choice rule for FLJÚGA, followed by the IFD in every block.

theorem BonamiStump2016.pf_gripa_pst : pf Verb.gripa {Feat.ind, Feat.pst, Feat.p2, Feat.sg} = ("greipst", {Feat.ind, Feat.pst, Feat.p2, Feat.sg})

The strong second-singular past greipst of Table 17.1 arises as the strong-verb rule preempts -r.

theorem BonamiStump2016.stem_gripa_pst : stemChoice (Verb.gripa, {Feat.ind, Feat.pst, Feat.p1, Feat.sg}) = "greip"

The conflict among (7c)–(7e) at ⟨GRÍPA, {ind pst 1sg}⟩ resolves to the three-cell rule.

theorem BonamiStump2016.blockI_gripa : Morphology.PFM.evalBlock (lindex Verb.gripa) blockI ("gríp", {Feat.ind, Feat.prs, Feat.p1, Feat.sg}) = ("gríp", {Feat.ind, Feat.prs, Feat.p1, Feat.sg})

A strong verb's Block I has no applicable rule of exponence, so the IFD leaves the stem.

theorem BonamiStump2016.nar_aetla_imp : Morphology.PFM.evalBlock (lindex Verb.aetla) blockIII ("ætla", {Feat.imp, Feat.p2, Feat.sg}) = ("ætlaðu", {Feat.imp, Feat.p2, Feat.sg})

The example of (14) is the evaluation of Block III [iii : ⟨ætla, {imp 2sg}⟩] = ⟨ætlaðu, σ⟩.

theorem BonamiStump2016.blockIII_narrowness : weak4bImp < zeroImp ∧ zeroImp < rSg2

In the example of (15), the weak.4.b -ðu is narrower than the zero imperative, which is narrower than -r.

Sanskrit portmanteau and the Function Composition Default

inductive BonamiStump2016.NinthVerb : Type

The two ninth-conjugation verbs are consonant-final AŚ 'eat' and vowel-final KRĪ 'buy'.

• as : NinthVerb
• kri : NinthVerb

@[instance_reducible]

instance BonamiStump2016.instDecidableEqNinthVerb : DecidableEq NinthVerb

Equations

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

@[instance_reducible]

instance BonamiStump2016.instFintypeNinthVerb : Fintype NinthVerb

Equations

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

inductive BonamiStump2016.SF : Type

Properties of the second-person singular imperative active.

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

@[instance_reducible]

instance BonamiStump2016.instDecidableEqSF : DecidableEq SF

Equations

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

@[instance_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 NinthVerb String (Finset SF)

Block i (20a) realizes the ninth-conjugation -nī.

Equations

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

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

Block ii (20b) realizes the second-singular imperative active -hi.

Equations

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

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

Block [ii,i] (20c) realizes -āna after a consonant-final root, consonant-finality being carried by the class {AŚ}.

Equations

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

theorem BonamiStump2016.as_portmanteau : Morphology.PFM.evalPortmanteau (fun (x : String) => NinthVerb.as) blockAna blockHi blockNi ("aś", {SF.p2, SF.sg, SF.imp, SF.act}) = ("aśāna", {SF.p2, SF.sg, SF.imp, SF.act})

By (21) at (22), AŚ takes the portmanteau -āna (Table 17.5).

theorem BonamiStump2016.kri_no_portmanteau : Morphology.Exponence.RuleSet.applicable blockAna (NinthVerb.kri, {SF.p2, SF.sg, SF.imp, SF.act}) = []

No portmanteau rule applies at (23).

theorem BonamiStump2016.kri_fcd : Morphology.PFM.evalPortmanteau (fun (x : String) => NinthVerb.kri) blockAna blockHi blockNi ("krī", {SF.p2, SF.sg, SF.imp, SF.act}) = Morphology.PFM.evalBlock (fun (x : String) => NinthVerb.kri) blockHi (Morphology.PFM.evalBlock (fun (x : String) => NinthVerb.kri) blockNi ("krī", {SF.p2, SF.sg, SF.imp, SF.act}))

At (23), Block [ii,i] defaults to the composition of Blocks ii and i, the Function Composition Default (24).

theorem BonamiStump2016.kri_composition : Morphology.PFM.evalPortmanteau (fun (x : String) => NinthVerb.kri) blockAna blockHi blockNi ("krī", {SF.p2, SF.sg, SF.imp, SF.act}) = ("krīnīhi", {SF.p2, SF.sg, SF.imp, SF.act})

The composition gives KRĪ's krīnīhi of Table 17.5.

Sanskrit vocative referral

inductive BonamiStump2016.Noun : Type

The neuter a-stem DĀNA 'gift' of Table 17.2.

• dana : Noun

@[instance_reducible]

instance BonamiStump2016.instDecidableEqNoun : DecidableEq Noun

Equations

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

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

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

@[instance_reducible]

instance BonamiStump2016.instDecidableEqNF : DecidableEq NF

Equations

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

@[instance_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.toNom (σ : Finset NF) : Finset NF

The property set σ/{nom} of (17) is like σ but nominative.

Equations

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

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

Block i holds a nominative exponent and the vocative rule of referral (17), which re-consults the block at the nominative cell.

Equations

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

theorem BonamiStump2016.voc_refers_to_nom : (Morphology.PFM.evalBlock (fun (x : String) => Noun.dana) caseBlock ("dān", {NF.voc, NF.du})).1 = (Morphology.PFM.evalBlock (fun (x : String) => Noun.dana) caseBlock ("dān", {NF.nom, NF.du})).1

The vocative dual takes the nominative dual's exponent, a syncretism confined to Block i, unlike the whole-word clause (5).

theorem BonamiStump2016.voc_du : Morphology.PFM.evalBlock (fun (x : String) => Noun.dana) caseBlock ("dān", {NF.voc, NF.du}) = ("dāne", {NF.voc, NF.du})

The vocative dual is dāne, as in Table 17.2.