Typed Slot-Filler Representation

@cite{dunn-2025} @cite{kay-fillmore-1999} @cite{fillmore-kay-oconnor-1988} @cite{goldberg-1995}

Constructions are sequences of slots, where each slot is either fixed (a specific lexeme), open (any word of a given syntactic category), or headed (a phrase headed by a specific lexeme). @cite{dunn-2025}'s variationist CxG treats abstraction as continuous (the proportion of open slots). @cite{kay-fillmore-1999} add grammatical functions, coreference indices, and syntactic constraints to the slot representation.

Architecture

Slot Lex combines six pieces of information into one type:

Field	Type	Source
filler	SlotFiller Lex	@cite{dunn-2025} + @cite{kay-fillmore-1999} (fixed/open/headed)
role	Option String	@cite{goldberg-1995} (semantic role)
isHead	Bool	ArgumentStructure.lean
gf	Option GramFunction	@cite{kay-fillmore-1999} (grammatical function)
refIdx	Option RefIndex	@cite{kay-fillmore-1999} (coreference index)
constraints	List SlotConstraint	@cite{kay-fillmore-1999} (syntactic constraints)

TypedForm Lex := List (Slot Lex) is the typed form side of a construction.

The existing ConstructionSlot (which only represents open slots) embeds into Slot String via ConstructionSlot.toSlot (§3).

Key definitions

• abstractionLevel: continuous [0,1] proportion of open slots (ℚ)
• derivedSpecificity: derives Specificity from slot structure
• hasConstraint / refGroupCount: cross-slot constraint queries
• ConstructionSlot.toSlot: embeds existing all-open slots

Verification theorems live in Phenomena/Constructions/Bridge/SlotVerification.lean.

inductive ConstructionGrammar.SlotFiller (Lex : Type) : Type

A slot's filler: the representation level of slot content.

@cite{dunn-2025} distinguishes three representation levels for slot content:

• LEX (lexeme): a specific word form → fixed "must"
• SYN (syntactic): any word of a given POS category → open_.VERB
• SEM+ (semantic): any expression satisfying a semantic constraint → semantic "animate" (any animate NP)

@cite{kay-fillmore-1999} add headed phrases: headed "doing".VERB (a VP headed by doing). These are LEX-level (they fix the head lexeme).

Parameterized over Lex (the lexeme type) so the same representation works for strings, morphemes, or phonological forms.

• fixed {Lex : Type} : Lex → SlotFiller Lex
• open_ {Lex : Type} : UD.UPOS → SlotFiller Lex
• headed {Lex : Type} : Lex → UD.UPOS → SlotFiller Lex

  A phrase headed by a specific lexeme. headed "doing".VERB means "a VP headed by doing" — the slot is phrasal, not the bare word. Contrast with fixed "doing".

• semantic {Lex : Type} : String → SlotFiller Lex

  A semantically constrained slot (@cite{dunn-2025}, SEM+ level). semantic "animate" means any expression satisfying the semantic property "animate". More abstract than SYN (category-based): the filler is constrained by meaning, not by syntactic category.

instance ConstructionGrammar.instDecidableEqSlotFiller {Lex✝ : Type} [DecidableEq Lex✝] : DecidableEq (SlotFiller Lex✝)

Equations

• ConstructionGrammar.instDecidableEqSlotFiller = ConstructionGrammar.instDecidableEqSlotFiller.decEq

