Combinatory Categorial Grammar (CCG)

A lexicalized grammar in which categories encode argument structure and a small fixed set of combinatory rules (>, <, B, T, S) derive phrases ([Ste00a]).

Main definitions

• CCG.Cat — categories: atoms plus the directional slashes / and \
• CCG.combine — try every combinatory rule on a pair of categories
• CCG.DerivStep — a derivation tree; DerivStep.cat reads off its category and DerivStep.yield the surface string it spells out

Notation

/ and \ build directional slash categories. Because / overloads Lean's division, categories are written fully parenthesized ((S \ NP) / NP) rather than relying on the Steedman left-to-right reading.

inductive CCG.Atom : Type

Atomic categories.

• S : Atom
• NP : Atom
• N : Atom
• PP : Atom

@[implicit_reducible]

instance CCG.instReprAtom : Repr Atom

Equations

• CCG.instReprAtom = { reprPrec := CCG.instReprAtom.repr }

def CCG.instReprAtom.repr : Atom → ℕ → Std.Format

Equations

• CCG.instReprAtom.repr CCG.Atom.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Atom.S")).group prec✝
• CCG.instReprAtom.repr CCG.Atom.NP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Atom.NP")).group prec✝
• CCG.instReprAtom.repr CCG.Atom.N prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Atom.N")).group prec✝
• CCG.instReprAtom.repr CCG.Atom.PP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Atom.PP")).group prec✝

@[implicit_reducible]

instance CCG.instDecidableEqAtom : DecidableEq Atom

Equations

• CCG.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive CCG.Cat : Type

CCG categories.

• atom : Atom → Cat
• rslash : Cat → Cat → Cat
• lslash : Cat → Cat → Cat

def CCG.instReprCat.repr : Cat → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CCG.instReprCat : Repr Cat

Equations

• CCG.instReprCat = { reprPrec := CCG.instReprCat.repr }

def CCG.instDecidableEqCat.decEq (x✝ x✝¹ : Cat) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• CCG.instDecidableEqCat.decEq (CCG.Cat.atom a) (CCG.Cat.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• CCG.instDecidableEqCat.decEq (CCG.Cat.atom a) (a_1.rslash a_2) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (CCG.Cat.atom a) (a_1.lslash a_2) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.rslash a_1) (CCG.Cat.atom a_2) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.rslash a_1) (a_2.lslash a_3) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.lslash a_1) (CCG.Cat.atom a_2) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.lslash a_1) (a_2.rslash a_3) = isFalse ⋯

@[implicit_reducible]

instance CCG.instDecidableEqCat : DecidableEq Cat

Equations

• CCG.instDecidableEqCat = CCG.instDecidableEqCat.decEq

def CCG.«term_/_» : Lean.TrailingParserDescr

Equations

• CCG.«term_/_» = Lean.ParserDescr.trailingNode `CCG.«term_/_» 60 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "/") (Lean.ParserDescr.cat `term 0))

def CCG.«term_\_» : Lean.TrailingParserDescr

Equations

• CCG.«term_\_» = Lean.ParserDescr.trailingNode `CCG.«term_\_» 60 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "\\") (Lean.ParserDescr.cat `term 0))

def CCG.S : Cat

Equations

• CCG.S = CCG.Cat.atom CCG.Atom.S

def CCG.NP : Cat

Equations

• CCG.NP = CCG.Cat.atom CCG.Atom.NP

def CCG.N : Cat

Equations

• CCG.N = CCG.Cat.atom CCG.Atom.N

def CCG.PP : Cat

Equations

• CCG.PP = CCG.Cat.atom CCG.Atom.PP

def CCG.IV : Cat

Equations

• CCG.IV = CCG.S.lslash CCG.NP

def CCG.TV : Cat

Equations

• CCG.TV = (CCG.S.lslash CCG.NP).rslash CCG.NP

def CCG.DTV : Cat

Equations

• CCG.DTV = ((CCG.S.lslash CCG.NP).rslash CCG.NP).rslash CCG.NP

def CCG.Det : Cat

Equations

• CCG.Det = CCG.NP.rslash CCG.N

def CCG.Prep : Cat

Equations

• CCG.Prep = CCG.PP.rslash CCG.NP

def CCG.AdjAttr : Cat

Equations

• CCG.AdjAttr = CCG.N.rslash CCG.N

def CCG.AdjPred : Cat

Equations

• CCG.AdjPred = CCG.S.lslash CCG.NP

def CCG.forwardApp : Cat → Cat → Option Cat

Forward application: X/Y Y => X.

Equations

• CCG.forwardApp (x_2.rslash y) x✝ = if (y == x✝) = true then some x_2 else none
• CCG.forwardApp x✝¹ x✝ = none

def CCG.backwardApp : Cat → Cat → Option Cat

Backward application: Y X\Y => X.

Equations

• CCG.backwardApp x✝ (x_2.lslash y) = if (y == x✝) = true then some x_2 else none
• CCG.backwardApp x✝¹ x✝ = none

