Bonami and Stump 2016: Paradigm Function Morphology

This file formalizes the worked PFM1 fragments of [bonami-stump-2016] 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, blockI, blockII, blockIII, pf — the Icelandic rules of 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

• [bonami-stump-2016]
• [stump-2001]

Icelandic verbs

inductive BonamiStump2016.Verb : Type

The four verbs of Table 17.1: 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

@[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: 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: past-tense exponence.

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: agreement and mood 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 (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): every stem in v's paradigm is indexed v.

Equations

• BonamiStump2016.lindex v x✝ = v

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

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

Equations

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

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})

(4a): kallaðir, 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})

(4c): the bare imperative gríp — 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})

(4d): flaug, 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})

Table 17.1: the strong second-singular past greipst, the strong-verb rule preempting -r.

theorem BonamiStump2016.stem_gripa_pst : Morphology.PFM.stemChoiceOf iceStems (fun (x : Verb) => "") (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): [iii : ⟨ætla, {imp 2sg}⟩] = ⟨ætlaðu, σ⟩.

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

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

Two ninth-conjugation verbs: 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): 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): 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): -āna after a consonant-final root, consonant-finality 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})

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

theorem BonamiStump2016.kri_no_portmanteau : Morphology.Exponence.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}))

(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})

Table 17.5: krīnīhi.

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

σ/{nom} of (17): the property set 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: 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})

Table 17.2: the vocative dual dāne.