Constructions

A construction is a learned pairing of a form and a meaning, for Goldberg the basic unit of grammatical knowledge. The form side is a TypedForm, a sequence of Slots, each fixing a lexeme, opening a category, or admitting any phrase, and a construction's Specificity is derived from its slot structure rather than stipulated.

Main definitions

• SlotFiller, Slot, TypedForm: the typed form side
• RepresentationLevel, SlotFiller.level: the level of a slot's content
• derivedSpecificity, HasConstraint, refGroupCount: measures derived from forms
• Construction, Construction.specificity, Construction.map: typed form–meaning pairings
• Construction.IsFullyCompositional, Construction.IsFormalIdiom: analyzability by the universal combination schemata, and lexical openness

References

• [Gol06]
• [Gol03]
• [Gol95]
• [Dun25]
• [KF99]
• [FKOC88]
• [GS25]
• [Mul13]
• [KM19]

inductive ConstructionGrammar.Specificity : Type

The specificity of a construction is how fully its form side is specified, along [Gol03]'s degree-of-abstraction continuum as [GS25]'s Table 8 discretizes it.

• lexicallySpecified : Specificity

  Every slot is lexically filled, as in veggie-wrap and must-read.

• partiallyOpen : Specificity

  Fixed and open slots are mixed, as in N-wrap and a simple ⟨PAL⟩.

• fullyAbstract : Specificity

  Every slot is open, as in [N⁰ N⁰ N⁰] and [N′ PAL⁰ N].

@[instance_reducible]

instance ConstructionGrammar.instReprSpecificity : Repr Specificity

Equations

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

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

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqSpecificity : DecidableEq Specificity

Equations

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

Typed slots

Slot content follows [Dun25]'s three representation levels, a fixed lexeme (LEX), a word of a category (SYN) and a semantic constraint (SEM), with the categories the parts of speech of Universal Dependencies where Dunn's are learned, plus [KF99]'s headed phrases, grammatical functions, coreference indices and slot constraints.

inductive ConstructionGrammar.SlotFiller (Lex : Type u_1) : Type u_1

A slot's filler gives the slot's content at one of the representation levels. It is parameterized over the lexeme type Lex, so the same representation works for strings, morphemes, or phonological forms.

• fixed {Lex : Type u_1} : Lex → SlotFiller Lex

  fixed w is the word form w itself, at the LEX level, as fixed "must".

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

  open_ pos is any word of part of speech pos, as open_ .VERB.

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

  headed w pos is a phrase of part of speech pos headed by the lexeme w ([KF99]), so headed "doing" .VERB is a VP headed by doing. It is at the LEX level, since the head lexeme is fixed even though the phrase is open.

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

  semantic c is any expression meeting the semantic constraint c, at the SEM level ([Dun25]), so semantic "animate" is any expression denoting an animate.

