Constructional schemas

This file defines the schemas of Relational Morphology and Construction Morphology, lexical entries with variables. A schema is a description indexed by slots, valued in a partial order with a bottom element, together with the set of slots marked as open variables. A slot above ⊥ is a constant and a slot at ⊥ is a variable, open or closed. An item instantiates a schema when the description lies below it slot by slot, so the instances of a schema form the principal upper set of its description, and instantiation is unification against the description.

A description over variables is read at positions through a subscripting of positions by variables. Positions with the same subscript are coindexed and must be filled alike, so an item over positions instantiates a schema when it is an instance read through the subscripting. Two items are a paired instantiation, sister items, when their sum instantiates the schema through the sum of their subscriptings; the relation is symmetric.

A schema plays two roles relative to a lexicon of stored items. In its relational role it motivates an item already stored; in its generative role it licenses a possibly novel item whose closed variables take only fillers attested among the stored instances. Every related item is generated, every generated item is related once stored, and a schema is productive, every variable open, exactly when it generates its own description over the empty lexicon.

Two items over one position space are the same except at a set of positions when they agree off it, Set.EqOn on the complement, and what happens at those positions classifies the link between them: an instantiation when the second strictly dominates the first there, the link from a schema's description to its instances, and a contrast when the two are incompatible there, the link between sister words. An elaboration, one item the same as the other plus something else, is an instantiation read from the elaborated item. On a flat carrier a filled item instantiates a schema exactly when it is the description, the same except at the variables (Schema.instantiates_iff_instantiation_of_forall_isMax).

Main declarations

• Schema: a slot-indexed description with a set of open variables.
• Schema.Instantiates, Schema.instantiates_iff_unify: instantiation as pointwise domination, equivalently as unification.
• Schema.InstantiatesAt, Schema.instantiatesAt_iff: instantiation at positions through a subscripting, as instantiation of the pulled-back description together with agreement at coindexed positions.
• Schema.productive, Schema.Relates, Schema.Generates, Schema.IsProductive: the schema with every variable open, the two roles of a schema, and productivity; Schema.generates_iff_mem_pi: what a schema generates is the product of its slotwise fillers.
• Instantiation, Contrast: the relational links, same except at a set of positions.
• Schema.instantiates_inf_iff, Schema.instantiates_iff_of_unify_eq_some: the meet of two items is their least general generalization, the Structural Intersection of Relational Morphology, and the unification of two descriptions has exactly their common instances.

Implementation notes

Productivity is a property of variables rather than of a schema as a whole, so constants are exempt from attestation and Schema.IsProductive is the case in which every variable is open. Marking a constant slot as open has no effect.

References

• [jackendoff-audring-2020]
• [culicover-jackendoff-2012]
• [booij-2010]
• [booij-2010-compass]
• [plotkin-1970]
• [albright-hayes-2003]

structure ConstructionMorphology.Schema (V : Type u_7) (α : Type u_8) : Type (max u_7 u_8)

A schema is a slot-indexed description body together with a set opens of slots marked as open variables. A slot at ⊥ is a variable and a slot above ⊥ is a constant.

• body : V → α

  The slot-indexed description.

• opens : Set V

  The slots marked as open variables.

theorem ConstructionMorphology.Schema.ext {V : Type u_7} {α : Type u_8} {x y : Schema V α} (body : x.body = y.body) (opens : x.opens = y.opens) : x = y

theorem ConstructionMorphology.Schema.ext_iff {V : Type u_7} {α : Type u_8} {x y : Schema V α} : x = y ↔ x.body = y.body ∧ x.opens = y.opens

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

An item w instantiates a schema s if the description of s lies below w slot by slot: each constant is matched and each variable is filled freely.

Equations

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

@[instance_reducible]

instance ConstructionMorphology.Schema.decidablePredInstantiates {V : Type u_1} {α : Type u_6} [PartialOrder α] [DecidableLE (V → α)] (s : Schema V α) : DecidablePred s.Instantiates

Equations

• s.decidablePredInstantiates w = ConstructionMorphology.Schema.decidablePredInstantiates._aux_1 s w

theorem ConstructionMorphology.Schema.instantiates_body {V : Type u_1} {α : Type u_6} [PartialOrder α] (s : Schema V α) : s.Instantiates s.body

