Constructional schemas

A schema in the sense of [JA20] is a lexical entry with variables: a slot-indexed description body : V → α over a bundle of typed slots, together with the subset opens of slots marked open. A slot pinned above ⊥ is a constant; a slot at ⊥ is a variable, open (freely fillable) or closed (a learned list of fillers). Instantiation is domination in the pointwise order (Schema.Instantiates), which is unification against the description (instantiates_iff_unify, wiring to Core.Order.PartialUnify).

The relational and generative roles a schema can play ([JA20] §2.11) are lexicon-relative: over a stored lexicon Λ, Relates records a schema motivating a stored item, Generates licenses a possibly-novel item whose closed slots stay within the fillers attested in Λ. A closed variable's filler list is not a second stipulated field — it is derived from Λ, since nonproductive schemas have all their instances listed in the lexicon. generates_relates_insert is the memory-collapse step of that section's argument: a generated word, once committed to memory, falls under the schema's relational role.

Structural intersection is the pointwise meet (instantiates_inf); the least general generalization of a filler set is the dual of unification ([Plo70]'s lgg, [AH03]'s minimal generalization), recorded here as the order-theoretic content without minting new algebra.

Main declarations

• Schema — a slot-indexed description with an open-variable set
• Schema.Instantiates, instantiates_iff_unify — domination as unification
• Schema.attested, Schema.Relates, Schema.Generates — lexicon-relative roles
• Schema.instantiates_relates_insert, Schema.generates_relates_insert — the memory-collapse step
• Schema.IsProductive, Schema.IsProductive.generates_of_instantiates — a fully open schema generates any instance
• Schema.instantiates_inf — structural intersection is instantiated by each conjunct

structure Morphology.Construction.Schema (V : Type u_3) (α : Type u_4) [PartialOrder α] : Type (max u_3 u_4)

A schema: a slot-indexed description body, with opens the slots marked as open variables. A slot at ⊥ is a variable; a slot above ⊥ is a constant.

• body : V → α

  The slot-indexed description.

• opens : Set V

  The slots marked as open variables.

def Morphology.Construction.Schema.Instantiates {V : Type u_1} {α : Type u_2} [PartialOrder α] (s : Schema V α) (w : V → α) : Prop

A schema is instantiated by a filling w when its description dominates w slot-by-slot: every pinned slot's constraint is met and variables are free.

Equations

• s.Instantiates w = (s.body ≤ w)

theorem Morphology.Construction.Schema.instantiates_iff_unify {V : Type u_1} {α : Type u_2} [PartialOrder α] [Fintype V] [PartialUnify α] {s : Schema V α} {w : V → α} : s.Instantiates w ↔ PartialUnify.unify s.body w = some w

Instantiation is unification against the description: w instantiates s exactly when unifying the description with w succeeds and returns w.

def Morphology.Construction.Schema.attested {V : Type u_1} {α : Type u_2} [PartialOrder α] (s : Schema V α) (Λ : Set (V → α)) (v : V) : Set α

The fillers attested at a slot: the values a stored instance of s in Λ takes there. A closed variable's filler list, derived from storage rather than stipulated separately.

Equations

• s.attested Λ v = {a : α | ∃ w ∈ Λ, s.Instantiates w ∧ w v = a}

def Morphology.Construction.Schema.Relates {V : Type u_1} {α : Type u_2} [PartialOrder α] (s : Schema V α) (Λ : Set (V → α)) (w : V → α) : Prop

The relational role ([JA20] §2.11): s motivates the stored item w.

Equations

• s.Relates Λ w = (w ∈ Λ ∧ s.Instantiates w)

def Morphology.Construction.Schema.Generates {V : Type u_1} {α : Type u_2} [PartialOrder α] (s : Schema V α) (Λ : Set (V → α)) (w : V → α) : Prop

The generative role ([JA20] §2.11): s licenses a possibly-novel item w whose closed slots take only attested fillers.

Equations

• s.Generates Λ w = (s.Instantiates w ∧ ∀ v ∉ s.opens, w v ∈ s.attested Λ v)

theorem Morphology.Construction.Schema.instantiates_relates_insert {V : Type u_1} {α : Type u_2} [PartialOrder α] {s : Schema V α} {Λ : Set (V → α)} {w : V → α} (h : s.Instantiates w) : s.Relates (insert w Λ) w

Any instance, once added to the lexicon, is related by the schema.

theorem Morphology.Construction.Schema.generates_relates_insert {V : Type u_1} {α : Type u_2} [PartialOrder α] {s : Schema V α} {Λ : Set (V → α)} {w : V → α} (h : s.Generates Λ w) : s.Relates (insert w Λ) w

The memory-collapse step of [JA20]'s §2.11 argument: a generated word, once committed to memory, falls under the schema's relational role.

def Morphology.Construction.Schema.IsProductive {V : Type u_1} {α : Type u_2} [PartialOrder α] (s : Schema V α) : Prop

A schema is productive when every slot is open — a fully general pattern with no learned filler lists.

Equations

• s.IsProductive = ∀ (v : V), v ∈ s.opens

theorem Morphology.Construction.Schema.IsProductive.generates_of_instantiates {V : Type u_1} {α : Type u_2} [PartialOrder α] {s : Schema V α} {Λ : Set (V → α)} {w : V → α} (hp : s.IsProductive) (h : s.Instantiates w) : s.Generates Λ w

A productive schema generates every instance ([JA20]: a productive schema has "gone viral"), since it has no closed slots to confine.

theorem Morphology.Construction.Schema.instantiates_inf {V : Type u_1} {α : Type u_2} [SemilatticeInf α] {w₁ w₂ : V → α} {opens : Set V} : { body := w₁ ⊓ w₂, opens := opens }.Instantiates w₁

Structural intersection is instantiated by each conjunct: the pointwise meet of two fillers is a schema they both instantiate — the lower-bound face of the least general generalization.

Productivity is a genuine restriction

A schema with a closed slot relates its stored instance but cannot generate a fresh filler for that slot. Generation over the function type V → α is an existential with no Decidable instance, so nonproductivity is witnessed structurally.