The PFM1 paradigm function

The standard Paradigm Function Morphology engine ([BS17]'s streamlined PFM1, after [Stu01]): a paradigm function is a set of realization rules organized into ordered blocks. A rule ⟨klass, props, payload⟩ applies to a cell ⟨L, σ⟩ when the lexeme L belongs to klass and the property set props is contained in σ; among the applicable rules of a block, the narrowest wins ([Kip73]'s Elsewhere Condition, PFM's Pāṇinian Determinism). A single payload-polymorphic carrier Rule L P F serves all three rule types: rules of exponence and referral take F := Action Z P, rules of basic stem choice take F := Z; stem-choice conflicts are arbitrated by the same narrowness order.

Narrowness (Rule's ≤) is [Stu01]'s two clauses: same class with a larger property set, or a properly smaller class. It is intensional — for same-class rules it collapses to applicability-set inclusion (applySet_mono), but across classes a smaller class outranks a larger one whatever the property sets, so the order is strictly finer than the extensional [Stu16]/[Stu22] domain-subset order of Exponence/Basic.lean ([Stu20] likewise glosses "narrowest" extensionally, as the smaller domain of application).

The Identity Function Default — every block has a rule leaving the stem unchanged — is assumed as a universal principle in PFM; here it is a definition (identityDefault) and its consequences are theorems (it is ≤-maximal, and a block containing it always selects). Two implicative devices are kept distinct ([BS17]): a rule of referral (Action.referral) models block-confined syncretism, competing inside its block; whole-word syncretism lives a layer up, as a many-to-one property mapping in Linkage.pm (Linkage.realize_eq_of_corr_eq), where [Stu20] relocates it — paradigm-function-level override clauses are not modeled. Overabundance (one cell, several forms) is out of scope: the realized paradigm is function-valued, one form per cell. Morphophonological metageneralizations (the -a-loss and umlaut rules of the Icelandic fragment) are phonological substance and live in Phonology/; here stem alternants like köll enter as data-level stem values, not string operations.

Because payloads are functions, Exponence.Coherent and Realizes over Action Z P are funext propositions rather than decidable checks; a study decides realized values, not payload equality.

Main declarations

• Action, Rule — the payload (exponence or referral) and the payload-polymorphic realization rule
• Rule's Exponence.Rule and Preorder instances — applicability and two-clause narrowness; Rule.applies_iff, Rule.le_iff, Rule.applySet_mono
• identityDefault, le_identityDefault, selectMinimal_isSome_of_mem_identityDefault — the IFD and its consequences
• evalBlock, paradigmFunction, stemChoiceOf — narrowest-rule block evaluation and the block cascade
• evalPortmanteau, evalPortmanteau_eq_comp_of_not_applies — portmanteau blocks and the Function Composition Default
• selectMinimal_append_maximal — appending a maximal always-applicable rule is elsewhere-only: the mechanism behind identityDefault and the FCD
• functionCompositionDefault, le_functionCompositionDefault, evalPortmanteau_eq_functionCompositionDefault — the FCD as a derived ≤-maximal rule, and the stipulated portmanteau evaluation equals its appended-block form
• Linkage.realize_eq_paradigmFunction — the PFM2 realization of a linkage's block cascade is this paradigm function

inductive Morphology.PFM.Action (Z : Type u_5) (P : Type u_6) : Type (max u_5 u_6)

The payload of a realization rule: a rule of exponence carries a form operation f : P → Z → Z that may consult the realized property set, a rule of referral carries a property-set retargeting P → P whose block is re-consulted at the retargeted cell. The property argument makes the form operation σ-sensitive, as [Stu20]'s rule format allows (his conditional affixation operator for ambifixal classes consults σ), and lets the Function Composition Default carry a rule whose action is "evaluate two blocks at the current cell".

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

def Morphology.PFM.Action.const {Z : Type u_2} {P : Type u_3} (f : Z → Z) : Action Z P

A property-insensitive rule of exponence: a form operation f : Z → Z applied regardless of the property set — the special case of Action.expo before [Stu20]'s σ-sensitive rule format, and the shape of every exponent in [BS17]'s worked fragments.

Equations

• Morphology.PFM.Action.const f = Morphology.PFM.Action.expo fun (x : P) => f

structure Morphology.PFM.Rule (L : Type u_5) (P : Type u_6) (F : Type u_7) : Type (max (max u_5 u_6) u_7)

A realization rule in [BS17]'s format ⟨klass, props, payload⟩ (the chapter's n, X_C, τ → f(X)), payload-polymorphic à la Containment.SpanRule: rules of exponence and referral instantiate F := Action Z P, rules of basic stem choice F := Z. klass is the lexeme class C, props the realized property set τ.

• klass : Finset L

  The lexeme class the rule applies in.

• props : P

  The property set the rule realizes.

• payload : F

  The form operation (exponence/referral) or stem the rule supplies.

@[implicit_reducible]

instance Morphology.PFM.instPreorderRule {L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] : Preorder (Rule L P F)

Two-clause Pāṇinian narrowness ([Stu01]) as the carrier's order: r is at least as narrow as s when either they share a class and s realizes a subset of r's properties, or r's class is properly smaller. Intensional — strictly finer than applicability-set inclusion (see Rule.applySet_mono; the converse fails).

Equations

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

theorem Morphology.PFM.Rule.le_iff {L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] {r s : Rule L P F} : r ≤ s ↔ r.klass = s.klass ∧ s.props ≤ r.props ∨ r.klass ⊂ s.klass

@[implicit_reducible]

instance Morphology.PFM.instRuleRuleProd {L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] : Exponence.Rule (Rule L P F) (L × P) F

Applicability ([BS17]'s rule format): a rule applies to a cell ⟨L, σ⟩ when L is in its class and its property set is contained in σ.

Equations

• Morphology.PFM.instRuleRuleProd = { exponent := Morphology.PFM.Rule.payload, Applies := fun (r : Morphology.PFM.Rule L P F) (c : L × P) => c.1 ∈ r.klass ∧ r.props ≤ c.2 }

@[simp]

theorem Morphology.PFM.Rule.applies_iff {L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] {r : Rule L P F} {c : L × P} : Exponence.Applies r c ↔ c.1 ∈ r.klass ∧ r.props ≤ c.2

theorem Morphology.PFM.Rule.applySet_mono {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 ≤ s) : Exponence.applySet r ⊆ Exponence.applySet s

For same-class rules, narrowness is applicability-set inclusion: the narrower rule applies in a subset of the contexts — [Stu01]'s two-clause narrowness collapsing to [Stu16]'s single-clause domain-subset precedence. Across classes the order is strictly intensional (a smaller class outranks a larger one whatever the property sets), so a class hypothesis is required.

Selection over the narrowness order

@[implicit_reducible]

instance Morphology.PFM.instDecidableRelRuleProdApplies {L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] [DecidableEq L] [DecidableLE P] : DecidableRel Exponence.Applies

Equations

• Morphology.PFM.instDecidableRelRuleProdApplies r c = instDecidableAnd

@[implicit_reducible]

instance Morphology.PFM.instDecidableLERule {L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] [DecidableEq L] [DecidableLE P] : DecidableLE (Rule L P F)

Equations

• Morphology.PFM.instDecidableLERule r s = instDecidableOr

@[implicit_reducible]

instance Morphology.PFM.instDecidableLTRule {L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] [DecidableEq L] [DecidableLE P] : DecidableLT (Rule L P F)

Equations

• Morphology.PFM.instDecidableLTRule r s = instDecidableAnd

The Identity Function Default

def Morphology.PFM.identityDefault {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [Fintype L] [OrderBot P] : Rule L P (Action Z P)

The Identity Function Default ([BS17]): the rule applying to every lexeme and every property set, changing nothing. PFM assumes a rule of this form in every block as a universal principle; here it is a definition whose consequences are theorems.

Equations

• Morphology.PFM.identityDefault = { klass := Finset.univ, props := ⊥, payload := Morphology.PFM.Action.const id }

theorem Morphology.PFM.identityDefault_applies {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [Fintype L] [OrderBot P] (c : L × P) : Exponence.Applies identityDefault c

theorem Morphology.PFM.le_identityDefault {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [Fintype L] [OrderBot P] (r : Rule L P (Action Z P)) : r ≤ identityDefault

The IFD is ≤-maximal: every rule is at least as narrow. It is a top element of the narrowness order without an OrderTop instance (which would force Fintype/OrderBot globally).

theorem Morphology.PFM.selectMinimal_isSome_of_mem_identityDefault {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [Fintype L] [OrderBot P] {v : List (Rule L P (Action Z P))} {c : L × P} (h : identityDefault ∈ v) : (Exponence.selectMinimal v c).isSome = true

A block containing the IFD always selects a rule — the totality of Nar ([BS17]'s (14)) that [Stu01] secures by stipulating the IFD.

Blocks and the paradigm function

@[reducible, inline]

abbrev Morphology.PFM.Block (L : Type u_5) (Z : Type u_6) (P : Type u_7) : Type (max (max u_7 u_6) u_5)

A rule block ([BS17]): rules of exponence and referral in paradigmatic opposition, only the narrowest applying.

Equations

• Morphology.PFM.Block L Z P = List (Morphology.PFM.Rule L P (Morphology.PFM.Action Z P))

def Morphology.PFM.expoFragment {L : Type u_1} {Z : Type u_2} {P : Type u_3} (b : Block L Z P) : Block L Z P

The rules of exponence in a block (referral rules dropped), the target of a referral's re-selection.

Equations

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

def Morphology.PFM.evalBlockForm {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (b : Block L Z P) (wσ : Z × P) : Z

The form produced by evaluating a block at a cell: select the narrowest applicable rule; an exponence rule applies its form operation, a referral rule re-selects among the block's exponence rules at the retargeted property set (one hop). The stem is left unchanged when nothing applies.

Equations

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

def Morphology.PFM.evalBlock {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (b : Block L Z P) (wσ : Z × P) : Z × P

Evaluate a block at a form-state, keeping the property set ([BS17]'s rule format outputs ⟨f(W), σ⟩).

Equations

• Morphology.PFM.evalBlock Lindex b wσ = (Morphology.PFM.evalBlockForm Lindex b wσ, wσ.2)

@[simp]

theorem Morphology.PFM.evalBlock_snd {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (b : Block L Z P) (wσ : Z × P) : (evalBlock Lindex b wσ).2 = wσ.2

def Morphology.PFM.blocksEval {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (blocks : List (Block L Z P)) (wσ : Z × P) : Z × P

Thread a form-state through a block cascade (blocks listed inner-first).

Equations

• Morphology.PFM.blocksEval Lindex blocks wσ = List.foldl (fun (w : Z × P) (b : Morphology.PFM.Block L Z P) => Morphology.PFM.evalBlock Lindex b w) wσ blocks

@[simp]

theorem Morphology.PFM.blocksEval_snd {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (blocks : List (Block L Z P)) (wσ : Z × P) : (blocksEval Lindex blocks wσ).2 = wσ.2

def Morphology.PFM.paradigmFunction {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (stemChoice : L × P → Z) (blocks : List (Block L Z P)) (c : L × P) : Z × P

The paradigm function ([BS17]'s (13)): basic stem choice, then the stipulated block cascade. blocks are listed inner-first, so [I, II, III] realizes [iii : [ii : [i : Stem]]]. Lindex : Z → L recovers a stem's covert lexemic index (fn. 7); L-index persistence holds by construction, since selection threads a fixed lexeme through L × P.

Equations

• Morphology.PFM.paradigmFunction Lindex stemChoice blocks c = Morphology.PFM.blocksEval Lindex blocks (stemChoice c, c.2)

def Morphology.PFM.stemChoiceOf {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (sv : List (Rule L P Z)) (default : L → Z) : L × P → Z

Basic stem choice ([BS17]'s (7)) as narrowest-rule selection over stem-choice rules (payload := Z), falling back to a per-lexeme default. Rule conflicts (the chapter's greip/grip/gríp) are resolved by the same narrowness order.

Equations

• Morphology.PFM.stemChoiceOf sv default c = (Option.map Morphology.PFM.Rule.payload (Morphology.Exponence.selectMinimal sv c)).getD (default c.1)

def Morphology.PFM.evalPortmanteau {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (bmn bm bn : Block L Z P) (wσ : Z × P) : Z × P

A portmanteau block [m, n] ([BS17]): its rules compete with the composition of blocks m and n; when none applies, the Function Composition Default falls back to that composition. This is the handbook's block-straddling device; [Stu20] supersedes it with rule conflation (a portmanteau rule as the conflation of two rules, sitting in a single block and winning by ordinary narrowness), the route [Stu22] develops — kept here as the faithfully pre-conflation account.

Equations

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

theorem Morphology.PFM.evalPortmanteau_eq_comp_of_not_applies {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (bmn bm bn : Block L Z P) (wσ : Z × P) (h : Exponence.applicable bmn (Lindex wσ.1, wσ.2) = []) : evalPortmanteau Lindex bmn bm bn wσ = evalBlock Lindex bm (evalBlock Lindex bn wσ)

The Function Composition Default ([BS17]): where no portmanteau rule applies, the portmanteau block is the composition of its component blocks.

theorem Morphology.PFM.selectMinimal_append_maximal {L : Type u_1} {P : Type u_3} {F : Type u_4} [PartialOrder P] [DecidableEq L] [DecidableLE P] {v : List (Rule L P F)} {c : L × P} {top : Rule L P F} (hmax : ∀ (r : Rule L P F), r ≤ top) (htop : Exponence.Applies top c) : Exponence.selectMinimal (v ++ [top]) c = (Exponence.selectMinimal v c).or (some top)

Appending a ≤-maximal always-applicable rule to a block leaves narrowest-rule selection unchanged when the block already selects, and picks that rule otherwise: a maximal rule is preempted by any genuine competitor and fires only in the elsewhere. The mechanism shared by identityDefault and functionCompositionDefault.

The Function Composition Default as a derived rule

def Morphology.PFM.functionCompositionDefault {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [Fintype L] [OrderBot P] (Lindex : Z → L) (bm bn : Block L Z P) : Rule L P (Action Z P)

The Function Composition Default as a derived rule ([Spe13b]): the rule of a portmanteau block [m, n] whose σ-sensitive action evaluates blocks m then n at the current cell. Like identityDefault it applies everywhere (klass = univ, props = ⊥) and is ≤-maximal, so any explicit portmanteau rule — being narrower — preempts it by ordinary Pāṇinian narrowness. [Spe13b] observes that an explicit portmanteau rule is by definition more specific than the FCD, so ordinary narrowness suffices to order them; this derives what evalPortmanteau stipulates, the same stipulate-to-derive upgrade identityDefault gives the Identity Function Default.

Equations

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

theorem Morphology.PFM.functionCompositionDefault_applies {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [Fintype L] [OrderBot P] (Lindex : Z → L) (bm bn : Block L Z P) (c : L × P) : Exponence.Applies (functionCompositionDefault Lindex bm bn) c

theorem Morphology.PFM.le_functionCompositionDefault {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [Fintype L] [OrderBot P] (Lindex : Z → L) (bm bn : Block L Z P) (r : Rule L P (Action Z P)) : r ≤ functionCompositionDefault Lindex bm bn

The FCD is ≤-maximal: every rule is at least as narrow, so an explicit portmanteau rule always preempts it ([Spe13b]). Same shape as le_identityDefault.

theorem Morphology.PFM.evalPortmanteau_eq_functionCompositionDefault {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [Fintype L] [OrderBot P] (Lindex : Z → L) (bmn bm bn : Block L Z P) (wσ : Z × P) (hbmn : ∀ r ∈ bmn, ∃ (f : P → Z → Z), r.payload = Action.expo f) : evalPortmanteau Lindex bmn bm bn wσ = evalBlock Lindex (bmn ++ [functionCompositionDefault Lindex bm bn]) wσ

FCD-as-derived-default: for a portmanteau block bmn of rules of exponence, the stipulated evalPortmanteau equals the block bmn ++ [fcd] evaluated as an ordinary block. Where a portmanteau rule applies it wins by narrowness (le_functionCompositionDefault, via selectMinimal_append_maximal); where none does, the appended FCD fires and evaluates bm ∘ bn at the cell. This certifies the stipulated Function Composition Default as [Stu20]'s single-block rule-conflation reading of [BS17]'s block-straddling device. The exponence-only hypothesis on bmn is what a portmanteau block is in PFM — referral, a separate syncretism device, re-selects over the block's expoFragment, which the appended (exponence-shaped) FCD would perturb.

theorem Morphology.PFM.Linkage.realize_eq_paradigmFunction {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] [DecidableEq Z] (ℓ : Linkage L Z P) (Lindex : Z → L) (stemChoice : L × P → Z) (blocks : List (Block L Z P)) (l : L) (σ : P) (h : ℓ.IsPropertyPreserving) (hstem : ∀ (l : L) (σ : P), ℓ.stems l σ = {stemChoice (l, σ)}) : ℓ.realize (fun (z : Z) (τ : P) => (blocksEval Lindex blocks (z, τ)).1) l σ = {paradigmFunction Lindex stemChoice blocks (l, σ)}

With property-preserving property mapping and PFM1 basic stem choice, the PFM2 realization of a paradigm linkage's block cascade ([Stu16]'s PF(⟨L, σ⟩) = PF(Corr(⟨L, σ⟩))) is this paradigm function — Linkage.realize's form-realization hole filled true by construction.

def Morphology.PFM.paradigmRealization {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (stemChoice : L × P → Z) (blocks : List (Block L Z P)) : Realization L P (Z × P)

The paradigm function as a realization: lexemes as opaque indices, realized at every cell — total and univalent, PFM's stratum. Lindex is the seed of the lexeme-to-√ coarsening arrow between individuation grains.

Equations

• Morphology.PFM.paradigmRealization Lindex stemChoice blocks = { realize := fun (l : L) (σ : P) => {Morphology.PFM.paradigmFunction Lindex stemChoice blocks (l, σ)} }

theorem Morphology.PFM.paradigmRealization_isTotal {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (stemChoice : L × P → Z) (blocks : List (Block L Z P)) : (paradigmRealization Lindex stemChoice blocks).IsTotal

theorem Morphology.PFM.paradigmRealization_isUnivalent {L : Type u_1} {Z : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (Lindex : Z → L) (stemChoice : L × P → Z) (blocks : List (Block L Z P)) : (paradigmRealization Lindex stemChoice blocks).IsUnivalent

Payload functoriality

def Morphology.PFM.Rule.mapPayload {L : Type u_1} {P : Type u_3} {F : Type u_4} {F' : Type u_5} (g : F → F') (r : Rule L P F) : Rule L P F'

Relabel a rule's payload, keeping its class and property set.

Equations

• Morphology.PFM.Rule.mapPayload g r = { klass := r.klass, props := r.props, payload := g r.payload }

@[simp]

theorem Morphology.PFM.Rule.mapPayload_klass {L : Type u_1} {P : Type u_3} {F : Type u_4} {F' : Type u_5} (g : F → F') (r : Rule L P F) : (mapPayload g r).klass = r.klass

@[simp]

theorem Morphology.PFM.Rule.mapPayload_props {L : Type u_1} {P : Type u_3} {F : Type u_4} {F' : Type u_5} (g : F → F') (r : Rule L P F) : (mapPayload g r).props = r.props

@[simp]

theorem Morphology.PFM.Rule.mapPayload_lt_iff {L : Type u_1} {P : Type u_3} {F : Type u_4} {F' : Type u_5} [PartialOrder P] {g : F → F'} {r s : Rule L P F} : mapPayload g r < mapPayload g s ↔ r < s

theorem Morphology.PFM.selectMinimal_map_payload {L : Type u_1} {P : Type u_3} {F : Type u_4} {F' : Type u_5} [PartialOrder P] [DecidableEq L] [DecidableLE P] (g : F → F') (v : List (Rule L P F)) (c : L × P) : Exponence.selectMinimal (List.map (Rule.mapPayload g) v) c = Option.map (Rule.mapPayload g) (Exponence.selectMinimal v c)

Applicability and narrowness read only class and props, so narrowest-rule selection is blind to a payload relabelling.