Templates: word-skeletal morphotactic substrate

A template stipulates a word's positional skeleton directly — the word-skeletal answer to where affix order comes from, rival to the rule-combining answer on which templates are emergent patterns of rule composition ([stump-2022]). The layered-vs-templatic typological contrast and its diagnostics (long-distance slot dependencies, non-functional slot assignment) are [bickel-nichols-2007] §6, with the caveat that templatic vs layered properties "are likely to hold of individual formatives rather than of the entire string" (p. 219). AffixTemplate is the position-class species (a prosodic/CV species would be its sibling); the rivalry itself is study content, not settled here.

A word's affix template: the ordered position-class slots of its prefix and suffix strings, parameterized by the slot type Slot — so the order lives once, as Fragment data, and study files derive their checks from it rather than re-typing the template. Instantiating at MorphCategory (Morphology/RelevanceHierarchy.lean) gives a language's slot order in relevance-hierarchy vocabulary; a language-specific slot type carries finer position classes: Mayan.template uses Mayan.VerbSlot, with the prefix/suffix split encoding a morpheme's position relative to the verb stem.

Main definitions

• Morphology.AffixTemplate — a word's prefix/suffix slots over an arbitrary slot type.
• Morphology.PositionClassSystem — a template with the exponents of each slot, and the slots that may be filled more than once; PositionClassSystem.Licenses is the affix strings it admits.

structure Morphology.AffixTemplate (Slot : Type u_1) : Type u_1

A word's affix position-class template. suffixSlots runs stem-outward (innermost suffix first); prefixSlots is listed as the source grammar writes it, word-edge inward. Slots are Slot tags, not exponents — the actual morphemes live in the citing grammar.

• prefixSlots : List Slot

  Prefix slots, ordered word-edge inward (outermost prefix first).

• suffixSlots : List Slot

  Suffix slots, ordered stem-outward (innermost suffix first).

def Morphology.instReprAffixTemplate.repr {Slot✝ : Type u_1} [Repr Slot✝] : AffixTemplate Slot✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.instReprAffixTemplate {Slot✝ : Type u_1} [Repr Slot✝] : Repr (AffixTemplate Slot✝)

Equations

• Morphology.instReprAffixTemplate = { reprPrec := Morphology.instReprAffixTemplate.repr }

@[instance_reducible]

instance Morphology.instDecidableEqAffixTemplate {Slot✝ : Type u_1} [DecidableEq Slot✝] : DecidableEq (AffixTemplate Slot✝)

Equations

• Morphology.instDecidableEqAffixTemplate = Morphology.instDecidableEqAffixTemplate.decEq

def Morphology.instDecidableEqAffixTemplate.decEq {Slot✝ : Type u_1} [DecidableEq Slot✝] (x✝ x✝¹ : AffixTemplate Slot✝) : Decidable (x✝ = x✝¹)

Equations

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

Position-class systems

structure Morphology.PositionClassSystem : Type (u + 1)

A position-class system: a slot inventory ordered by an affix template, the exponents of each slot, and the slots that may be filled by several exponents in sequence. The exponents are abstract symbols, as the symbols of a FirstOrder.Language are; their forms are an interpretation supplied by the citing grammar.

• Slot : Type u

  The position classes.

• decEq : DecidableEq self.Slot
• template : AffixTemplate self.Slot

  Their order.

• Exponent : self.Slot → Type u

  The exponents of each slot.

• Iterable : self.Slot → Prop

  The slots admitting more than one exponent in sequence.

• decIterable : DecidablePred self.Iterable

def Morphology.PositionClassSystem.Precedes (P : PositionClassSystem) (slots : List P.Slot) (a b : P.Slot) : Prop

In the slot order slots, b may follow a: a later slot, or the same iterable slot.

Equations

• P.Precedes slots a b = (List.idxOf a slots < List.idxOf b slots ∨ a = b ∧ P.Iterable a)

@[instance_reducible]

instance Morphology.PositionClassSystem.instDecidableRelSlotPrecedes (P : PositionClassSystem) (slots : List P.Slot) : DecidableRel (P.Precedes slots)

Equations

• P.instDecidableRelSlotPrecedes slots x✝¹ x✝ = Morphology.PositionClassSystem.instDecidableRelSlotPrecedes._aux_1 P slots x✝¹ x✝

def Morphology.PositionClassSystem.LicensesIn (P : PositionClassSystem) (slots : List P.Slot) (w : List ((s : P.Slot) × P.Exponent s)) : Prop

The affix strings admitted in the slot order slots: every exponent in one of its slots, consecutive exponents in later or iterable slots.

Equations

• P.LicensesIn slots w = ((∀ (x : (s : P.Slot) × P.Exponent s), x ∈ w → x.fst ∈ slots) ∧ List.IsChain (P.Precedes slots) (List.map Sigma.fst w))

@[instance_reducible]

instance Morphology.PositionClassSystem.instDecidableLicensesIn (P : PositionClassSystem) (slots : List P.Slot) (w : List ((s : P.Slot) × P.Exponent s)) : Decidable (P.LicensesIn slots w)

Equations

• P.instDecidableLicensesIn slots w = Morphology.PositionClassSystem.instDecidableLicensesIn._aux_1 P slots w

def Morphology.PositionClassSystem.Licenses (P : PositionClassSystem) (pre suf : List ((s : P.Slot) × P.Exponent s)) : Prop

The words the system admits: the prefixes licensed in the prefix order and the suffixes in the suffix order.

Equations

• P.Licenses pre suf = (P.LicensesIn P.template.prefixSlots pre ∧ P.LicensesIn P.template.suffixSlots suf)

@[instance_reducible]

instance Morphology.PositionClassSystem.instDecidableLicenses (P : PositionClassSystem) (pre suf : List ((s : P.Slot) × P.Exponent s)) : Decidable (P.Licenses pre suf)

Equations

• P.instDecidableLicenses pre suf = Morphology.PositionClassSystem.instDecidableLicenses._aux_1 P pre suf

theorem Morphology.PositionClassSystem.not_licensesIn_pair (P : PositionClassSystem) {s : P.Slot} (h : ¬P.Iterable s) (slots : List P.Slot) (e₁ e₂ : P.Exponent s) : ¬P.LicensesIn slots [⟨s, e₁⟩, ⟨s, e₂⟩]

Two exponents of one slot cannot be adjacent unless the slot is iterable.