The PFM1 paradigm function

import Linglib.Morphology.Paradigm.Function · namespace Morphology

This file defines the Paradigm Function Morphology engine of Stump's book in Bonami and Stump's streamlined form, PFM1. A paradigm function applies basic stem choice to a cell ⟨L, σ⟩ and then an ordered cascade of rule blocks. A rule applies at the cell when L is in its class and its property set is contained in σ, and in each block the narrowest applicable rule wins, by Pāṇinian narrowness. The Identity Function Default and the Function Composition Default are the least narrow rules of their blocks, and their behaviour as defaults is derived from that.

Main definitions

PFM.Action, PFM.Rule, PFM.Rule.narrowness: rule payloads, the realization rule shared by rules of exponence, referral and basic stem choice, and its narrowness key.
PFM.Rule.elsewhere, PFM.identityDefault: the least narrow rule with a given payload, and the Identity Function Default.
PFM.Block.eval, PFM.evalBlocks, PFM.paradigmFunction: a block, the block cascade and the paradigm function evaluated at a cell.
PFM.functionCompositionDefault, PFM.Block.portmanteau: portmanteau blocks, whose least narrow rule is the Function Composition Default.

Main results

PFM.Rule.narrowness_le_iff, PFM.Rule.applySet_mono: the two clauses of narrowness, and applicability-set inclusion between rules of one class.
PFM.selectMinimal_append_elsewhere, PFM.selectMinimal_isSome_of_identityDefault_mem: a least narrow rule is selected only where no other rule applies, and a block with the IFD always selects.
PFM.Block.eval_of_referral: a rule of referral re-consults its block at the retargeted cell.
PFM.Block.eval_portmanteau_of_applicable_eq_nil, PFM.Block.eval_portmanteau_of_applicable_ne_nil: the Function Composition Default, and its override by a portmanteau rule.
Morphology.Linkage.realized_eq_paradigmFunction: under the default rule of paradigm linkage, the realization of a content cell is the paradigm function.

Implementation notes

Blocks are evaluated at the cell rather than at a ⟨stem, property set⟩ pair, so the lexeme a stem is covertly indexed with persists through every block by construction. The chapter's values ⟨R, σ⟩ carry the cell's own property set, so evaluation returns the form alone. Whole-word syncretism, a clause of the paradigm function such as (5), is a property mapping of Linkage rather than a rule of referral. Morphophonological metageneralizations, conditions on a stem's phonological shape, and overabundance are outside the engine. Numbered examples refer to Bonami and Stump's chapter.

TODO

Stump's later rule conflation, which replaces a portmanteau block by a single rule combining two rules, is not modeled.

References

Bonami & Stump 2016, Paradigm Function Morphology formalized
Kiparsky 1973, “Elsewhere” in Phonology
Spencer 2013, Lexical Relatedness: A Paradigm-Based Model
Stump 2001, Inflectional Morphology: A Theory of Paradigm Structure
Stump 2016, Inflectional Paradigms: Content and Form at the Syntax-Morphology Interface formalized
Stump 2020, Paradigm Function Morphology: Assumptions and Innovations formalized
Stump 2022, Morphotactics: A Rule-Combining Approach

Declarations

A rule of exponence carries a form operation, which may consult the cell (its lexeme, with which a stem is covertly indexed, and, as Stump 2020 allows, its property set); a rule of referral carries a retargeting of property sets, at which its block is re-consulted.

inductive PFM.Action L78–83

(L : Type u_5) (Z : Type u_6) (P : Type u_7) :

Type (max (max u_5 u_6) u_7)

expo {L : Type u_5} {Z : Type u_6} {P : Type u_7} (f : L × P → Z → Z) : Action L Z P
referral {L : Type u_5} {Z : Type u_6} {P : Type u_7} (retarget : P → P) : Action L Z P

Used by PFM.Action.const, PFM.identityDefault, PFM.Block, PFM.Block.exists_eq_expo_of_mem_expoFragment, PFM.selectMinimal_isSome_of_identityDefault_mem, PFM.Block.eval_of_expo, PFM.Block.eval_of_referral, PFM.functionCompositionDefault

Used in BonamiStump2016

L85–86

A realization rule n, X_C, τ → f(X) of Bonami & Stump 2016 has a lexeme class C, the property set τ it realizes, and a payload: an Action for rules of exponence and referral, a stem for rules of basic stem choice.

structure PFM.Rule L88–97

(L : Type u_5) (P : Type u_6) (F : Type u_7) :

Type (max (max u_5 u_6) u_7)

klass : Finset L
The lexeme class the rule applies in.
props : P
The property set the rule realizes.
payload : F
The action or stem the rule supplies.

