CCG grammars and their languages

This file defines CCG grammars and their string languages. A grammar is a finite lexicon, a start atom, and its rule system, given as permission gates on the generalized composition schema; the formalisms of the literature are choices of gate. Grammar.targetRestricted is VW-CCG ([VSW94], [WJ88]), where the grammar owns a degree bound and a target restriction; Grammar.multimodal is the radically lexicalized modern formalism ([Bal02], [Ste19]), whose rule system is universal — a grammar is nothing but its lexicon and start symbol. The restriction modelled is the one [KKS15]'s generative-capacity results turn on, a target restriction: a rule fires only when the target of its primary input category (the leftmost atom, after stripping all arguments) is a distinguished atom s.

Rules are the generalized-composition schema CCG.Cat.generalizedForwardComp / CCG.Cat.generalizedBackwardComp, gated on the target: a derivation node records only its degree and direction, per the [VSW94] rule form — degree 0 is application, and the harmonic/crossed distinction is a consequence of the slash directions rather than a separate rule class. The schema is modality-blind (VW-CCG predates slash typing); grammars instantiate categories at the unrestricted modality.

The two rule-control mechanisms differ in expressive power ([KKS15]): with target restrictions VW-CCG is weakly equivalent to TAG, without them it is strictly weaker, and the slash-typing variant is likewise slightly less expressive than TAG. [SM21] upgrade the equivalence to strong equivalence (the same tree languages, modulo relabeling) for the modern capacity object: CCG without empty-string lexicon entries and with rules of degree at most 2 — with unbounded degree the formalism is Turing-complete. The Grammar of this file is that object (yields are token lists, so ε-entries are inexpressible by construction), and this file is the substrate for the constructions of CCGs for non-context-free languages in Studies/KuhlmannKollerSatta2015.

Main definitions

• CCG.Grammar: a lexicon, a start atom, and rule-permission gates.
• CCG.Grammar.targetRestricted, CCG.Grammar.multimodal: the two rule systems of the literature, as gate choices.
• CCG.Grammar.Derives: the derivability relation — G.Derives c w says the grammar derives token string w at category c; Grammar.language is the set of strings derived at the distinguished atom.

Main statements

• CCG.Grammar.multimodal_derives_iff: a multimodal grammar derives w at c iff some intrinsically typed CCG.Derivation over its lexicon has yield w — the relation is the string-language shadow of the tree calculus.

Implementation notes

Derivability is an inductive Prop, mathlib's form for grammar formalisms (ContextFreeGrammar.Derives), in contrast to the intrinsically typed CCG.Derivation of the interpreted theory: capacity arguments quantify over all derivations, and induction on Derives is exactly that quantification.

Grammars and their languages

structure CCG.Grammar (α : Type u_2) : Type u_2

A CCG grammar: a finite lexicon, a distinguished start atom, and the grammar's rule system, given as permission gates — allowsFwd n a b says forward composition of degree n may combine primary a with secondary b (mirrored by allowsBwd). The formalisms of the literature are choices of gate: Grammar.targetRestricted (VW-CCG) and Grammar.multimodal (the universal modality-controlled rules).

• lexicon : List (String × Cat α)

  Lexical entries, pairing a token with a category.

• start : α

  The distinguished atom: the language collects derivations of this category.

• allowsFwd : ℕ → Cat α → Cat α → Prop

  May forward composition of degree n combine primary a with secondary b?

• allowsBwd : ℕ → Cat α → Cat α → Prop

  May backward composition of degree n combine secondary a with primary b?

def CCG.Grammar.targetRestricted {α : Type u_1} (lexicon : List (String × Cat α)) (start : α) (degree : ℕ) : Grammar α

A target-restricted (VW-CCG) grammar ([VSW94], [KKS15]): rules up to a degree bound, gated on the primary input's target (degree = 2 in [SM21]'s normal form).

Equations

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

def CCG.Multimodal.allowsFwd {α : Type u_1} : ℕ → Cat α → Cat α → Prop

The universal rule system of multimodal CCG ([Bal02], [Ste19]): degree at most 2, harmonic and crossing composition gated by the primary slash's modality, uniform secondary spines.

Equations

• CCG.Multimodal.allowsFwd 0 x✝¹ x✝ = True
• CCG.Multimodal.allowsFwd 1 (a.rslash m a_1) (a_2.rslash a_3 a_4) = (m ≤ CCG.Modality.diamond)
• CCG.Multimodal.allowsFwd 1 (a.rslash m a_1) (a_2.lslash a_3 a_4) = (m ≤ CCG.Modality.cross)
• CCG.Multimodal.allowsFwd 2 (a.rslash m a_1) ((a_2.rslash a_3 a_4).rslash a_5 a_6) = (m ≤ CCG.Modality.diamond)
• CCG.Multimodal.allowsFwd 2 (a.rslash m a_1) ((a_2.lslash a_3 a_4).lslash a_5 a_6) = (m ≤ CCG.Modality.cross)
• CCG.Multimodal.allowsFwd x✝² x✝¹ x✝ = False