A schema instantiates its own description.

theorem ConstructionMorphology.Schema.Instantiates.trans_le {V : Type u_1} {α : Type u_6} [PartialOrder α] {s : Schema V α} {w₁ w₂ : V → α} (h : s.Instantiates w₁) (hw : w₁ ≤ w₂) : s.Instantiates w₂

The instances of a schema form an upper set.

theorem ConstructionMorphology.Schema.instantiates_iff_eq_of_forall_isMax {V : Type u_1} {α : Type u_6} [PartialOrder α] {s : Schema V α} {w : V → α} (h : ∀ (v : V), IsMax (s.body v)) : s.Instantiates w ↔ w = s.body

A fully specified description, every slot maximal, is instantiated by itself alone.

theorem ConstructionMorphology.Schema.body_le_body_iff {V : Type u_1} {α : Type u_6} [PartialOrder α] {s t : Schema V α} : t.body ≤ s.body ↔ ∀ ⦃w : V → α⦄, s.Instantiates w → t.Instantiates w

A schema lies below another exactly when it is instantiated by everything the other is.

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

An item instantiates a schema exactly when unifying it with the description returns the item.

theorem ConstructionMorphology.Schema.instantiates_iff_of_unify_eq_some {V : Type u_1} {α : Type u_6} [PartialOrder α] {s t : Schema V α} {w : V → α} [Fintype V] [PartialUnify α] {u : Schema V α} (h : PartialUnify.unify s.body t.body = some u.body) : u.Instantiates w ↔ s.Instantiates w ∧ t.Instantiates w

The instances of a unified description are the common instances of its two conjuncts.

Positions and coindexation

def ConstructionMorphology.Schema.comap {V : Type u_1} {P : Type u_2} {α : Type u_6} (s : Schema V α) (pos : P → V) : Schema P α

The schema s read at positions through the subscripting pos, with coindexation forgotten: the description and the open variables pulled back along pos.

Equations