Used by PFM.Rule.narrowness, PFM.Rule.narrowness_le_iff, PFM.instRuleRuleProd, PFM.Rule.applies_iff, PFM.Rule.applySet_mono, PFM.Rule.elsewhere, PFM.identityDefault, PFM.Block, PFM.Block.exists_eq_expo_of_mem_expoFragment, PFM.selectMinimal_append_elsewhere, PFM.selectMinimal_isSome_of_identityDefault_mem, PFM.Block.eval_of_expo, PFM.Block.eval_of_referral, PFM.functionCompositionDefault

Used in BonamiStump2016

Narrowness as a key: r is at least as narrow as s when r's class is properly smaller, or the classes coincide and r's property set extends s's.

def PFM.Rule.narrowness L102–104

{L : Type u_1} {P : Type u_3} {F : Type u_4} (r : Rule L P F) :

Lex (Finset L × Pᵒᵈ)

r.narrowness = toLex (r.klass, OrderDual.toDual r.props)

Built from

Used by PFM.Rule.narrowness_le_iff, PFM.Rule.applySet_mono, PFM.Rule.narrowness_elsewhere, PFM.selectMinimal_append_elsewhere, PFM.selectMinimal_isSome_of_identityDefault_mem, PFM.Block.eval_of_expo, PFM.Block.eval_of_referral

Used in BonamiStump2016

Narrowness (15): a properly smaller class, or the same class and a larger property set.

theorem PFM.Rule.narrowness_le_iff L106–109

{L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] {r s : Rule L P F} :

r.narrowness ≤ s.narrowness ↔ r.klass ⊂ s.klass ∨ r.klass = s.klass ∧ s.props ≤ r.props

Built from ,

L111–113

L115–117

Between rules of one class, a narrower rule applies in fewer cells. Across classes a smaller class outranks a larger one whatever the property sets, so narrowness is strictly finer than applicability-set inclusion.

theorem PFM.Rule.applySet_mono L119–126

{L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] {r s : Rule L P F} (hk : r.klass = s.klass) (h : r.narrowness ≤ s.narrowness) :

Exponence.applySet r ⊆ Exponence.applySet s

Built from ,

The least narrow rule with payload f, n, X_U, {} → f(X), applies in the class of all lexemes and realizes the empty property set.

def PFM.Rule.elsewhere L130–132

{L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] [Fintype L] [OrderBot P] (f : F) :

Rule L P F

PFM.Rule.elsewhere f = { klass := Finset.univ, props := ⊥, payload := f }

Built from

Used by PFM.Rule.narrowness_elsewhere, PFM.Rule.elsewhere_applies, PFM.identityDefault, PFM.selectMinimal_append_elsewhere, PFM.functionCompositionDefault

L134–136

L138–139

The Identity Function Default (16) leaves the stem unchanged.

def PFM.identityDefault L141–142

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [Fintype L] [OrderBot P] :

Rule L P (Action L Z P)

PFM.identityDefault = PFM.Rule.elsewhere (PFM.Action.const id)

Built from , , ,

Used by PFM.selectMinimal_isSome_of_identityDefault_mem

Used in BonamiStump2016

Blocks and the paradigm function

A least narrow rule appended to a rule set is selected only where none of its rules applies.

theorem PFM.selectMinimal_append_elsewhere L174–178

{L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] [Fintype L] [OrderBot P] (v : Exponence.RuleSet (Rule L P F)) (f : F) (c : L × P) :

(v ++ [Rule.elsewhere f]).selectMinimal Rule.narrowness c = (v.selectMinimal Rule.narrowness c).or (some (Rule.elsewhere f))

Built from , ,

A block containing the IFD always selects a rule, the totality of Nar (14).

theorem PFM.selectMinimal_isSome_of_identityDefault_mem L180–184

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] [Fintype L] [OrderBot P] {v : Exponence.RuleSet (Rule L P (Action L Z P))} (h : identityDefault ∈ v) (c : L × P) :

(v.selectMinimal Rule.narrowness c).isSome = true

Built from , , ,

b.eval c w is Nar (14), [n : ⟨w, σ⟩]: the narrowest rule of b applicable at the cell c acts on the form w. A rule of referral re-selects among the rules of exponence at the retargeted cell, and w is unchanged where no rule applies.

def PFM.Block.eval L186–196

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] (b : Block L Z P) (c : L × P) (w : Z) :

The definition is too large to print here; read it in the source.

Built from

Used by PFM.Block.eval_of_expo, PFM.Block.eval_of_referral, PFM.evalBlocks, PFM.evalBlocks_cons, PFM.functionCompositionDefault, PFM.Block.eval_portmanteau_of_applicable_eq_nil, PFM.Block.eval_portmanteau_of_applicable_ne_nil

Used in BonamiStump2016