• phrasal {Lex : Type u_1} : SlotFiller Lex

  phrasal is any phrase, with no fixed head and no category restriction on its internal structure, the filler of a phrasal-compound or PAL slot (the ⟨phrase⟩ node of [GS25]'s Figure 5).

def ConstructionGrammar.instDecidableEqSlotFiller.decEq {Lex✝ : Type u_1} [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.fixed a) ConstructionGrammar.SlotFiller.phrasal = 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.open_ a) ConstructionGrammar.SlotFiller.phrasal = 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.headed a a_1) ConstructionGrammar.SlotFiller.phrasal = 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 ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.semantic a) ConstructionGrammar.SlotFiller.phrasal = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq ConstructionGrammar.SlotFiller.phrasal (ConstructionGrammar.SlotFiller.fixed a) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq ConstructionGrammar.SlotFiller.phrasal (ConstructionGrammar.SlotFiller.open_ a) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq ConstructionGrammar.SlotFiller.phrasal (ConstructionGrammar.SlotFiller.headed a a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq ConstructionGrammar.SlotFiller.phrasal (ConstructionGrammar.SlotFiller.semantic a) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq ConstructionGrammar.SlotFiller.phrasal ConstructionGrammar.SlotFiller.phrasal = isTrue ⋯

@[instance_reducible]

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

Equations

• ConstructionGrammar.instDecidableEqSlotFiller = ConstructionGrammar.instDecidableEqSlotFiller.decEq

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

Equations

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

@[instance_reducible]

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

Equations

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

def ConstructionGrammar.SlotFiller.IsOpen {Lex : Type u_1} : SlotFiller Lex → Prop

A filler is open when no lexeme anchors it. The open_, semantic and phrasal fillers are open, while fixed and headed are not, the latter fixing its head lexeme even though the phrase is open.

Equations

• (ConstructionGrammar.SlotFiller.fixed a).IsOpen = False
• (ConstructionGrammar.SlotFiller.headed a a_1).IsOpen = False
• (ConstructionGrammar.SlotFiller.open_ a).IsOpen = True
• (ConstructionGrammar.SlotFiller.semantic a).IsOpen = True
• ConstructionGrammar.SlotFiller.phrasal.IsOpen = True

@[instance_reducible]

instance ConstructionGrammar.instDecidablePredSlotFillerIsOpen {Lex : Type u_1} : DecidablePred SlotFiller.IsOpen

Equations

• ConstructionGrammar.instDecidablePredSlotFillerIsOpen (ConstructionGrammar.SlotFiller.fixed a) = isFalse ⋯
• ConstructionGrammar.instDecidablePredSlotFillerIsOpen (ConstructionGrammar.SlotFiller.headed a a_1) = isFalse ⋯
• ConstructionGrammar.instDecidablePredSlotFillerIsOpen (ConstructionGrammar.SlotFiller.open_ a) = isTrue trivial
• ConstructionGrammar.instDecidablePredSlotFillerIsOpen (ConstructionGrammar.SlotFiller.semantic a) = isTrue trivial
• ConstructionGrammar.instDecidablePredSlotFillerIsOpen ConstructionGrammar.SlotFiller.phrasal = isTrue trivial

inductive ConstructionGrammar.RepresentationLevel : Type

A representation level is one of [Dun25]'s three ontologies of slot-constraints.

• lex : RepresentationLevel

  A lexical constraint, LEX, fixes a lexeme.

• syn : RepresentationLevel

  A syntactic constraint, SYN, admits the words of a category.

• sem : RepresentationLevel

  A semantic constraint, SEM, admits the expressions that meet it.

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqRepresentationLevel : DecidableEq RepresentationLevel

Equations

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

def ConstructionGrammar.instReprRepresentationLevel.repr : RepresentationLevel → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprRepresentationLevel : Repr RepresentationLevel

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instFintypeRepresentationLevel : Fintype RepresentationLevel

Equations

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

def ConstructionGrammar.SlotFiller.level {Lex : Type u_1} : SlotFiller Lex → RepresentationLevel

f.level is lexical for fixed lexemes and headed phrases, syntactic for categories and phrases, and semantic for semantic constraints.

Equations

• (ConstructionGrammar.SlotFiller.fixed a).level = ConstructionGrammar.RepresentationLevel.lex
• (ConstructionGrammar.SlotFiller.headed a a_1).level = ConstructionGrammar.RepresentationLevel.lex
• (ConstructionGrammar.SlotFiller.open_ a).level = ConstructionGrammar.RepresentationLevel.syn
• ConstructionGrammar.SlotFiller.phrasal.level = ConstructionGrammar.RepresentationLevel.syn
• (ConstructionGrammar.SlotFiller.semantic a).level = ConstructionGrammar.RepresentationLevel.sem

theorem ConstructionGrammar.SlotFiller.isOpen_iff_level_ne_lex {Lex : Type u_1} (f : SlotFiller Lex) : f.IsOpen ↔ f.level ≠ RepresentationLevel.lex

A filler is open exactly when it is not lexical.

inductive ConstructionGrammar.GrammaticalFunction : Type

The grammatical function of a valence member ([KF99], Figure 12) is distinct from its semantic role, since a subject can be an agent, a theme, or an experiencer.

• subj : GrammaticalFunction

  subj is the subject.

• comp : GrammaticalFunction

  comp is a clausal or verbal complement.

• obj : GrammaticalFunction

  obj is the direct object.

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqGrammaticalFunction : DecidableEq GrammaticalFunction

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprGrammaticalFunction : Repr GrammaticalFunction

Equations

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

def ConstructionGrammar.instReprGrammaticalFunction.repr : GrammaticalFunction → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev ConstructionGrammar.RefIndex : Type

A reference index marks unification across slots, [KF99]'s #1 and #2; values bearing one index are unified.

Equations

• ConstructionGrammar.RefIndex = ℕ

inductive ConstructionGrammar.SlotConstraint : Type

A slot constraint is a syntactic constraint on a slot ([KF99], Figure 12).

• locMinus : SlotConstraint

  [loc -] requires the slot to occur left-isolated, not VP-internal.

• negMinus : SlotConstraint

  [neg -] forbids negating the slot.

• refEmpty : SlotConstraint

  [ref ∅] marks the slot as no operator, "in the sense of binding the reference of something else".

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqSlotConstraint : DecidableEq SlotConstraint

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprSlotConstraint : Repr SlotConstraint

Equations

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

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

Equations

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

structure ConstructionGrammar.Slot (Lex : Type u_1) : Type u_1

A slot in a construction's form has a filler, a headedness flag, and Kay and Fillmore's lexicality of the position, where lex := none leaves it unspecified; their maximality is not stored, since a head is nonmaximal and every other daughter maximal. A slot's semantics bears its refIdx, and a predicate phrase that does not realize its own subject bears the index of that subject requirement as its subjIdx. Coinstantiation, which covers raising and control, unifies a predicator's subject with the subject requirement of its complement ([KF99], Figure 13).

• filler : SlotFiller Lex

  filler is what fills the slot.

• isHead : Bool

  isHead records whether the slot is the head of the construction.

• lex : Option Bool

  lex says whether the position is a word, some true for a word-level slot.

• gf : Option GrammaticalFunction

  gf is the slot's grammatical function ([KF99]).

• refIdx : Option RefIndex

  refIdx is the index of the slot's semantics.

• subjIdx : Option RefIndex

  subjIdx is the index of the slot's unrealized subject requirement.

• constraints : List SlotConstraint

  constraints lists the slot's syntactic constraints.

@[instance_reducible]

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

Equations

• ConstructionGrammar.instDecidableEqSlot = ConstructionGrammar.instDecidableEqSlot.decEq

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

@[reducible, inline]

abbrev ConstructionGrammar.TypedForm (Lex : Type u_1) : Type u_1

A typed form is the form side of a construction, a sequence of slots.

Equations

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

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

A slot holds a phrase in a word-level position when its filler is phrasal and its position a word, the defining configuration of phrasal compounds and the PAL construction ([GS25]) and the cell that lexical-integrity hypotheses rule out.

Equations

• s.IsPhraseInWordSlot = (s.filler = ConstructionGrammar.SlotFiller.phrasal ∧ s.lex = some true)

@[instance_reducible]

instance ConstructionGrammar.instDecidableIsPhraseInWordSlotOfDecidableEq {Lex : Type u_1} [DecidableEq Lex] (s : Slot Lex) : Decidable s.IsPhraseInWordSlot

Equations

• ConstructionGrammar.instDecidableIsPhraseInWordSlotOfDecidableEq s = { decide := decide (s.filler = ConstructionGrammar.SlotFiller.phrasal) && decide (s.lex = some true), reflects_decide := ⋯ }

Derived specificity

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

The derived specificity of a form is fullyAbstract when every slot is open (vacuously so for the empty form), lexicallySpecified when none is, and partiallyOpen otherwise.

Equations

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

def ConstructionGrammar.HasConstraint {Lex : Type u_1} (form : TypedForm Lex) (c : SlotConstraint) : Prop

Some slot in the form bears the constraint c.

Equations

• ConstructionGrammar.HasConstraint form c = ∃ s ∈ form, c ∈ s.constraints

@[instance_reducible]

instance ConstructionGrammar.instDecidableHasConstraint {Lex : Type u_1} (form : TypedForm Lex) (c : SlotConstraint) : Decidable (HasConstraint form c)

Equations

• ConstructionGrammar.instDecidableHasConstraint form c = ConstructionGrammar.instDecidableHasConstraint._aux_1 form c

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

The number of distinct unification indices in a form, on slots and on their subject requirements.

Equations

• ConstructionGrammar.refGroupCount form = (List.flatMap (fun (s : ConstructionGrammar.Slot Lex) => s.refIdx.toList ++ s.subjIdx.toList) form).dedup.length

Characterization lemmas

theorem ConstructionGrammar.derivedSpecificity_eq_fullyAbstract_iff {Lex : Type u_1} (form : TypedForm Lex) : derivedSpecificity form = Specificity.fullyAbstract ↔ ∀ s ∈ form, s.filler.IsOpen

A form is fully abstract exactly when every slot is open (vacuously so for the empty form).

theorem ConstructionGrammar.derivedSpecificity_eq_lexicallySpecified_iff {Lex : Type u_1} (form : TypedForm Lex) : derivedSpecificity form = Specificity.lexicallySpecified ↔ form ≠ [] ∧ ∀ s ∈ form, ¬s.filler.IsOpen

A form is lexically specified exactly when it is nonempty and no slot is open.

Constructions and the network

structure ConstructionGrammar.Construction (Sem : Type u_1) : Type u_1

A construction is a learned pairing of form and meaning. The meaning pole is typed by the domain that owns the construction, such as a composition rule or a presupposition, with Unit for a purely formal record or a defective, form-only construction.

• form : TypedForm String

  form is the form pole.

• meaning : Sem

  meaning is the meaning pole.

• pragmaticPoint : Bool

  pragmaticPoint records whether the construction carries a conventional pragmatic point ([FKOC88] §1.1.4).

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqConstruction {Sem✝ : Type u_1} [DecidableEq Sem✝] : DecidableEq (Construction Sem✝)

Equations

• ConstructionGrammar.instDecidableEqConstruction = ConstructionGrammar.instDecidableEqConstruction.decEq

def ConstructionGrammar.instDecidableEqConstruction.decEq {Sem✝ : Type u_1} [DecidableEq Sem✝] (x✝ x✝¹ : Construction Sem✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprConstruction {Sem✝ : Type u_1} [Repr Sem✝] : Repr (Construction Sem✝)

Equations

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

def ConstructionGrammar.instReprConstruction.repr {Sem✝ : Type u_1} [Repr Sem✝] : Construction Sem✝ → ℕ → Std.Format

Equations

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

def ConstructionGrammar.Construction.specificity {Sem : Type u_1} (c : Construction Sem) : Specificity

A construction's specificity is derived from its slot structure.

Equations

• c.specificity = ConstructionGrammar.derivedSpecificity c.form

def ConstructionGrammar.Construction.map {Sem : Type u_1} {Sem' : Type u_2} (f : Sem → Sem') (c : Construction Sem) : Construction Sem'

c.map f reinterprets the meaning pole of c along f, keeping the form.

Equations

• ConstructionGrammar.Construction.map f c = { form := c.form, meaning := f c.meaning, pragmaticPoint := c.pragmaticPoint }

def ConstructionGrammar.Construction.IsFullyCompositional {Sem : Type u_1} (c : Construction Sem) : Prop

A construction is fully compositional when the universal combination schemata alone analyze it, when its form is fully abstract and it carries no pragmatic point. This is a proxy for [Mul13]'s structural criterion, approximating what [KM19] survey as a continuum.

Equations

• c.IsFullyCompositional = (c.specificity = ConstructionGrammar.Specificity.fullyAbstract ∧ c.pragmaticPoint = false)

@[instance_reducible]

instance ConstructionGrammar.instDecidableIsFullyCompositional {Sem : Type u_1} (c : Construction Sem) : Decidable c.IsFullyCompositional

Equations

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

def ConstructionGrammar.Construction.IsFormalIdiom {Sem : Type u_1} (c : Construction Sem) : Prop

A construction is a formal idiom in the sense of [FKOC88] §1.1.3, a lexically open idiom, when it is a syntactic pattern rather than a lexically filled expression. The distinction is a cline (fn. 3), which Specificity discretizes.

Equations

• c.IsFormalIdiom = (c.specificity ≠ ConstructionGrammar.Specificity.lexicallySpecified)

@[instance_reducible]

instance ConstructionGrammar.instDecidableIsFormalIdiom {Sem : Type u_1} (c : Construction Sem) : Decidable c.IsFormalIdiom

Equations

• ConstructionGrammar.instDecidableIsFormalIdiom c = { decide := !decide (c.specificity = ConstructionGrammar.Specificity.lexicallySpecified), reflects_decide := ⋯ }