The paradigm function into word trees

The engine's state type Z is unconstrained ([BS17]'s PFM1, Paradigm/Function.lean), so the paradigm function runs at Z := Word.Tree M as readily as at material sequences. An affix-transparent vocabulary interprets into both, and toList intertwines the two runs (toList_paradigmFunction_tree); the emitted tree's stem is the chosen leaf under any classification counting the vocabulary's material as inflectional ([Spe13b]'s inflection-hood by provenance), and a kind-coherent vocabulary emits a kind-coherent tree.

Main declarations

• AffixAction — a prefix or suffix action carrying its affix; interprets into the engine at trees (toTreeAction) and at sequences (toAction)
• toList_paradigmFunction_tree, stem_paradigmFunction_tree, isKindCoherent_paradigmFunction_tree — linearization, stem, and coherence of the tree-valued run

The affix-transparent vocabulary

inductive Morphology.PFM.AffixAction (M : Type u_4) : Type u_4

A prefix or suffix action carrying its affix; rules over AffixAction cannot carry referrals.

• pre {M : Type u_4} (m : M) : AffixAction M

  Prepend the affix.

• suf {M : Type u_4} (m : M) : AffixAction M

  Append the affix.

def Morphology.PFM.AffixAction.material {M : Type u_1} : AffixAction M → M

The affix an action attaches.

Equations

• (Morphology.PFM.AffixAction.pre m).material = m
• (Morphology.PFM.AffixAction.suf m).material = m

def Morphology.PFM.AffixAction.apply {M : Type u_1} : AffixAction M → Word.Tree M → Word.Tree M

Apply an affix action to a tree.

Equations

• (Morphology.PFM.AffixAction.pre m).apply x✝ = Morphology.Word.Tree.prefixed m x✝
• (Morphology.PFM.AffixAction.suf m).apply x✝ = x✝.suffixed m

def Morphology.PFM.AffixAction.applyList {M : Type u_1} : AffixAction M → List M → List M

Apply an affix action to a material sequence.

Equations

• (Morphology.PFM.AffixAction.pre m).applyList x✝ = m :: x✝
• (Morphology.PFM.AffixAction.suf m).applyList x✝ = x✝ ++ [m]

def Morphology.PFM.AffixAction.toTreeAction {M : Type u_1} {P : Type u_3} (a : AffixAction M) : Action (Word.Tree M) P

The engine interpretation at tree-valued state.

Equations

• a.toTreeAction = Morphology.PFM.Action.const a.apply

def Morphology.PFM.AffixAction.toAction {M : Type u_1} {P : Type u_3} (a : AffixAction M) : Action (List M) P

The engine interpretation at material sequences.

Equations

• a.toAction = Morphology.PFM.Action.const a.applyList

theorem Morphology.PFM.AffixAction.toList_apply {M : Type u_1} (a : AffixAction M) (t : Word.Tree M) : (a.apply t).toList = a.applyList t.toList

theorem Morphology.PFM.AffixAction.apply_stem {M : Type u_1} {infl : M → Bool} (a : AffixAction M) (t : Word.Tree M) (h : infl a.material = true) : Word.Tree.stem infl (a.apply t) = Word.Tree.stem infl t

def Morphology.PFM.AffixAction.KindCoherent : AffixAction Morph → Prop

The affix is bound on the side apply places it.

Equations

• (Morphology.PFM.AffixAction.pre m).KindCoherent = (m.side? = some Morphology.Morph.Side.before)
• (Morphology.PFM.AffixAction.suf m).KindCoherent = (m.side? = some Morphology.Morph.Side.after)

theorem Morphology.PFM.AffixAction.apply_isKindCoherent {a : AffixAction Morph} (ha : a.KindCoherent) {t : Word.Tree Morph} (ht : t.IsKindCoherent) : (a.apply t).IsKindCoherent

The tree-valued run

theorem Morphology.PFM.toList_evalBlockForm {M : Type u_1} {L : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (LindexZ : List M → L) (b : List (Rule L P (AffixAction M))) (t : Word.Tree M) (σ : P) : (evalBlockForm (fun (t : Word.Tree M) => LindexZ t.toList) (List.map (Rule.mapPayload AffixAction.toTreeAction) b) (t, σ)).toList = evalBlockForm LindexZ (List.map (Rule.mapPayload AffixAction.toAction) b) (t.toList, σ)

theorem Morphology.PFM.stem_evalBlockForm {M : Type u_1} {L : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] {infl : M → Bool} (LindexZ : List M → L) (b : List (Rule L P (AffixAction M))) (hb : ∀ r ∈ b, infl r.payload.material = true) (t : Word.Tree M) (σ : P) : Word.Tree.stem infl (evalBlockForm (fun (t : Word.Tree M) => LindexZ t.toList) (List.map (Rule.mapPayload AffixAction.toTreeAction) b) (t, σ)) = Word.Tree.stem infl t

theorem Morphology.PFM.isKindCoherent_evalBlockForm {L : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (LindexZ : List Morph → L) (b : List (Rule L P (AffixAction Morph))) (hb : ∀ r ∈ b, r.payload.KindCoherent) (t : Word.Tree Morph) (ht : t.IsKindCoherent) (σ : P) : (evalBlockForm (fun (t : Word.Tree Morph) => LindexZ t.toList) (List.map (Rule.mapPayload AffixAction.toTreeAction) b) (t, σ)).IsKindCoherent

theorem Morphology.PFM.toList_blocksEval {M : Type u_1} {L : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (LindexZ : List M → L) (blocks : List (List (Rule L P (AffixAction M)))) (t : Word.Tree M) (σ : P) : (blocksEval (fun (t : Word.Tree M) => LindexZ t.toList) (List.map (List.map (Rule.mapPayload AffixAction.toTreeAction)) blocks) (t, σ)).1.toList = (blocksEval LindexZ (List.map (List.map (Rule.mapPayload AffixAction.toAction)) blocks) (t.toList, σ)).1

theorem Morphology.PFM.toList_paradigmFunction_tree {M : Type u_1} {L : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (LindexZ : List M → L) (blocks : List (List (Rule L P (AffixAction M)))) (stemLeaf : L × P → M) (c : L × P) : (paradigmFunction (fun (t : Word.Tree M) => LindexZ t.toList) (fun (c : L × P) => Word.Tree.root (stemLeaf c)) (List.map (List.map (Rule.mapPayload AffixAction.toTreeAction)) blocks) c).1.toList = (paradigmFunction LindexZ (fun (c : L × P) => [stemLeaf c]) (List.map (List.map (Rule.mapPayload AffixAction.toAction)) blocks) c).1

The tree-valued run linearizes to the sequence-valued run: the recorded structure is what the engine did.

theorem Morphology.PFM.stem_blocksEval {M : Type u_1} {L : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (LindexZ : List M → L) (blocks : List (List (Rule L P (AffixAction M)))) {infl : M → Bool} (hbs : ∀ b ∈ blocks, ∀ r ∈ b, infl r.payload.material = true) (t : Word.Tree M) (σ : P) : Word.Tree.stem infl (blocksEval (fun (t : Word.Tree M) => LindexZ t.toList) (List.map (List.map (Rule.mapPayload AffixAction.toTreeAction)) blocks) (t, σ)).1 = Word.Tree.stem infl t

theorem Morphology.PFM.stem_paradigmFunction_tree {M : Type u_1} {L : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (LindexZ : List M → L) (blocks : List (List (Rule L P (AffixAction M)))) {infl : M → Bool} (stemLeaf : L × P → M) (hbs : ∀ b ∈ blocks, ∀ r ∈ b, infl r.payload.material = true) (c : L × P) : Word.Tree.stem infl (paradigmFunction (fun (t : Word.Tree M) => LindexZ t.toList) (fun (c : L × P) => Word.Tree.root (stemLeaf c)) (List.map (List.map (Rule.mapPayload AffixAction.toTreeAction)) blocks) c).1 = Word.Tree.root (stemLeaf c)

Under any classification counting the vocabulary's material as inflectional, the tree-valued run's stem is the chosen leaf.

theorem Morphology.PFM.isKindCoherent_blocksEval {L : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (LindexZ : List Morph → L) (blocks : List (List (Rule L P (AffixAction Morph)))) (hbs : ∀ b ∈ blocks, ∀ r ∈ b, r.payload.KindCoherent) (t : Word.Tree Morph) (ht : t.IsKindCoherent) (σ : P) : (blocksEval (fun (t : Word.Tree Morph) => LindexZ t.toList) (List.map (List.map (Rule.mapPayload AffixAction.toTreeAction)) blocks) (t, σ)).1.IsKindCoherent

theorem Morphology.PFM.isKindCoherent_paradigmFunction_tree {L : Type u_2} {P : Type u_3} [PartialOrder P] [DecidableEq L] [DecidableLE P] (LindexZ : List Morph → L) (blocks : List (List (Rule L P (AffixAction Morph)))) (stemLeaf : L × P → Morph) (hbs : ∀ b ∈ blocks, ∀ r ∈ b, r.payload.KindCoherent) (hstem : ∀ (c : L × P), (stemLeaf c).kind = Morph.Kind.root ∨ (stemLeaf c).kind = Morph.Kind.free) (c : L × P) : (paradigmFunction (fun (t : Word.Tree Morph) => LindexZ t.toList) (fun (c : L × P) => Word.Tree.root (stemLeaf c)) (List.map (List.map (Rule.mapPayload AffixAction.toTreeAction)) blocks) c).1.IsKindCoherent

A kind-coherent vocabulary over a root-or-free stem leaf emits a kind-coherent tree.