def CCG.forwardComp : Cat → Cat → Option Cat

Forward composition: X/Y Y/Z => X/Z.

Equations

• CCG.forwardComp (x_2.rslash y) (y'.rslash z) = if (y == y') = true then some (x_2.rslash z) else none
• CCG.forwardComp x✝¹ x✝ = none

def CCG.backwardComp : Cat → Cat → Option Cat

Backward composition: Y\Z X\Y => X\Z.

Equations

• CCG.backwardComp (y.lslash z) (x_2.lslash y') = if (y == y') = true then some (x_2.lslash z) else none
• CCG.backwardComp x✝¹ x✝ = none

def CCG.forwardCompX : Cat → Cat → Option Cat

Forward crossed composition (>B×): X/Y Y\Z => X\Z.

In [Ste00a] this rule is language-specific and restricted (for Dutch, to Y = VP₋SUB; ch. 6 appendix) — unrestricted crossed composition licenses scrambling. The toy Cat carries no features, so the rule is stated unrestricted here; the rule-restricted variant lives in CCG.Classical.fcompX1.

Equations

• CCG.forwardCompX (x_2.rslash y) (y'.lslash z) = if (y == y') = true then some (x_2.lslash z) else none
• CCG.forwardCompX x✝¹ x✝ = none

def CCG.combine : Cat → Cat → Option Cat

Try to combine two categories using all available rules.

Equations

• CCG.combine x✝¹ x✝ = (CCG.forwardApp x✝¹ x✝ <|> CCG.backwardApp x✝¹ x✝ <|> CCG.forwardComp x✝¹ x✝ <|> CCG.backwardComp x✝¹ x✝ <|> CCG.forwardCompX x✝¹ x✝)

def CCG.forwardTypeRaise (x t : Cat) : Cat

Forward type-raising: X => T/(T\X).

Equations

• CCG.forwardTypeRaise x t = t.rslash (t.lslash x)

def CCG.backwardTypeRaise (x t : Cat) : Cat

Backward type-raising: X => T(T/X).

Equations

• CCG.backwardTypeRaise x t = t.lslash (t.rslash x)

def CCG.NPsubj : Cat

Equations

• CCG.NPsubj = CCG.forwardTypeRaise CCG.NP CCG.S

def CCG.NPobj : Cat

Equations

• CCG.NPobj = CCG.backwardTypeRaise CCG.NP CCG.S

def CCG.coordinate : Cat → Cat → Option Cat

Coordination: X conj X => X.

Equations

• CCG.coordinate x✝¹ x✝ = if (x✝¹ == x✝) = true then some x✝¹ else none

structure CCG.LexEntry : Type

A CCG lexical entry.

• form : String
• cat : Cat

def CCG.instReprLexEntry.repr : LexEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CCG.instReprLexEntry : Repr LexEntry

Equations

• CCG.instReprLexEntry = { reprPrec := CCG.instReprLexEntry.repr }

def CCG.Lexicon : Type

A CCG lexicon.

Equations

• CCG.Lexicon = List CCG.LexEntry

def CCG.exampleLexicon : Lexicon

Equations

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

inductive CCG.DerivStep : Type

A derivation step.

• lex : LexEntry → DerivStep
• fapp : DerivStep → DerivStep → DerivStep
• bapp : DerivStep → DerivStep → DerivStep
• fcomp : DerivStep → DerivStep → DerivStep
• bcomp : DerivStep → DerivStep → DerivStep
• fcompx : DerivStep → DerivStep → DerivStep
• ftr : DerivStep → Cat → DerivStep
• btr : DerivStep → Cat → DerivStep
• coord : Coordinator.Role → DerivStep → DerivStep → DerivStep

def CCG.instReprDerivStep.repr : DerivStep → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CCG.instReprDerivStep : Repr DerivStep

Equations

• CCG.instReprDerivStep = { reprPrec := CCG.instReprDerivStep.repr }

def CCG.DerivStep.cat : DerivStep → Option Cat

Get the category of a derivation.

Equations

