Construction Grammar: 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.

Main declarations

• Token: utterance tokens (words and constituents)
• SlotFiller.matches, 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

@[implicit_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

@[implicit_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.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.

Equations

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

def ConstructionGrammar.Constructicon.licenses (cx : Constructicon) (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 (cx : Constructicon) (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 (cx : Constructicon) (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)

@[implicit_reducible]

instance ConstructionGrammar.instDecidableLicenses (cx : Constructicon) (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