CCG grammars and their languages

A CCG grammar is a finite lexicon, a start atom and a RuleSystem, so the formalisms of the literature are choices of rule system. In the classical formalism of Weir and Joshi and of Vijay-Shanker and Weir (Grammar.targetRestricted) a grammar owns a degree bound and a target restriction, under which a rule fires only when the target of its primary input is the start atom. In the multimodal formalism of Baldridge and Steedman (Grammar.multimodal) the rule system is universal, and a grammar is nothing but its lexicon and start atom. A derivation step is an instance X/Y Yβ ⇒ Xβ of the composition schema or its mirror, so it records its argument sequence β, and the harmonic/crossed distinction follows from the slash directions. The target-restricted rule system is modality-blind, so target-restricted grammars use the unrestricted modality.

Kuhlmann, Koller and Satta show that with target restrictions the classical formalism is weakly equivalent to tree-adjoining grammar and without them strictly weaker, and that the multimodal formalism is likewise less expressive than TAG. Schiffer and Maletti upgrade the equivalence to strong equivalence for grammars without empty lexical entries and with rules of degree at most 2. Strings are lists over the token alphabet T, so empty lexical entries are inexpressible.

Main definitions

• CCG.Grammar: a lexicon, a start atom, and a rule system.
• CCG.Grammar.targetRestricted, CCG.Grammar.multimodal: the two formalisms of the literature.
• CCG.Grammar.Derives: the derivability relation, with Grammar.language the language of token strings derived at the start atom.

Main statements

• CCG.Grammar.derives_iff: a grammar derives w at c iff some CCG.Derivation in its rule system over its lexicon has yield w.

Implementation notes

Derivability is an inductive Prop, mathlib's form for grammar formalisms (ContextFreeGrammar.Derives), beside the intrinsically typed CCG.Derivation of the interpreted theory: capacity arguments quantify over all derivations, and induction on Derives is exactly that quantification. As with mathlib's ContextFreeGrammar T, a grammar is parameterized by its token alphabet, and its language is a Language T.

References

• [WJ88]
• [VSW94]
• [Bal02]
• [Ste19]
• [KKS15]
• [SM21]

Grammars and their languages

def CCG.RuleSystem.targetRestricted {α : Type u_2} (start : α) (degree : ℕ) : RuleSystem α

The rule system of the classical formalism ([VSW94], [KKS15]) admits composition up to a degree bound into a primary whose target is the start atom.

Equations

• CCG.RuleSystem.targetRestricted start degree x x✝ β = (β.length ≤ degree ∧ x.target = start)

structure CCG.Grammar (T : Type u_3) (α : Type u_4) : Type (max u_3 u_4)

A CCG grammar has a finite lexicon, a distinguished start atom, and a rule system.

• lexicon : List (T × Cat α)

  Lexical entries, pairing a token with a category.

• start : α

  The distinguished atom, at which the language collects derivations.

• rules : RuleSystem α

  The instances of the composition schema the grammar permits.

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

A target-restricted (VW-CCG) grammar restricts its rules to primary inputs with the start atom as target. The normal form of [SM21] has degree = 2.

Equations

• CCG.Grammar.targetRestricted lexicon start degree = { lexicon := lexicon, start := start, rules := CCG.RuleSystem.targetRestricted start degree }

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

A multimodal grammar, in the radically lexicalized formalism of [Ste19], is a lexicon and a start atom under the universal modality-controlled rule system. It is strictly less expressive than the target-restricted grammars ([KKS15]).

Equations

• CCG.Grammar.multimodal lexicon start = { lexicon := lexicon, start := start, rules := CCG.RuleSystem.multimodal }

@[simp]

theorem CCG.Grammar.multimodal_rules {T : Type u_1} {α : Type u_2} (lexicon : List (T × Cat α)) (start : α) : (multimodal lexicon start).rules = RuleSystem.multimodal

inductive CCG.Grammar.Derives {T : Type u_1} {α : Type u_2} (G : Grammar T α) : Cat α → List T → Prop

G.Derives c w says the grammar derives the token string w at category c, by a lexical entry or by an instance of the composition schema over two adjacent derivations that the grammar's rule system permits.

• lex {T : Type u_1} {α : Type u_2} {G : Grammar T α} {t : T} {c : Cat α} : (t, c) ∈ G.lexicon → G.Derives c [t]

  A lexical entry derives its token.

• forward {T : Type u_1} {α : Type u_2} {G : Grammar T α} {x y : Cat α} {m : Modality} (β : List (Cat.Arg α)) {u v : List T} : G.Derives (x.rslash m y) u → G.Derives (y.pushArgs β) v → G.rules x { side := Edge.right, modality := m, cat := y } β → G.Derives (x.pushArgs β) (u ++ v)

  Forward composition X/Y Yβ ⇒ Xβ, application when β = [].

• backward {T : Type u_1} {α : Type u_2} {G : Grammar T α} {x y : Cat α} {m : Modality} (β : List (Cat.Arg α)) {u v : List T} : G.Derives (y.pushArgs β) u → G.Derives (x.lslash m y) v → G.rules x { side := Edge.left, modality := m, cat := y } β → G.Derives (x.pushArgs β) (u ++ v)

  Backward composition Yβ X\Y ⇒ Xβ, application when β = [].

def CCG.Grammar.language {T : Type u_1} {α : Type u_2} (G : Grammar T α) : Language T

The string language of a grammar is the set of token strings derived at the start atom.

Equations

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

theorem CCG.Grammar.Derives.ne_nil {T : Type u_1} {α : Type u_2} {G : Grammar T α} {c : Cat α} {w : List T} (h : G.Derives c w) : w ≠ []

Every derivable string is nonempty, since a lexical entry is a single token, so grammars are ε-free as in the normal form of [SM21].

Derivability and the tree calculus

A grammar's derivability coincides with the existence of an intrinsically typed Derivation tree in its rule system 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 {T : Type u_1} {α : Type u_2} {G : Grammar T α} {c : Cat α} (d : Derivation T G.rules c) (h : LexIn G.lexicon d) : G.Derives c d.yield

Every Derivation tree in a grammar's rule system over its lexicon witnesses derivability.

theorem CCG.Grammar.derives_iff {T : Type u_1} {α : Type u_2} {G : Grammar T α} {c : Cat α} {w : List T} : G.Derives c w ↔ ∃ (d : Derivation T G.rules c), Derivation.LexIn G.lexicon d ∧ d.yield = w

Derivability is the tree calculus: a grammar derives w at c iff some derivation in its rule system over its lexicon has yield w.