• (CCG.DerivStep.lex a).cat = some a.cat
• (a.fapp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.forwardApp c1 c2
• (a.bapp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.backwardApp c1 c2
• (a.fcomp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.forwardComp c1 c2
• (a.bcomp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.backwardComp c1 c2
• (a.fcompx a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.forwardCompX c1 c2
• (a.ftr a_1).cat = do let x ← a.cat some (CCG.forwardTypeRaise x a_1)
• (a.btr a_1).cat = do let x ← a.cat some (CCG.backwardTypeRaise x a_1)
• (CCG.DerivStep.coord a a_1 a_2).cat = do let c1 ← a_1.cat let c2 ← a_2.cat CCG.coordinate c1 c2

def CCG.DerivStep.yield : DerivStep → List String

The surface string a derivation spells out: its leaf forms, left to right.

Combinatory rules concatenate their daughters and type-raising leaves the string untouched, so the yield is independent of the derivation's combinatory structure — the property that lets a CCG derivation witness a string language. (Coordination elides the conjunction's surface form in the yield; DerivStep.coord carries the coordinator's role, not its spelled-out word.)

Equations

• (CCG.DerivStep.lex a).yield = [a.form]
• (a.fapp a_1).yield = a.yield ++ a_1.yield
• (a.bapp a_1).yield = a.yield ++ a_1.yield
• (a.fcomp a_1).yield = a.yield ++ a_1.yield
• (a.bcomp a_1).yield = a.yield ++ a_1.yield
• (a.fcompx a_1).yield = a.yield ++ a_1.yield
• (a.ftr a_1).yield = a.yield
• (a.btr a_1).yield = a.yield
• (CCG.DerivStep.coord a a_1 a_2).yield = a_1.yield ++ a_2.yield

def CCG.john_sleeps : DerivStep

Equations

• CCG.john_sleeps = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.sees_mary : DerivStep

Equations

• CCG.sees_mary = (CCG.DerivStep.lex { form := "sees", cat := CCG.TV }).fapp (CCG.DerivStep.lex { form := "Mary", cat := CCG.NP })

def CCG.john_sees_mary : DerivStep

Equations

• CCG.john_sees_mary = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).bapp CCG.sees_mary

def CCG.the_cat : DerivStep

Equations

• CCG.the_cat = (CCG.DerivStep.lex { form := "the", cat := CCG.Det }).fapp (CCG.DerivStep.lex { form := "cat", cat := CCG.N })

def CCG.the_cat_sleeps : DerivStep

Equations

• CCG.the_cat_sleeps = CCG.the_cat.bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.big_cat : DerivStep

Equations

• CCG.big_cat = (CCG.DerivStep.lex { form := "big", cat := CCG.AdjAttr }).fapp (CCG.DerivStep.lex { form := "cat", cat := CCG.N })

def CCG.the_big_cat : DerivStep

Equations

• CCG.the_big_cat = (CCG.DerivStep.lex { form := "the", cat := CCG.Det }).fapp CCG.big_cat

def CCG.the_big_cat_sleeps : DerivStep

Equations

• CCG.the_big_cat_sleeps = CCG.the_big_cat.bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.derivesS (d : DerivStep) : Bool

Check if a derivation yields category S.

Equations

• CCG.derivesS d = (d.cat == some CCG.S)

def CCG.DerivStep.opCount : DerivStep → ℕ

Count combinatory operations in a derivation.

Equations

• (CCG.DerivStep.lex a).opCount = 0
• (a.fapp a_1).opCount = 1 + a.opCount + a_1.opCount
• (a.bapp a_1).opCount = 1 + a.opCount + a_1.opCount
• (a.fcomp a_1).opCount = 2 + a.opCount + a_1.opCount
• (a.bcomp a_1).opCount = 2 + a.opCount + a_1.opCount
• (a.fcompx a_1).opCount = 2 + a.opCount + a_1.opCount
• (a.ftr a_1).opCount = 1 + a.opCount
• (a.btr a_1).opCount = 1 + a.opCount
• (CCG.DerivStep.coord a a_1 a_2).opCount = 1 + a_1.opCount + a_2.opCount

def CCG.DerivStep.depth : DerivStep → ℕ

Depth of derivation tree.

Equations

• (CCG.DerivStep.lex a).depth = 1
• (a.fapp a_1).depth = 1 + max a.depth a_1.depth
• (a.bapp a_1).depth = 1 + max a.depth a_1.depth
• (a.fcomp a_1).depth = 1 + max a.depth a_1.depth
• (a.bcomp a_1).depth = 1 + max a.depth a_1.depth
• (a.fcompx a_1).depth = 1 + max a.depth a_1.depth
• (a.ftr a_1).depth = 1 + a.depth
• (a.btr a_1).depth = 1 + a.depth
• (CCG.DerivStep.coord a a_1 a_2).depth = 1 + max a_1.depth a_2.depth

def CCG.john_tr : DerivStep

Equations

• CCG.john_tr = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).ftr CCG.S

def CCG.john_likes : DerivStep

Equations

• CCG.john_likes = CCG.john_tr.fcomp (CCG.DerivStep.lex { form := "likes", cat := CCG.TV })

def CCG.mary_tr : DerivStep

Equations

• CCG.mary_tr = (CCG.DerivStep.lex { form := "Mary", cat := CCG.NP }).ftr CCG.S

def CCG.mary_hates : DerivStep

Equations

• CCG.mary_hates = CCG.mary_tr.fcomp (CCG.DerivStep.lex { form := "hates", cat := CCG.TV })

def CCG.john_likes_and_mary_hates : DerivStep

Equations

• CCG.john_likes_and_mary_hates = CCG.DerivStep.coord Coordinator.Role.j CCG.john_likes CCG.mary_hates

def CCG.john_likes_and_mary_hates_beans : DerivStep

Equations

• CCG.john_likes_and_mary_hates_beans = CCG.john_likes_and_mary_hates.fapp (CCG.DerivStep.lex { form := "beans", cat := CCG.NP })