Construction Grammar: Inheritance Modes

Computational content for the two modes of constructional inheritance distinguished by [Gol95] §3.3.1 (the InheritanceMode enum in ConstructionGrammar.Basic), following [Die23]'s Table 2: in the complete mode, "high- and low-level representations are fully compatible with each other" — the unification-based regime [KF99] built their formal CxG on and [Sag12]'s SBCG inherits from HPSG — while in the default mode "low-level representations override high-level representations if there is a conflict", with formal semantics in the default-unification tradition ([LC99]). Complete mode is defined exactly on IsCompatible inputs; default mode (inheritField) lets the child win, and under multiple inheritance (a child with two or more schematic parents, [Die23] §2.2.2) leaves a field unspecified when the parents conflict and the child does not legislate (ResolvesField).

[Die23]'s other axis — impoverished vs. full entry model, i.e. whether shared information is stored once or redundantly at every level — is a storage claim orthogonal to the inheritance algebra and is not formalized here.

Main declarations

• IsCompatible: two partial field values can strictly unify
• HasConflict, inheritField, ResolvesField: normal-mode field semantics
• CxnSpec: a partial constructional specification (bar level, modifier position, stress locus, self-embedding)
• CxnSpec.inherit, CxnSpec.IsCompatible, CxnSpec.Resolves: componentwise lifts
• inheritField_of_isCompatible: the two modes agree absent conflict
• Constructicon.parentsOf, derivedSpec, ResolvesAll, WellFormed: inheritance computed through a constructicon's links
• inheritFieldUnique, Constructicon.derivedField: inheritance for fields without decidable equality (e.g. denotations)

Field algebra

A specification field is an Option-valued partial value: none is "unspecified", and inheritance fills unspecified fields from parents.

def ConstructionGrammar.IsCompatible {α : Type u_1} (p q : Option α) : Prop

Two partial field values are compatible — able to strictly unify: at most one is defined, or both agree. Complete-mode inheritance ([Die23] Table 2: representations "fully compatible with each other") is defined exactly on compatible values.

Equations

• ConstructionGrammar.IsCompatible p q = (p = none ∨ q = none ∨ p = q)

@[implicit_reducible]

instance ConstructionGrammar.instDecidableIsCompatible {α : Type u_1} [DecidableEq α] (p q : Option α) : Decidable (IsCompatible p q)

Equations

• ConstructionGrammar.instDecidableIsCompatible p q = ConstructionGrammar.instDecidableIsCompatible._aux_1 p q

def ConstructionGrammar.determinedValues {α : Type u_1} [DecidableEq α] (parents : List (Option α)) : List α

The distinct values a family of parents determines for a field.

Equations

• ConstructionGrammar.determinedValues parents = (List.filterMap id parents).dedup

def ConstructionGrammar.HasConflict {α : Type u_1} [DecidableEq α] (parents : List (Option α)) : Prop

A parent family conflicts on a field when it determines two or more distinct values.

Equations

• ConstructionGrammar.HasConflict parents = (1 < (ConstructionGrammar.determinedValues parents).length)

@[implicit_reducible]

instance ConstructionGrammar.instDecidableHasConflict {α : Type u_1} [DecidableEq α] (parents : List (Option α)) : Decidable (HasConflict parents)

Equations

• ConstructionGrammar.instDecidableHasConflict parents = ConstructionGrammar.instDecidableHasConflict._aux_1 parents

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

