The constructicon

A constructicon is a network of constructions ([Gol95] §3.3; [Die23]). Each node of a Constructicon ι Sem carries a construction. Its inheritance links run up from a construction to the constructions it inherits from, its mothers, and its horizontal links relate it to constructions at its own level of abstraction, which motivate it without passing information down: the links between syntactic alternates of [tW23], the motivation links of [GS25].

Inheritance is in the normal mode of [Gol95] §3.3.1: "information is inherited from dominant nodes transitively as long as that information does not conflict with information specified by nodes lower in the inheritance hierarchy" (p. 73). That is default inheritance over the order the inheritance links generate (DefaultInheritance.inherited): a construction takes each property from the most specific constructions above it that specify one. A construction whose mothers conflict on a property inherits both values unless it specifies its own, which is why normal mode, unlike complete mode, admits several mothers. A study puts the order on its node type with Constructicon.partialOrder, from a rank that every inheritance link decreases, so the network is the directed acyclic graph the book requires (p. 73).

The relation an inheritance link records constrains the forms it joins (§3.3.2): "the syntactic specifications of the central sense are inherited by the extensions" of a polysemy link (p. 75), a subpart is "a proper subpart of another construction" (p. 78), and an instance link exists "iff one construction is a more fully specified version of the other" (p. 79). Constructicon.WellTyped checks every inheritance link against its relation.

Main definitions

• LinkType, LinkType.Admits: the relations an inheritance link records, and what each requires of the forms it joins
• Constructicon: constructions at nodes, with inheritance and horizontal links
• Constructicon.IsMother, Constructicon.partialOrder, Constructicon.decidableLE: the inheritance order
• Constructicon.WellTyped: every inheritance link respects its relation

Implementation notes

A slot of an instance refines the corresponding slot of the construction it instantiates when the two are equal or the latter is open; the categories of fixed lexemes are not checked. A metaphorical extension may change its form, so the relation places no constraint on forms.

References

• [Gol95]
• [Die23]
• [GS25]
• [tW23]

Link types

inductive ConstructionGrammar.LinkType : Type

The semantic relation an inheritance link records: [Gol95]'s four major link types (§3.3.2, p. 75).

• polysemy : LinkType

  I_P: from a central sense to an extension, which inherits the syntax but differs in meaning (the senses of the ditransitive, pp. 75–77).

• metaphorical : LinkType

  I_M: source and target related by a systematic metaphor (caused motion to the resultative, change of state as change of location, p. 81).

• subpart : LinkType

  I_S: the linked construction is a proper subpart of the other (intransitive motion inside caused motion, p. 78).

• instance : LinkType

  I_I: the linked construction is a more fully specified version of the other (drive-crazy as an instance of the resultative, p. 79).

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqLinkType : DecidableEq LinkType

Equations

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

def ConstructionGrammar.instReprLinkType.repr : LinkType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprLinkType : Repr LinkType

Equations

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

def ConstructionGrammar.Slot.Refines {Lex : Type u_1} (s t : Slot Lex) : Prop

A slot refines another when the two are equal or the other is open: the lexically filled slots of an instance fill open slots of the construction it instantiates.

Equations

• s.Refines t = (s = t ∨ t.filler.IsOpen)

@[instance_reducible]

instance ConstructionGrammar.instDecidableRefinesOfDecidableEq {Lex : Type u_1} [DecidableEq Lex] (s t : Slot Lex) : Decidable (s.Refines t)

Equations

• ConstructionGrammar.instDecidableRefinesOfDecidableEq s t = { decide := decide (s = t) || decide t.filler.IsOpen, reflects_decide := ⋯ }

def ConstructionGrammar.LinkType.Admits {Lex : Type u_1} : LinkType → TypedForm Lex → TypedForm Lex → Prop

What a link type requires of the form c of the linked construction, given the form m of the construction it inherits from.

Equations

• ConstructionGrammar.LinkType.polysemy.Admits x✝¹ x✝ = (x✝¹ = x✝)
• ConstructionGrammar.LinkType.metaphorical.Admits x✝¹ x✝ = True
• ConstructionGrammar.LinkType.subpart.Admits x✝¹ x✝ = (List.Sublist x✝¹ x✝ ∧ x✝¹ ≠ x✝)
• ConstructionGrammar.LinkType.instance.Admits x✝¹ x✝ = (List.Forall₂ ConstructionGrammar.Slot.Refines x✝¹ x✝ ∧ x✝¹ ≠ x✝)