def ConstructionGrammar.instDecidableEqSlotFiller.decEq {Lex✝ : Type} [DecidableEq Lex✝] (x✝ x✝¹ : SlotFiller Lex✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.fixed a) (ConstructionGrammar.SlotFiller.fixed b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.fixed a) (ConstructionGrammar.SlotFiller.open_ a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.fixed a) (ConstructionGrammar.SlotFiller.headed a_1 a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.fixed a) (ConstructionGrammar.SlotFiller.semantic a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.open_ a) (ConstructionGrammar.SlotFiller.fixed a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.open_ a) (ConstructionGrammar.SlotFiller.open_ b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.open_ a) (ConstructionGrammar.SlotFiller.headed a_1 a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.open_ a) (ConstructionGrammar.SlotFiller.semantic a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.headed a a_1) (ConstructionGrammar.SlotFiller.fixed a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.headed a a_1) (ConstructionGrammar.SlotFiller.open_ a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.headed a a_1) (ConstructionGrammar.SlotFiller.semantic a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.semantic a) (ConstructionGrammar.SlotFiller.fixed a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.semantic a) (ConstructionGrammar.SlotFiller.open_ a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.semantic a) (ConstructionGrammar.SlotFiller.headed a_1 a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.semantic a) (ConstructionGrammar.SlotFiller.semantic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def ConstructionGrammar.instBEqSlotFiller.beq {Lex✝ : Type} [BEq Lex✝] : SlotFiller Lex✝ → SlotFiller Lex✝ → Bool

Equations

• ConstructionGrammar.instBEqSlotFiller.beq (ConstructionGrammar.SlotFiller.fixed a) (ConstructionGrammar.SlotFiller.fixed b) = (a == b)
• ConstructionGrammar.instBEqSlotFiller.beq (ConstructionGrammar.SlotFiller.open_ a) (ConstructionGrammar.SlotFiller.open_ b) = (a == b)
• ConstructionGrammar.instBEqSlotFiller.beq (ConstructionGrammar.SlotFiller.headed a a_1) (ConstructionGrammar.SlotFiller.headed b b_1) = (a == b && a_1 == b_1)
• ConstructionGrammar.instBEqSlotFiller.beq (ConstructionGrammar.SlotFiller.semantic a) (ConstructionGrammar.SlotFiller.semantic b) = (a == b)
• ConstructionGrammar.instBEqSlotFiller.beq x✝¹ x✝ = false

instance ConstructionGrammar.instBEqSlotFiller {Lex✝ : Type} [BEq Lex✝] : BEq (SlotFiller Lex✝)

Equations

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

instance ConstructionGrammar.instReprSlotFiller {Lex✝ : Type} [Repr Lex✝] : Repr (SlotFiller Lex✝)

Equations

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

def ConstructionGrammar.instReprSlotFiller.repr {Lex✝ : Type} [Repr Lex✝] : SlotFiller Lex✝ → ℕ → Std.Format

Equations

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

def ConstructionGrammar.SlotFiller.isOpen {Lex : Type} : SlotFiller Lex → Bool

Is this slot open (not lexically fixed)?

Both open_ (SYN) and semantic (SEM+) slots count as open for abstraction level computation. headed slots do not: they fix the head lexeme even though the phrase is open.

Equations

• (ConstructionGrammar.SlotFiller.fixed a).isOpen = false
• (ConstructionGrammar.SlotFiller.open_ a).isOpen = true
• (ConstructionGrammar.SlotFiller.headed a a_1).isOpen = false
• (ConstructionGrammar.SlotFiller.semantic a).isOpen = true

inductive ConstructionGrammar.GramFunction : Type

Grammatical function of a valence member (@cite{kay-fillmore-1999}, Figure 12). Distinct from semantic role: a subject (gf) can be an agent, theme, or experiencer (role).

• subj : GramFunction
• comp : GramFunction
• obj : GramFunction
• pred : GramFunction

instance ConstructionGrammar.instDecidableEqGramFunction : DecidableEq GramFunction

Equations

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

def ConstructionGrammar.instBEqGramFunction.beq : GramFunction → GramFunction → Bool

Equations

• ConstructionGrammar.instBEqGramFunction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance ConstructionGrammar.instBEqGramFunction : BEq GramFunction

Equations

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

instance ConstructionGrammar.instReprGramFunction : Repr GramFunction

Equations

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

def ConstructionGrammar.instReprGramFunction.repr : GramFunction → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev ConstructionGrammar.RefIndex : Type

Referential index for cross-slot coreference constraints. Slots sharing the same RefIndex must have their semantic values unified. @cite{kay-fillmore-1999} use #1, #2, etc. to express identity between a construction's semantic arguments and its valence members' semantic values.

Equations

• ConstructionGrammar.RefIndex = ℕ

inductive ConstructionGrammar.SlotConstraint : Type

Syntactic constraint on a slot (@cite{kay-fillmore-1999}, Figure 12).

• locMinus : SlotConstraint
• negMinus : SlotConstraint
• refEmpty : SlotConstraint

instance ConstructionGrammar.instDecidableEqSlotConstraint : DecidableEq SlotConstraint

Equations

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

def ConstructionGrammar.instBEqSlotConstraint.beq : SlotConstraint → SlotConstraint → Bool

Equations

• ConstructionGrammar.instBEqSlotConstraint.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance ConstructionGrammar.instBEqSlotConstraint : BEq SlotConstraint

Equations

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

def ConstructionGrammar.instReprSlotConstraint.repr : SlotConstraint → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.instReprSlotConstraint : Repr SlotConstraint

Equations

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

structure ConstructionGrammar.Slot (Lex : Type) : Type

A slot in a construction: filler content + semantic role + headedness.

Subsumes ConstructionSlot (which only represents open slots) by adding the fixed/open distinction via SlotFiller. Fixed slots (like "let" in let alone) have role := none since they carry no independent semantic role.

• filler : SlotFiller Lex

  What fills this slot: a specific lexeme, open category, or headed phrase

• role : Option String

  Semantic role label (agent, theme, etc.), if any

• isHead : Bool

  Whether this slot is the head of the construction

• gf : Option GramFunction

  Grammatical function (subj, comp, obj, pred) — @cite{kay-fillmore-1999}

• refIdx : Option RefIndex

  Coreference index: slots sharing an index have unified semantics

• constraints : List SlotConstraint

  Syntactic constraints on this slot ([loc -], [neg -], [ref ∅])

def ConstructionGrammar.instDecidableEqSlot.decEq {Lex✝ : Type} [DecidableEq Lex✝] (x✝ x✝¹ : Slot Lex✝) : Decidable (x✝ = x✝¹)

Equations

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

instance ConstructionGrammar.instDecidableEqSlot {Lex✝ : Type} [DecidableEq Lex✝] : DecidableEq (Slot Lex✝)

Equations

• ConstructionGrammar.instDecidableEqSlot = ConstructionGrammar.instDecidableEqSlot.decEq

def ConstructionGrammar.instBEqSlot.beq {Lex✝ : Type} [BEq Lex✝] : Slot Lex✝ → Slot Lex✝ → Bool

Equations

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

instance ConstructionGrammar.instBEqSlot {Lex✝ : Type} [BEq Lex✝] : BEq (Slot Lex✝)

Equations

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

def ConstructionGrammar.instReprSlot.repr {Lex✝ : Type} [Repr Lex✝] : Slot Lex✝ → ℕ → Std.Format

Equations

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

instance ConstructionGrammar.instReprSlot {Lex✝ : Type} [Repr Lex✝] : Repr (Slot Lex✝)

Equations

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

@[reducible, inline]

abbrev ConstructionGrammar.TypedForm (Lex : Type) : Type

A typed form: the form side of a construction as a sequence of slots.

This replaces Construction.form : String with a structured representation that supports computation (abstraction level, specificity derivation).

Equations

• ConstructionGrammar.TypedForm Lex = List (ConstructionGrammar.Slot Lex)

def ConstructionGrammar.abstractionLevel {Lex : Type} (form : TypedForm Lex) : ℚ

Proportion of open slots: a continuous [0,1] measure of abstraction.

This computes the fraction of slots that are open (SYN or SEM+). @cite{dunn-2025} defines four discrete abstraction orders based on which representation levels appear (1st = all LEX, 2nd = mostly LEX, 3rd = mixed, 4th = all abstract). This function computes the continuous proportion underlying those orders; derivedSpecificity (below) maps to the three-way Specificity enum.

Equations

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

def ConstructionGrammar.derivedSpecificity {Lex : Type} (form : TypedForm Lex) : Specificity

Derive Specificity from the slot structure.

Condition	Result
All slots open	.fullyAbstract
No slots open	.lexicallySpecified
Mix of fixed and open	.partiallyOpen

This makes Specificity a derived property rather than a stipulated one: changing a slot from open to fixed automatically changes the specificity.

Equations

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

def ConstructionGrammar.ConstructionSlot.toSlot (s : ConstructionSlot) : Slot String

Embed an all-open ConstructionSlot as a Slot String.

Every ConstructionSlot is an open slot (it only specifies cat : UPOS). The embedding preserves category, role, and headedness.

Equations

• s.toSlot = { filler := ConstructionGrammar.SlotFiller.open_ s.cat, role := some s.role, isHead := s.isHead }

def ConstructionGrammar.ArgStructureConstruction.toTypedForm (asc : ArgStructureConstruction) : TypedForm String

Convert an ArgStructureConstruction's slot list to a TypedForm.

Equations

• asc.toTypedForm = List.map ConstructionGrammar.ConstructionSlot.toSlot asc.slots

theorem ConstructionGrammar.ConstructionSlot.toSlot_isOpen (s : ConstructionSlot) : s.toSlot.filler.isOpen = true

All-open slots are always open (by construction).

def ConstructionGrammar.hasConstraint {Lex : Type} (form : TypedForm Lex) (c : SlotConstraint) : Bool

Does any slot in the form bear a given constraint?

Equations

• ConstructionGrammar.hasConstraint form c = List.any form fun (x : ConstructionGrammar.Slot Lex) => x.constraints.any fun (x : ConstructionGrammar.SlotConstraint) => x == c

def ConstructionGrammar.refGroupCount {Lex : Type} (form : TypedForm Lex) : ℕ

Count of distinct coreference groups in a form.

Equations

• ConstructionGrammar.refGroupCount form = (List.filterMap (fun (x : ConstructionGrammar.Slot Lex) => x.refIdx) form).eraseDups.length