Normal-mode (default) inheritance for one field ([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 field takes the unique value its parents agree on; a parental conflict the child does not legislate leaves the field unspecified.

Equations

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

def ConstructionGrammar.ResolvesField {α : Type u_1} [DecidableEq α] (own : Option α) (parents : List (Option α)) : 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 = (ConstructionGrammar.HasConflict parents → own ≠ none)

@[implicit_reducible]

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

Equations

• ConstructionGrammar.instDecidableResolvesField own parents = id inferInstance

@[simp]

theorem ConstructionGrammar.inheritField_some {α : Type u_1} [DecidableEq α] (x : α) (parents : List (Option α)) : inheritField (some x) parents = some x

@[simp]

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

theorem ConstructionGrammar.inheritField_of_isCompatible {α : Type u_1} [DecidableEq α] (own : Option α) {p q : Option α} (h : IsCompatible 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_isCompatible {α : Type u_1} [DecidableEq α] (own : Option α) {p q : Option α} (h : IsCompatible p q) : ResolvesField own [p, q]

Compatible parents impose no resolution burden on the child.

Constructional specification vocabulary

Typed values for the inheritable form-side properties at issue in nominal-modification networks ([Gol95] §3.3; [GS25] §6).

inductive ConstructionGrammar.StressLocus : Type

Locus of primary stress in a modification construction: compound stress falls within the modifier (BLACKbird), phrasal modification stresses the head (black BIRD).

• modifier : StressLocus
• head : StressLocus

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqStressLocus : DecidableEq StressLocus

Equations

• ConstructionGrammar.instDecidableEqStressLocus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConstructionGrammar.instReprStressLocus.repr : StressLocus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprStressLocus : Repr StressLocus

Equations

• ConstructionGrammar.instReprStressLocus = { reprPrec := ConstructionGrammar.instReprStressLocus.repr }

inductive ConstructionGrammar.ModPosition : Type

Position of the modifier slot relative to the head.

• prenominal : ModPosition
• postnominal : ModPosition

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqModPosition : DecidableEq ModPosition

Equations

• ConstructionGrammar.instDecidableEqModPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConstructionGrammar.instReprModPosition.repr : ModPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprModPosition : Repr ModPosition

Equations

• ConstructionGrammar.instReprModPosition = { reprPrec := ConstructionGrammar.instReprModPosition.repr }

inductive ConstructionGrammar.SelfEmbedding : Type

Whether a construction's output can recur inside the construction's own open slot.

• allowed : SelfEmbedding
• banned : SelfEmbedding

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqSelfEmbedding : DecidableEq SelfEmbedding

Equations

• ConstructionGrammar.instDecidableEqSelfEmbedding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConstructionGrammar.instReprSelfEmbedding.repr : SelfEmbedding → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprSelfEmbedding : Repr SelfEmbedding

Equations

• ConstructionGrammar.instReprSelfEmbedding = { reprPrec := ConstructionGrammar.instReprSelfEmbedding.repr }

structure ConstructionGrammar.CxnSpec : Type

A partial constructional specification: the inheritable form-side properties of a (nominal-modification) construction. none means the construction does not legislate the field; inheritance fills unspecified fields from parents.

• level : Option BarLevel

  X-bar level of the construction's output

• modPosition : Option ModPosition

  Position of the modifier slot

• stress : Option StressLocus

  Locus of primary stress

• selfEmbedding : Option SelfEmbedding

  Whether the construction self-embeds

def ConstructionGrammar.instDecidableEqCxnSpec.decEq (x✝ x✝¹ : CxnSpec) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqCxnSpec : DecidableEq CxnSpec

Equations

• ConstructionGrammar.instDecidableEqCxnSpec = ConstructionGrammar.instDecidableEqCxnSpec.decEq

def ConstructionGrammar.instReprCxnSpec.repr : CxnSpec → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprCxnSpec : Repr CxnSpec

Equations

• ConstructionGrammar.instReprCxnSpec = { reprPrec := ConstructionGrammar.instReprCxnSpec.repr }

def ConstructionGrammar.CxnSpec.IsCompatible (p q : CxnSpec) : Prop

Componentwise compatibility: complete-mode inheritance ([Gol95]'s complete mode; the regime of [Sag12]'s type hierarchy) is defined exactly on compatible specifications.

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.CxnSpec.instDecidableIsCompatible (p q : CxnSpec) : Decidable (p.IsCompatible q)

Equations

• p.instDecidableIsCompatible q = ConstructionGrammar.CxnSpec.instDecidableIsCompatible._aux_1 p q

def ConstructionGrammar.CxnSpec.inherit (own : CxnSpec) (parents : List CxnSpec) : CxnSpec

Normal-mode inheritance from a family of parent specifications, componentwise.

Equations

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

def ConstructionGrammar.CxnSpec.Resolves (own : CxnSpec) (parents : List CxnSpec) : Prop

The child's own specification legislates every field its parents conflict on — well-formedness of a normal-mode multi-mother node.

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.CxnSpec.instDecidableResolves (own : CxnSpec) (parents : List CxnSpec) : Decidable (own.Resolves parents)

Equations

• own.instDecidableResolves parents = ConstructionGrammar.CxnSpec.instDecidableResolves._aux_1 own parents

@[simp]

theorem ConstructionGrammar.CxnSpec.inherit_nil (own : CxnSpec) : own.inherit [] = own

theorem ConstructionGrammar.CxnSpec.resolves_of_isCompatible (own : CxnSpec) {p q : CxnSpec} (h : p.IsCompatible q) : own.Resolves [p, q]

Compatible parents impose no resolution burden: any child — including one with no constraints of its own — is well-formed below them. Normal mode only demands child-side legislation at genuine conflicts.

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.

def ConstructionGrammar.Constructicon.parentsOf (cx : Constructicon) (name : String) : List Construction

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 (cx : Constructicon) (name : String) : List Construction

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 (cx : Constructicon) : 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

@[implicit_reducible]

instance ConstructionGrammar.instDecidableWellFormed (cx : Constructicon) : Decidable cx.WellFormed

Equations

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

def ConstructionGrammar.Constructicon.derivedSpec (cx : Constructicon) (own : Construction → CxnSpec) (c : Construction) : CxnSpec

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

Equations

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

def ConstructionGrammar.Constructicon.ResolvesAll (cx : Constructicon) (own : Construction → CxnSpec) : Prop

Normal-mode well-formedness of the whole network: every construction legislates every field its parents conflict on (CxnSpec.Resolves, at each node).

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instDecidableResolvesAll (cx : Constructicon) (own : Construction → CxnSpec) : Decidable (cx.ResolvesAll own)

Equations

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

Inheritance of denotation-valued fields

Denotations (e.g. PartialProp-valued pragmatic contributions) have no decidable equality, so agreeing parents cannot be deduplicated as in inheritField. 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_1} (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 {α : Type u_1} (cx : Constructicon) (own : Construction → Option α) (c : Construction) : 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))