Construction Grammar: Core Types

@cite{goldberg-1995} @cite{goldberg-2003} @cite{goldberg-2006}

Minimal infrastructure for Construction Grammar (CxG), the framework in which constructions — learned pairings of form and function — are the basic units of grammatical knowledge.

inductive ConstructionGrammar.Specificity : Type

How specified a construction's form side is (@cite{goldberg-2003}:220, Table 8).

Specificity	Example
lexicallySpecified	"veggie-wrap", "must-read"
partiallyOpen	"N-wrap", "a simple ⟨PAL⟩"
fullyAbstract	[N⁰ N⁰ N⁰], [N' PAL⁰ N]

• lexicallySpecified : Specificity
• partiallyOpen : Specificity
• fullyAbstract : Specificity

def ConstructionGrammar.instReprSpecificity.repr : Specificity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprSpecificity : Repr Specificity

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqSpecificity : DecidableEq Specificity

Equations

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

inductive ConstructionGrammar.InheritanceMode : Type

Mode of information transfer in an inheritance link (@cite{goldberg-1995} §3.3.1, p. 73–74).

@cite{goldberg-1995} distinguishes two modes, orthogonal to link type:

• Normal: child inherits defaults from parent but may override them. Allows subregularities and exceptions. The only mode used in @cite{goldberg-1995}'s system.
• Complete: all information from dominating nodes is inherited strictly; no conflicts allowed. Used in unification-based grammars (HPSG, GPSG) but not exploited in @cite{goldberg-1995}'s constructional analysis.

• normal : InheritanceMode
• complete : InheritanceMode

def ConstructionGrammar.instReprInheritanceMode.repr : InheritanceMode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprInheritanceMode : Repr InheritanceMode

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqInheritanceMode : DecidableEq InheritanceMode

Equations

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

inductive ConstructionGrammar.LinkType : Type

Type of semantic relation in an inheritance link (@cite{goldberg-1995} §3.3.2, p. 75).

@cite{goldberg-1995} distinguishes four major link types:

• I_P (Polysemy): relates the central sense of a construction to its extensions. Each extension inherits syntax but differs in meaning (e.g., the six senses of the ditransitive, pp. 75–77).
• I_M (Metaphorical extension): source and target related by systematic metaphor (e.g., caused-motion → resultative via the motion→change metaphor, p. 81).
• I_S (Subpart): one construction is a proper subpart of another (e.g., intransitive motion is a subpart of caused-motion, p. 78).
• I_I (Instance): one construction is a more fully specified version of another (e.g., drive-crazy is an instance of the resultative, p. 79).

• polysemy : LinkType
• metaphorical : LinkType
• subpart : LinkType
• instance : LinkType

@[implicit_reducible]

instance ConstructionGrammar.instReprLinkType : Repr LinkType

Equations

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

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

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqLinkType : DecidableEq LinkType

Equations

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

structure ConstructionGrammar.Construction : Type

A construction: a learned pairing of form and function.

Constructions range from fully lexically specified (idioms, words) to fully abstract (argument-structure constructions).

• name : String
• form : String
• meaning : String
• specificity : Specificity
• pragmaticFunction : Option String

def ConstructionGrammar.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprConstruction : Repr Construction

Equations

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

def ConstructionGrammar.instBEqConstruction.beq : Construction → Construction → Bool

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.instBEqConstruction.beq x✝¹ x✝ = false

@[implicit_reducible]

instance ConstructionGrammar.instBEqConstruction : BEq Construction

Equations

• ConstructionGrammar.instBEqConstruction = { beq := ConstructionGrammar.instBEqConstruction.beq }

structure ConstructionGrammar.InheritanceLink : Type

An inheritance link between two constructions in the network.

Each link specifies both how information flows (mode, §3.3.1) and what semantic relation holds (linkType, §3.3.2). Links without a specific semantic relation (e.g., general taxonomic inheritance of shared morphophonological properties) use linkType := none.

• parent : String
• child : String
• mode : InheritanceMode
• linkType : Option LinkType
• sharedProperties : List String
• overriddenProperties : List String

@[implicit_reducible]

instance ConstructionGrammar.instReprInheritanceLink : Repr InheritanceLink

Equations

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

def ConstructionGrammar.instReprInheritanceLink.repr : InheritanceLink → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instBEqInheritanceLink : BEq InheritanceLink

Equations

• ConstructionGrammar.instBEqInheritanceLink = { beq := ConstructionGrammar.instBEqInheritanceLink.beq }

def ConstructionGrammar.instBEqInheritanceLink.beq : InheritanceLink → InheritanceLink → Bool

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.instBEqInheritanceLink.beq x✝¹ x✝ = false

structure ConstructionGrammar.Constructicon : Type

A constructicon: a network of constructions connected by inheritance links.

• constructions : List Construction
• links : List InheritanceLink

@[implicit_reducible]

instance ConstructionGrammar.instReprConstructicon : Repr Constructicon

Equations

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

def ConstructionGrammar.instReprConstructicon.repr : Constructicon → ℕ → Std.Format

Equations

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