def CCG.Multimodal.allowsBwd {α : Type u_1} : ℕ → Cat α → Cat α → Prop

The mirror of Multimodal.allowsFwd.

Equations

• CCG.Multimodal.allowsBwd 0 x✝¹ x✝ = True
• CCG.Multimodal.allowsBwd 1 (a.lslash a_1 a_2) (a_3.lslash m a_4) = (m ≤ CCG.Modality.diamond)
• CCG.Multimodal.allowsBwd 1 (a.rslash a_1 a_2) (a_3.lslash m a_4) = (m ≤ CCG.Modality.cross)
• CCG.Multimodal.allowsBwd 2 ((a.lslash a_1 a_2).lslash a_3 a_4) (a_5.lslash m a_6) = (m ≤ CCG.Modality.diamond)
• CCG.Multimodal.allowsBwd 2 ((a.rslash a_1 a_2).rslash a_3 a_4) (a_5.lslash m a_6) = (m ≤ CCG.Modality.cross)
• CCG.Multimodal.allowsBwd x✝² x✝¹ x✝ = False

def CCG.Grammar.multimodal {α : Type u_1} (lexicon : List (String × Cat α)) (start : α) : Grammar α

A multimodal grammar: the radically lexicalized formalism of [Ste19], where a grammar is nothing but a lexicon and a start symbol — its rule system is the universal modality-controlled one. Strictly less expressive than the target-restricted grammars ([KKS15]).

Equations

• CCG.Grammar.multimodal lexicon start = { lexicon := lexicon, start := start, allowsFwd := CCG.Multimodal.allowsFwd, allowsBwd := CCG.Multimodal.allowsBwd }

inductive CCG.Grammar.Derives {α : Type u_1} [DecidableEq α] (G : Grammar α) : Cat α → List String → Prop

G.Derives c w: the grammar derives token string w at category c — a lexical entry, or a generalized composition of two adjacent derivations permitted by the grammar's gates. Capacity arguments proceed by induction on this relation.

• lex {α : Type u_1} [DecidableEq α] {G : Grammar α} {w : String} {c : Cat α} : (w, c) ∈ G.lexicon → G.Derives c [w]

  A lexical entry derives its token.

• fc {α : Type u_1} [DecidableEq α] {G : Grammar α} (n : ℕ) {a b c : Cat α} {u v : List String} : G.Derives a u → G.Derives b v → G.allowsFwd n a b → Cat.generalizedForwardComp n a b = some c → G.Derives c (u ++ v)

  Forward composition of degree n (>Bⁿ; degree 0 is application), if the grammar's gate permits it.

• bc {α : Type u_1} [DecidableEq α] {G : Grammar α} (n : ℕ) {a b c : Cat α} {u v : List String} : G.Derives a u → G.Derives b v → G.allowsBwd n a b → Cat.generalizedBackwardComp n a b = some c → G.Derives c (u ++ v)

  Backward composition of degree n (<Bⁿ; degree 0 is application), if the grammar's gate permits it.

def CCG.Grammar.language {α : Type u_1} [DecidableEq α] (G : Grammar α) : Set (List String)

The string language of a grammar: the token strings derived at the distinguished atom. Strings are token lists, so empty-string lexical entries are inexpressible — the ε-freeness of [SM21]'s normal form holds by construction.

Equations

• G.language = {w : List String | G.Derives (CCG.Cat.atom G.start) w}

The multimodal gate and the tree calculus

A multimodal grammar's derivability coincides with the existence of an intrinsically typed Derivation tree over its lexicon: the trees are the proof-relevant calculus (what Derivation.interp consumes), the relation is its string-language shadow.

theorem CCG.Derivation.derives_multimodal {α : Type u_1} [DecidableEq α] {L : List (String × Cat α)} {s : α} {c : Cat α} (d : Derivation α c) : LexIn L d → (Grammar.multimodal L s).Derives c d.yield

Every Derivation tree over the lexicon witnesses multimodal derivability.

theorem CCG.Grammar.Derives.to_derivation {α : Type u_1} [DecidableEq α] {L : List (String × Cat α)} {s : α} {c₀ : Cat α} {w : List String} (h : (multimodal L s).Derives c₀ w) : ∃ (d : Derivation α c₀), Derivation.LexIn L d ∧ d.yield = w

Multimodal derivability yields a Derivation tree over the lexicon: the gate and the schema equation jointly force the shape of a rule of the modern inventory.

theorem CCG.Grammar.multimodal_derives_iff {α : Type u_1} [DecidableEq α] {L : List (String × Cat α)} {s : α} {c : Cat α} {w : List String} : (multimodal L s).Derives c w ↔ ∃ (d : Derivation α c), Derivation.LexIn L d ∧ d.yield = w

Multimodal derivability is the tree calculus: G.Derives c w for a multimodal grammar iff some intrinsically typed derivation over its lexicon has yield w.