Constructional inheritance

Computational content for the two modes of constructional inheritance distinguished by [Gol95] §3.3.1 (the InheritanceMode enum in ConstructionGrammar.Basic), grounded in the flat feature-slot order: in the complete mode representations must strictly unify (Compat, PartialUnify.unify — the regime [KF99] built their formal CxG on and [Sag12]'s SBCG inherits from HPSG), while in the default mode the inheriting construction overrides its parents ([Die23] Table 2; the default-unification tradition of [LC99]): inheritField is the priority union (Flat.or) of the child's slot with its parents' unification (PartialUnify.unifyList), so a parental conflict the child does not legislate leaves the slot unspecified.

Main declarations

• inheritField, ResolvesField: default-mode slot semantics
• inheritField_of_compat: the two modes agree absent conflict
• Constructicon.parentsOf, derivedSpec, ResolvesAll, WellFormed: inheritance computed through a constructicon's links, generic in the specification type
• inheritFieldUnique, Constructicon.derivedField: inheritance for slots without decidable equality (e.g. denotations)

Default-mode slot algebra

A specification slot is a Flat-ordered partial value: ⊥ is "unspecified", and inheritance fills unspecified slots from parents.

def ConstructionGrammar.inheritField {α : Type u_1} [DecidableEq α] (own : Flat α) (parents : List (Flat α)) : Flat α

Normal-mode (default) inheritance for one slot ([Gol95] §3.3.1; [Die23] Table 2: "low-level representations override high-level representations if there is a conflict"; [LC99]): the inheriting construction's own value wins; an unspecified slot takes its parents' unification when it exists; a parental conflict the child does not legislate leaves the slot unspecified.

Equations

• ConstructionGrammar.inheritField own parents = own.or ((PartialUnify.unifyList parents).getD ⊥)

def ConstructionGrammar.ResolvesField {α : Type u_1} [DecidableEq α] (own : Flat α) (parents : List (Flat α)) : Prop

The child legislates wherever its parents conflict — [Gol95]'s normal mode: "conflicts are addressed by the inheriting construction, which specifies its own constraints".

Equations

• ConstructionGrammar.ResolvesField own parents = (PartialUnify.unifyList parents = none → own ≠ ⊥)

@[instance_reducible]

instance ConstructionGrammar.instDecidableResolvesField {α : Type u_1} [DecidableEq α] (own : Flat α) (parents : List (Flat α)) : Decidable (ResolvesField own parents)

Equations

• ConstructionGrammar.instDecidableResolvesField own parents = ConstructionGrammar.instDecidableResolvesField._aux_1 own parents

@[simp]

theorem ConstructionGrammar.inheritField_coe {α : Type u_1} [DecidableEq α] (a : α) (parents : List (Flat α)) : inheritField (↑a) parents = ↑a

@[simp]

theorem ConstructionGrammar.inheritField_nil {α : Type u_1} [DecidableEq α] (own : Flat α) : inheritField own [] = own

theorem ConstructionGrammar.inheritField_of_compat {α : Type u_1} [DecidableEq α] (own : Flat α) {p q : Flat α} (h : Compat p q) : inheritField own [p, q] = (own.or p).or q

Absent conflict, normal-mode inheritance agrees with strict (complete-mode) unification: with compatible parents the inherited value is the priority union of child and parents. Normal mode departs from complete inheritance only at genuine conflicts.

theorem ConstructionGrammar.resolvesField_of_compat {α : Type u_1} [DecidableEq α] (own : Flat α) {p q : Flat α} (h : Compat p q) : ResolvesField own [p, q]

Compatible parents impose no resolution burden on the child.

Inheritance through a constructicon

A specification assignment maps each construction to its own (conflict-resolving) specification; the network then computes each construction's full specification by normal-mode inheritance from the parents its links name. The walk is generic in the specification type: record-valued specifications supply their componentwise inherit and Resolves lifts.

def ConstructionGrammar.Constructicon.parentsOf {Sem : Type u_1} (cx : Constructicon Sem) (name : String) : List (Construction Sem)

The constructions a network's links name as parents of name.

Equations

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

def ConstructionGrammar.Constructicon.childrenOf {Sem : Type u_1} (cx : Constructicon Sem) (name : String) : List (Construction Sem)

The constructions a network's links name as children of name.

Equations

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

def ConstructionGrammar.Constructicon.WellFormed {Sem : Type u_1} (cx : Constructicon Sem) : Prop

Every link endpoint resolves to a construction in the network — no dangling name-keyed links.

Equations

• cx.WellFormed = ∀ l ∈ cx.links, (∃ c ∈ cx.constructions, c.name = l.parent) ∧ ∃ c ∈ cx.constructions, c.name = l.child

@[instance_reducible]

instance ConstructionGrammar.instDecidableWellFormed {Sem : Type u_1} (cx : Constructicon Sem) : Decidable cx.WellFormed

Equations

• ConstructionGrammar.instDecidableWellFormed cx = ConstructionGrammar.instDecidableWellFormed._aux_1 cx

def ConstructionGrammar.Constructicon.derivedSpec {Sem : Type u_1} {σ : Type u_2} (cx : Constructicon Sem) (inherit : σ → List σ → σ) (own : Construction Sem → σ) (c : Construction Sem) : σ

Normal-mode derived specification of c in the network: c's own specification wins; fields it leaves open are filled from the parents its links name ([Die23] Table 2's default mode, computed over the links rather than stipulated per node).