L198–203

A selected rule of referral evaluates its block's rules of exponence at the retargeted cell, as in the Sanskrit vocative (17).

theorem PFM.Block.eval_of_referral L205–216

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] {b : Block L Z P} {c : L × P} {r : Rule L P (Action L Z P)} {g : P → P} (hr : Exponence.RuleSet.selectMinimal b Rule.narrowness c = some r) (hg : r.payload = Action.referral g) (w : Z) :

b.eval c w = b.expoFragment.eval (c.1, g c.2) w

Built from , , , , ,

evalBlocks bs c w threads the form w through the blocks bs, listed inner-first, at the cell c.

def PFM.evalBlocks L218–221

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] (bs : List (Block L Z P)) (c : L × P) (w : Z) :

PFM.evalBlocks bs c w = List.foldl (fun (w : Z) (b : PFM.Block L Z P) => b.eval c w) w bs

Built from ,

Used by PFM.evalBlocks_nil, PFM.evalBlocks_cons, PFM.paradigmFunction, Linkage.realized_eq_paradigmFunction

L223–224

L226–228

The paradigm function (13) applies basic stem choice and then the blocks bs, listed inner-first, so that paradigmFunction stem [i, ii, iii] realizes [iii : [ii : [i : Stem]]].

def PFM.paradigmFunction L230–233

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] (stem : L × P → Z) (bs : List (Block L Z P)) (c : L × P) :

PFM.paradigmFunction stem bs c = PFM.evalBlocks bs c (stem c)

Built from ,

Used by Linkage.realized_eq_paradigmFunction

Used in BonamiStump2016, Stump2016

Portmanteau blocks

The Function Composition Default (24) of a portmanteau block [m, n] is the least narrow rule realizing [m : [n : ⟨X, σ⟩]].

def PFM.functionCompositionDefault L240–243

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] [Fintype L] [OrderBot P] (bm bn : Block L Z P) :

Rule L P (Action L Z P)

PFM.functionCompositionDefault bm bn = PFM.Rule.elsewhere (PFM.Action.expo fun (c : L × P) (w : Z) => bm.eval c (bn.eval c w))

Built from , , , ,

Used by PFM.Block.portmanteau

A portmanteau block [m, n] of Stump 2001 has rules bmn in paradigmatic opposition to blocks m and n together, and the Function Composition Default.

def PFM.Block.portmanteau L245–248

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] [Fintype L] [OrderBot P] (bmn bm bn : Block L Z P) :

Block L Z P

bmn.portmanteau bm bn = bmn ++ [PFM.functionCompositionDefault bm bn]

Built from ,

Used by PFM.Block.eval_portmanteau_of_applicable_eq_nil, PFM.Block.eval_portmanteau_of_applicable_ne_nil

Where no portmanteau rule applies, block [m, n] is the composition of blocks m and n, the Function Composition Default (24).

theorem PFM.Block.eval_portmanteau_of_applicable_eq_nil L250–258

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] [Fintype L] [OrderBot P] {bmn bm bn : Block L Z P} {c : L × P} (h : Exponence.RuleSet.applicable bmn c = []) (w : Z) :

(bmn.portmanteau bm bn).eval c w = bm.eval c (bn.eval c w)

Built from , ,

Where a portmanteau rule of exponence applies, it overrides blocks m and n.

theorem PFM.Block.eval_portmanteau_of_applicable_ne_nil L260–271

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] [Fintype L] [OrderBot P] {bmn bm bn : Block L Z P} {c : L × P} (hbmn : ∀ r ∈ bmn, ∃ (f : L × P → Z → Z), r.payload = Action.expo f) (h : Exponence.RuleSet.applicable bmn c ≠ []) (w : Z) :

(bmn.portmanteau bm bn).eval c w = bmn.eval c w

Built from , ,

Under the default rule of paradigm linkage (27), with property-preserving property mapping, form cells realized by the block cascade at their stem's L-index, and the convention (11) that a basic stem's L-index is its lexeme, a content cell realizes as the paradigm function.

theorem Linkage.realized_eq_paradigmFunction L275–284

{L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableLT P] [DecidableEq Z] (ℓ : Linkage L Z P P) (lindex : Z → L) (stem : L × P → Z) (bs : List (PFM.Block L Z P)) (h : ℓ.IsPropertyPreserving id) (hstem : ∀ (l : L) (σ : P), ℓ.realize l σ = {stem (l, σ)}) (hl : ∀ (c : L × P), lindex (stem c) = c.1) (l : L) (σ : P) :

ℓ.realized (fun (z : Z) (τ : P) => PFM.evalBlocks bs (lindex z, τ) z) l σ = {(PFM.paradigmFunction stem bs (l, σ), σ)}

Built from , ,