Constructional licensing

The licensing model of constructional grammar ([Sag12]; [Gol95]): an utterance token is grammatical iff every constituent in it instantiates some construction of the network. Constructicon.licenses is the recognizer — a constituent's daughters must match some construction's typed form slot-by-slot (formMatches), and each daughter must itself be licensed; words are licensed lexically.

Matching is relative to a POS lexicon String → Option UD.UPOS. headed fillers are checked against immediate daughters (a flat approximation of headedness), and semantic constraints are not checkable at this level and match any token. Slot constraints are enforced where they can be: negMinus rejects a negated daughter (SlotConstraint.allows).

Main declarations

• Token: utterance tokens (words and constituents)
• SlotFiller.matches, SlotConstraint.allows, formMatches: slot/daughter matching
• Constructicon.Licenses: the licensing relation, via the recognizer

inductive ConstructionGrammar.Token : Type

An utterance token: a word or a constituent with daughter tokens.

• word : String → Token
• node : List Token → Token

def ConstructionGrammar.Token.beq : Token → Token → Bool

Boolean equality on tokens (hand-rolled: Token is a nested inductive, outside the deriving handlers' fragment).

Equations

• (ConstructionGrammar.Token.word a).beq (ConstructionGrammar.Token.word b) = (a == b)
• (ConstructionGrammar.Token.node as).beq (ConstructionGrammar.Token.node bs) = ConstructionGrammar.Token.beqList as bs
• x✝¹.beq x✝ = false

def ConstructionGrammar.Token.beqList : List Token → List Token → Bool

Boolean equality on token lists.

Equations

• ConstructionGrammar.Token.beqList [] [] = true
• ConstructionGrammar.Token.beqList (a :: as) (b :: bs) = (a.beq b && ConstructionGrammar.Token.beqList as bs)
• ConstructionGrammar.Token.beqList x✝¹ x✝ = false

@[instance_reducible]

instance ConstructionGrammar.instBEqToken : BEq Token

Equations

• ConstructionGrammar.instBEqToken = { beq := ConstructionGrammar.Token.beq }

theorem ConstructionGrammar.Token.beq_iff_eq (a b : Token) : a.beq b = true ↔ a = b

theorem ConstructionGrammar.Token.beqList_iff_eq (as bs : List Token) : beqList as bs = true ↔ as = bs

instance ConstructionGrammar.instLawfulBEqToken : LawfulBEq Token

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqToken : DecidableEq Token

Equations

• ConstructionGrammar.instDecidableEqToken a b = decidable_of_iff (a.beq b = true) ⋯

def ConstructionGrammar.SlotFiller.matches (pos : String → Option UD.UPOS) : SlotFiller String → Token → Bool

Does a token satisfy a slot filler, relative to a POS lexicon? semantic constraints are not checkable at this level and match any token; headed requires the head word as an immediate daughter, of the required category.

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.SlotFiller.matches pos (ConstructionGrammar.SlotFiller.fixed w) (ConstructionGrammar.Token.word w') = (w == w')
• ConstructionGrammar.SlotFiller.matches pos (ConstructionGrammar.SlotFiller.open_ cat) (ConstructionGrammar.Token.word w) = (pos w == some cat)
• ConstructionGrammar.SlotFiller.matches pos ConstructionGrammar.SlotFiller.phrasal (ConstructionGrammar.Token.node a) = true
• ConstructionGrammar.SlotFiller.matches pos (ConstructionGrammar.SlotFiller.semantic a) x✝ = true
• ConstructionGrammar.SlotFiller.matches pos x✝¹ x✝ = false

def ConstructionGrammar.SlotConstraint.allows : SlotConstraint → Token → Bool

Does a token respect a slot constraint? negMinus forbids a negation daughter; locMinus and refEmpty concern the slot's external syntax and semantics and are not checkable against the daughter itself.

Equations

• ConstructionGrammar.SlotConstraint.negMinus.allows (ConstructionGrammar.Token.node ts) = !ts.contains (ConstructionGrammar.Token.word "not")
• ConstructionGrammar.SlotConstraint.negMinus.allows (ConstructionGrammar.Token.word w) = !w == "not"
• ConstructionGrammar.SlotConstraint.locMinus.allows x✝ = true
• ConstructionGrammar.SlotConstraint.refEmpty.allows x✝ = true

def ConstructionGrammar.formMatches (pos : String → Option UD.UPOS) (form : TypedForm String) (ts : List Token) : Bool

A daughter sequence instantiates a typed form: same arity, and each daughter matches its slot's filler and respects its slot's constraints.

Equations

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

def ConstructionGrammar.Constructicon.licenses {Sem : Type u_1} (cx : Constructicon Sem) (pos : String → Option UD.UPOS) : Token → Bool

The licensing recognizer: words are licensed lexically; a constituent is licensed iff its daughters instantiate some construction of the network and are each licensed themselves.

Equations

• One or more equations did not get rendered due to their size.
• cx.licenses pos (ConstructionGrammar.Token.word a) = true

def ConstructionGrammar.Constructicon.licensesList {Sem : Type u_1} (cx : Constructicon Sem) (pos : String → Option UD.UPOS) : List Token → Bool

All tokens in a list are licensed.

Equations

• cx.licensesList pos [] = true
• cx.licensesList pos (t :: ts) = (cx.licenses pos t && cx.licensesList pos ts)

def ConstructionGrammar.Constructicon.Licenses {Sem : Type u_1} (cx : Constructicon Sem) (pos : String → Option UD.UPOS) (t : Token) : Prop

cx licenses token t (relative to a POS lexicon): every constituent instantiates some construction of the network. Defined via the licenses recognizer, so concrete cases are kernel-decidable.

Equations

• cx.Licenses pos t = (cx.licenses pos t = true)

@[instance_reducible]

instance ConstructionGrammar.instDecidableLicenses {Sem : Type u_1} (cx : Constructicon Sem) (pos : String → Option UD.UPOS) (t : Token) : Decidable (cx.Licenses pos t)

Equations

• ConstructionGrammar.instDecidableLicenses cx pos t = ConstructionGrammar.instDecidableLicenses._aux_1 cx pos t