Equations

• cx.derivedSpec inherit own c = inherit (own c) (List.map own (cx.parentsOf c.name))

def ConstructionGrammar.Constructicon.ResolvesAll {Sem : Type u_1} {σ : Type u_2} (cx : Constructicon Sem) (resolves : σ → List σ → Prop) (own : Construction Sem → σ) : Prop

Normal-mode well-formedness of the whole network: every construction legislates every field its parents conflict on.

Equations

• cx.ResolvesAll resolves own = ∀ c ∈ cx.constructions, resolves (own c) (List.map own (cx.parentsOf c.name))

@[instance_reducible]

instance ConstructionGrammar.instDecidableResolvesAll {Sem : Type u_1} {σ : Type u_2} (cx : Constructicon Sem) (resolves : σ → List σ → Prop) [(o : σ) → (ps : List σ) → Decidable (resolves o ps)] (own : Construction Sem → σ) : Decidable (cx.ResolvesAll resolves own)

Equations

• ConstructionGrammar.instDecidableResolvesAll cx resolves own = ConstructionGrammar.instDecidableResolvesAll._aux_1 cx resolves own

Inheritance of denotation-valued fields

Denotations (e.g. PartialProp-valued pragmatic contributions) have no decidable equality, so agreeing parents cannot be reconciled by unification. inheritFieldUnique inherits when exactly one parent supplies a value — sufficient for single-mother inheritance, the configuration of conventional-subtype links.

def ConstructionGrammar.inheritFieldUnique {α : Type u_3} (own : Option α) (parents : List (Option α)) : Option α

Normal-mode inheritance for one field without decidable equality: the child's own value wins; an unspecified field takes the value of the unique supplying parent; multiple suppliers (which inheritField could reconcile when they agree) yield none.

Equations

• ConstructionGrammar.inheritFieldUnique (some x_1) parents = some x_1
• ConstructionGrammar.inheritFieldUnique none parents = some x_1
• ConstructionGrammar.inheritFieldUnique none parents = none

def ConstructionGrammar.Constructicon.derivedField {Sem : Type u_1} {α : Type u_3} (cx : Constructicon Sem) (own : Construction Sem → Option α) (c : Construction Sem) : Option α

Derived value of a denotation-valued field for c in the network: c's own value wins; otherwise the value of the unique supplying parent.

Equations

• cx.derivedField own c = ConstructionGrammar.inheritFieldUnique (own c) (List.map own (cx.parentsOf c.name))