@[instance_reducible]

instance ConstructionGrammar.instDecidableAdmitsOfDecidableEq {Lex : Type u_1} [DecidableEq Lex] (t : LinkType) (c m : TypedForm Lex) : Decidable (t.Admits c m)

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.instDecidableAdmitsOfDecidableEq ConstructionGrammar.LinkType.polysemy x✝¹ x✝ = ConstructionGrammar.instDecidableAdmitsOfDecidableEq._aux_1 x✝¹ x✝
• ConstructionGrammar.instDecidableAdmitsOfDecidableEq ConstructionGrammar.LinkType.metaphorical x✝¹ x✝ = isTrue trivial
• ConstructionGrammar.instDecidableAdmitsOfDecidableEq ConstructionGrammar.LinkType.subpart x✝¹ x✝ = { decide := decide (List.Sublist x✝¹ x✝) && decide (x✝¹ ≠ x✝), reflects_decide := ⋯ }

The network

structure ConstructionGrammar.Constructicon (ι : Type u_2) (Sem : Type u_3) : Type (max u_2 u_3)

A constructicon over the nodes ι: the construction at each node, the inheritance links from a node up to its mothers, and the horizontal links from a node to constructions at its level, each with the relation it records if any.

• cxn : ι → Construction Sem

  The construction at each node.

• mothers : ι → List (ι × Option LinkType)

  The mothers of each node, the constructions it inherits from.

• related : ι → List (ι × Option LinkType)

  The constructions each node is related to at its own level, without inheritance.

def ConstructionGrammar.Constructicon.IsMother {ι : Type u_2} {Sem : Type u_3} (N : Constructicon ι Sem) (c m : ι) : Prop

m is a mother of c: c inherits from m by an inheritance link.

Equations

• N.IsMother c m = (m ∈ List.map Prod.fst (N.mothers c))

@[instance_reducible]

instance ConstructionGrammar.Constructicon.instDecidableRelIsMotherOfDecidableEq {ι : Type u_2} {Sem : Type u_3} (N : Constructicon ι Sem) [DecidableEq ι] : DecidableRel N.IsMother

Equations

• N.instDecidableRelIsMotherOfDecidableEq c m = { decide := decide (List.elem m (List.map Prod.fst (N.mothers c)) = true), reflects_decide := ⋯ }

@[reducible, inline]

abbrev ConstructionGrammar.Constructicon.partialOrder {ι : Type u_2} {Sem : Type u_3} (N : Constructicon ι Sem) (rank : ι → ℕ) (h : ∀ (c m : ι), N.IsMother c m → rank m < rank c) : PartialOrder ι

The inheritance order: c ≤ m when c inherits from m through a chain of links. A rank that every link decreases makes it antisymmetric.

Equations

• N.partialOrder rank h = partialOrderOfCovers N.IsMother rank h

@[reducible, inline]

abbrev ConstructionGrammar.Constructicon.decidableLE {ι : Type u_2} {Sem : Type u_3} (N : Constructicon ι Sem) [DecidableEq ι] (nodes : List ι) (h : ∀ (c m : ι), N.IsMother c m → m ∈ nodes) (c m : ι) : Decidable (Relation.ReflTransGen N.IsMother c m)

The inheritance order is decidable given a list of every mother.

Equations

• N.decidableLE nodes h c m = decidableLEOfCovers nodes h c m

def ConstructionGrammar.Constructicon.WellTyped {ι : Type u_2} {Sem : Type u_3} (N : Constructicon ι Sem) : Prop

Every inheritance link respects the relation it records.

Equations

• N.WellTyped = ∀ (c : ι), ∀ e ∈ N.mothers c, ∀ t ∈ e.2, t.Admits (N.cxn c).form (N.cxn e.1).form

@[instance_reducible]

instance ConstructionGrammar.Constructicon.instDecidableWellTypedOfFintype {ι : Type u_2} {Sem : Type u_3} (N : Constructicon ι Sem) [Fintype ι] : Decidable N.WellTyped

Equations

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