• s.comap pos = { body := s.body ∘ pos, opens := pos ⁻¹' s.opens }

@[simp]

theorem ConstructionMorphology.Schema.comap_body {V : Type u_1} {P : Type u_2} {α : Type u_6} (s : Schema V α) (pos : P → V) : (s.comap pos).body = s.body ∘ pos

@[simp]

theorem ConstructionMorphology.Schema.comap_opens {V : Type u_1} {P : Type u_2} {α : Type u_6} (s : Schema V α) (pos : P → V) : (s.comap pos).opens = pos ⁻¹' s.opens

def ConstructionMorphology.Schema.InstantiatesAt {V : Type u_1} {P : Type u_2} {α : Type u_6} [PartialOrder α] (s : Schema V α) (pos : P → V) (w : P → α) : Prop

An item w over positions instantiates a schema s through the subscripting pos if w is an instance of s read at the positions: w = u ∘ pos for some instance u.

Equations

• s.InstantiatesAt pos w = ∃ (u : V → α), s.Instantiates u ∧ w = u ∘ pos

theorem ConstructionMorphology.Schema.Instantiates.instantiatesAt {V : Type u_1} {P : Type u_2} {α : Type u_6} [PartialOrder α] {s : Schema V α} {u : V → α} (h : s.Instantiates u) (pos : P → V) : s.InstantiatesAt pos (u ∘ pos)

@[simp]

theorem ConstructionMorphology.Schema.instantiatesAt_id {V : Type u_1} {α : Type u_6} [PartialOrder α] {s : Schema V α} {w : V → α} : s.InstantiatesAt id w ↔ s.Instantiates w

theorem ConstructionMorphology.Schema.instantiatesAt_iff {V : Type u_1} {P : Type u_2} {α : Type u_6} [PartialOrder α] {s : Schema V α} {pos : P → V} {w : P → α} : s.InstantiatesAt pos w ↔ (s.comap pos).Instantiates w ∧ Function.FactorsThrough w pos

An item instantiates a schema through a subscripting exactly when it instantiates the pulled-back description and fills coindexed positions alike.

theorem ConstructionMorphology.Schema.instantiatesAt_comp_equiv {V : Type u_1} {P : Type u_2} {Q : Type u_3} {α : Type u_6} [PartialOrder α] {s : Schema V α} {pos : P → V} {w : P → α} (e : Q ≃ P) : s.InstantiatesAt (pos ∘ ⇑e) (w ∘ ⇑e) ↔ s.InstantiatesAt pos w

Instantiation through a subscripting is invariant under reindexing the positions.

theorem ConstructionMorphology.Schema.instantiatesAt_elim_iff {V : Type u_1} {P₁ : Type u_4} {P₂ : Type u_5} {α : Type u_6} [PartialOrder α] {s : Schema V α} {pos₁ : P₁ → V} {pos₂ : P₂ → V} {w₁ : P₁ → α} {w₂ : P₂ → α} : s.InstantiatesAt (Sum.elim pos₁ pos₂) (Sum.elim w₁ w₂) ↔ (s.comap pos₁).Instantiates w₁ ∧ (s.comap pos₂).Instantiates w₂ ∧ Function.FactorsThrough w₁ pos₁ ∧ Function.FactorsThrough w₂ pos₂ ∧ ∀ (a : P₁) (b : P₂), pos₁ a = pos₂ b → w₁ a = w₂ b

Two items are a paired instantiation through their subscriptings exactly when each instantiates its pulled-back description, each fills its own coindexed positions alike, and the two agree wherever their subscripts coincide.

theorem ConstructionMorphology.Schema.instantiatesAt_elim_swap {V : Type u_1} {P₁ : Type u_4} {P₂ : Type u_5} {α : Type u_6} [PartialOrder α] {s : Schema V α} {pos₁ : P₁ → V} {pos₂ : P₂ → V} {w₁ : P₁ → α} {w₂ : P₂ → α} : s.InstantiatesAt (Sum.elim pos₂ pos₁) (Sum.elim w₂ w₁) ↔ s.InstantiatesAt (Sum.elim pos₁ pos₂) (Sum.elim w₁ w₂)

A paired instantiation is symmetric: the sister relation has no direction.

theorem ConstructionMorphology.Schema.instantiatesAt_elim_iff_eqOn {V : Type u_1} {P : Type u_2} {α : Type u_6} [PartialOrder α] {s : Schema V α} {pos₁ pos₂ : P → V} {w₁ w₂ : P → α} {S : Set P} (h₁ : Function.Injective pos₁) (h₂ : Function.Injective pos₂) (h : ∀ (a b : P), pos₁ a = pos₂ b ↔ a = b ∧ a ∉ S) : s.InstantiatesAt (Sum.elim pos₁ pos₂) (Sum.elim w₁ w₂) ↔ (s.comap pos₁).Instantiates w₁ ∧ (s.comap pos₂).Instantiates w₂ ∧ Set.EqOn w₁ w₂ Sᶜ

Through injective subscriptings that coincide exactly off S, a paired instantiation is two instances of the pulled-back descriptions that are the same except at S.

The relational role

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

A schema s relates an item w over a lexicon Λ if w is stored in Λ and instantiates s: the relational role of a schema.

Equations

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

theorem ConstructionMorphology.Schema.Relates.instantiates {V : Type u_1} {α : Type u_6} [PartialOrder α] {s : Schema V α} {w : V → α} {Λ : Set (V → α)} (h : s.Relates Λ w) : s.Instantiates w

theorem ConstructionMorphology.Schema.Relates.mono {V : Type u_1} {α : Type u_6} [PartialOrder α] {s : Schema V α} {w : V → α} {Λ Λ' : Set (V → α)} (h : Λ ⊆ Λ') (hw : s.Relates Λ w) : s.Relates Λ' w

theorem ConstructionMorphology.Schema.Instantiates.relates_insert {V : Type u_1} {α : Type u_6} [PartialOrder α] {s : Schema V α} {w : V → α} {Λ : Set (V → α)} (h : s.Instantiates w) : s.Relates (insert w Λ) w

An instance, once stored, is related by the schema.

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

The fillers attested at a slot v are the values the stored instances of s take there: the filler list of a closed variable, derived from the lexicon rather than stipulated.

Equations

• s.attested Λ v = {a : α | ∃ (w : V → α), s.Relates Λ w ∧ w v = a}

@[simp]

theorem ConstructionMorphology.Schema.mem_attested {V : Type u_1} {α : Type u_6} [PartialOrder α] {s : Schema V α} {Λ : Set (V → α)} {v : V} {a : α} : a ∈ s.attested Λ v ↔ ∃ (w : V → α), s.Relates Λ w ∧ w v = a

theorem ConstructionMorphology.Schema.Relates.apply_mem_attested {V : Type u_1} {α : Type u_6} [PartialOrder α] {s : Schema V α} {w : V → α} {Λ : Set (V → α)} (h : s.Relates Λ w) (v : V) : w v ∈ s.attested Λ v

theorem ConstructionMorphology.Schema.attested_mono {V : Type u_1} {α : Type u_6} [PartialOrder α] {s : Schema V α} {Λ Λ' : Set (V → α)} (h : Λ ⊆ Λ') (v : V) : s.attested Λ v ⊆ s.attested Λ' v

theorem ConstructionMorphology.Schema.instantiates_inf_iff {V : Type u_1} {α : Type u_6} [SemilatticeInf α] {s : Schema V α} {w₁ w₂ : V → α} : s.Instantiates (w₁ ⊓ w₂) ↔ s.Instantiates w₁ ∧ s.Instantiates w₂

A schema is instantiated by the meet of two items exactly when it is instantiated by both: the meet is their least general generalization, the Structural Intersection of Relational Morphology.

The generative role

def ConstructionMorphology.Schema.productive {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] (body : V → α) : Schema V α

The schema with description body and every variable open.

Equations

• ConstructionMorphology.Schema.productive body = { body := body, opens := {v : V | body v = ⊥} }

@[simp]

theorem ConstructionMorphology.Schema.productive_body {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] (body : V → α) : (productive body).body = body

@[simp]

theorem ConstructionMorphology.Schema.productive_opens {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] (body : V → α) : (productive body).opens = {v : V | body v = ⊥}

def ConstructionMorphology.Schema.Generates {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] (s : Schema V α) (Λ : Set (V → α)) (w : V → α) : Prop

A schema s generates an item w over a lexicon Λ if w instantiates s and every closed variable of s, a slot at ⊥ not marked open, takes in w a filler attested in Λ: the generative role of a schema, licensing possibly novel items.

Equations

• s.Generates Λ w = (s.Instantiates w ∧ ∀ (v : V), s.body v = ⊥ → v ∉ s.opens → w v ∈ s.attested Λ v)

theorem ConstructionMorphology.Schema.Generates.instantiates {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] {s : Schema V α} {w : V → α} {Λ : Set (V → α)} (h : s.Generates Λ w) : s.Instantiates w

def ConstructionMorphology.Schema.fillers {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] (s : Schema V α) (Λ : Set (V → α)) (v : V) : Set α

The fillers a schema admits at a slot over a lexicon: anything above the description at an open variable, the attested fillers at a closed one, and whatever lies above a constant.

Equations

• s.fillers Λ v = {a : α | s.body v ≤ a ∧ (s.body v = ⊥ → v ∉ s.opens → a ∈ s.attested Λ v)}

theorem ConstructionMorphology.Schema.generates_iff_mem_pi {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] {s : Schema V α} {w : V → α} {Λ : Set (V → α)} : s.Generates Λ w ↔ w ∈ Set.univ.pi (s.fillers Λ)

The items a schema generates are the product of its slotwise filler sets.

theorem ConstructionMorphology.Schema.fillers_eq_singleton_of_forall_isMax {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] {s : Schema V α} {Λ : Set (V → α)} (hα : ∀ (a : α), a ≠ ⊥ → IsMax a) {v : V} (hv : s.body v ≠ ⊥) : s.fillers Λ v = {s.body v}

Where every value other than ⊥ is maximal, a constant admits only itself.

theorem ConstructionMorphology.Schema.Relates.generates {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] {s : Schema V α} {w : V → α} {Λ : Set (V → α)} (h : s.Relates Λ w) : s.Generates Λ w

A related item is generated, attesting its own fillers.

theorem ConstructionMorphology.Schema.Generates.relates_insert {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] {s : Schema V α} {w : V → α} {Λ : Set (V → α)} (h : s.Generates Λ w) : s.Relates (insert w Λ) w

A generated item, once stored, is related by the schema.

theorem ConstructionMorphology.Schema.Generates.mono {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] {s : Schema V α} {w : V → α} {Λ Λ' : Set (V → α)} (h : Λ ⊆ Λ') (hw : s.Generates Λ w) : s.Generates Λ' w

Generation is monotone in the lexicon.

def ConstructionMorphology.Schema.IsProductive {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] (s : Schema V α) : Prop

A schema is productive if every variable, every slot at ⊥, is open.

Equations

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

theorem ConstructionMorphology.Schema.isProductive_productive {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] (body : V → α) : (productive body).IsProductive

theorem ConstructionMorphology.Schema.IsProductive.generates_iff {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] {s : Schema V α} {w : V → α} {Λ : Set (V → α)} (hs : s.IsProductive) : s.Generates Λ w ↔ s.Instantiates w

A productive schema generates exactly its instances.

theorem ConstructionMorphology.Schema.isProductive_iff_generates_empty {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] {s : Schema V α} : s.IsProductive ↔ s.Generates ∅ s.body

A schema is productive exactly when it generates its own description over the empty lexicon.

theorem ConstructionMorphology.Schema.isProductive_iff_forall_generates_iff {V : Type u_1} {α : Type u_6} [PartialOrder α] [OrderBot α] {s : Schema V α} : s.IsProductive ↔ ∀ (Λ : Set (V → α)) (w : V → α), s.Generates Λ w ↔ s.Instantiates w

A schema generates every instance over every lexicon exactly when it is productive.

Relational links

Two items over one position space are the same except at S when they agree off S; what happens at S classifies the link.

def ConstructionMorphology.Instantiation {P : Type u_2} {α : Type u_6} [PartialOrder α] (f g : P → α) (S : Set P) : Prop

Instantiation f g S means that g is the same as f except at S, where it strictly dominates f: the relational link from a schema's description to its instances.

Equations

• ConstructionMorphology.Instantiation f g S = (Set.EqOn f g Sᶜ ∧ StrongLT (S.domRestrict f) (S.domRestrict g))

def ConstructionMorphology.Contrast {P : Type u_2} {α : Type u_6} [PartialOrder α] (f g : P → α) (S : Set P) : Prop

Contrast f g S means that f and g are the same except at S, where they are incompatible: the relational link between sister words.

Equations

• ConstructionMorphology.Contrast f g S = (Set.EqOn f g Sᶜ ∧ ∀ p ∈ S, ¬Compat (f p) (g p))

theorem ConstructionMorphology.Contrast.symm {P : Type u_2} {α : Type u_6} {f g : P → α} {S : Set P} [PartialOrder α] (h : Contrast f g S) : Contrast g f S

theorem ConstructionMorphology.Instantiation.instantiates {P : Type u_2} {α : Type u_6} {S : Set P} [PartialOrder α] {s : Schema P α} {w : P → α} (h : Instantiation s.body w S) : s.Instantiates w

An instantiation of a schema's description instantiates the schema.

theorem ConstructionMorphology.contrast_iff_of_forall_isMax {P : Type u_2} {α : Type u_6} {f g : P → α} {S : Set P} [PartialOrder α] [OrderBot α] (hα : ∀ (a : α), a ≠ ⊥ → IsMax a) : Contrast f g S ↔ Set.EqOn f g Sᶜ ∧ ∀ p ∈ S, f p ≠ ⊥ ∧ g p ≠ ⊥ ∧ f p ≠ g p

Where every value other than ⊥ is maximal, a contrast is two present and distinct values.

theorem ConstructionMorphology.Schema.instantiates_iff_instantiation_of_forall_isMax {P : Type u_2} {α : Type u_6} [PartialOrder α] [OrderBot α] (hα : ∀ (a : α), a ≠ ⊥ → IsMax a) {s : Schema P α} {w : P → α} (hw : ∀ (p : P), w p ≠ ⊥) : s.Instantiates w ↔ Instantiation s.body w {p : P | s.body p = ⊥}

On a flat carrier, a filled item instantiates a schema exactly when it is the schema's description, the same except at the variables.