CCG categories

The categories of combinatory categorial grammar are built from atoms by a rightward and a leftward slash, each slash carrying one of Baldridge's modalities. Every category is uniquely an atom, its target, followed by a sequence of arguments, slash–category pairs; Kuhlmann, Koller and Satta write it A|ₘXₘ ⋯ |₁X₁, and the composition rules of every CCG formalism have the form X/Y Yβ ⇒ Xβ over an argument sequence β. Categories are stated over an arbitrary type α of atoms, so a grammar with featured atoms instantiates its own inventory.

Main definitions

• CCG.Modality: the slash modalities, a bounded order with dot = ⊥, star = ⊤, and diamond and cross incomparable.
• CCG.Cat: categories over a type α of atoms.
• CCG.Cat.Arg, CCG.Cat.pushArgs: an argument, and the category xβ.
• CCG.Cat.target, CCG.Cat.args: the target and the arguments of a category.
• CCG.Cat.equivTargetArgs: a category is its target together with its arguments.
• CCG.Cat.count: the count of an atom.

Main statements

• CCG.Cat.atom_pushArgs_eq_iff: a category is aβ exactly when a is its target and β its arguments.

Notation

• X / Y, X \ Y: slashes with the unrestricted modality dot, written unannotated as in Steedman's presentation.
• X /⋄ Y, X \⋄ Y, X /× Y, X \× Y, X /⋆ Y, X \⋆ Y: slashes with the annotated modality.

All are scoped to the CCG namespace. Because / overloads division, categories are written fully parenthesized ((S \ NP) / NP).

References

• [Ste00a]
• [Ste19]
• [Bal02]
• [KKS15]
• [vB86]

Slash modalities

inductive CCG.Modality : Type

The modality a slash carries, determining which rule classes it licenses. The order is reverse inclusion of licenses, s ≤ m iff s licenses every rule class m does, so composition gates on s ≤ diamond (harmonic) and s ≤ cross (crossing), while application is licensed by every modality (s ≤ ⊤).

• dot : Modality

  The unrestricted modality, written as an unannotated slash, combining by any rule.

• diamond : Modality

  The order-preserving ⋄, licensing application and harmonic composition.

• cross : Modality

  The permuting ×, licensing application and crossing composition.

• star : Modality

  The modality ⋆, licensing application only.

@[instance_reducible]

instance CCG.instDecidableEqModality : DecidableEq Modality

Equations

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

def CCG.instReprModality.repr : Modality → ℕ → Std.Format

Equations

• CCG.instReprModality.repr CCG.Modality.dot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Modality.dot")).group prec✝
• CCG.instReprModality.repr CCG.Modality.diamond prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Modality.diamond")).group prec✝
• CCG.instReprModality.repr CCG.Modality.cross prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Modality.cross")).group prec✝
• CCG.instReprModality.repr CCG.Modality.star prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Modality.star")).group prec✝

@[instance_reducible]

instance CCG.instReprModality : Repr Modality

Equations

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

@[instance_reducible]

instance CCG.instFintypeModality : Fintype Modality

Equations

• CCG.instFintypeModality = { elems := { val := ↑CCG.Modality.enumList, nodup := CCG.Modality.enumList_nodup }, complete := CCG.instFintypeModality._proof_1 }

@[instance_reducible]

instance CCG.Modality.instLE : LE Modality

Equations

• CCG.Modality.instLE = { le := fun (a b : CCG.Modality) => a = CCG.Modality.dot ∨ a = b ∨ b = CCG.Modality.star }

@[instance_reducible]

instance CCG.Modality.instDecidableLE : DecidableLE Modality

Equations

• a.instDecidableLE b = { decide := decide (a = CCG.Modality.dot) || decide (a = b ∨ b = CCG.Modality.star), reflects_decide := ⋯ }

@[instance_reducible]

instance CCG.Modality.instPartialOrder : PartialOrder Modality

Equations

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

@[instance_reducible]

instance CCG.Modality.instBoundedOrder : BoundedOrder Modality

Equations

• CCG.Modality.instBoundedOrder = { top := CCG.Modality.star, le_top := CCG.Modality.instBoundedOrder._proof_1, bot := CCG.Modality.dot, bot_le := CCG.Modality.instBoundedOrder._proof_2 }

@[simp]

theorem CCG.Modality.dot_le (m : Modality) : dot ≤ m

The unrestricted modality licenses every rule class.

Categories

inductive CCG.Cat (α : Type u_1) : Type u_1

CCG categories over a type α of atomic categories, built from atoms by directional slashes that each carry a Modality.

• atom {α : Type u_1} : α → Cat α

  An atomic category.

• rslash {α : Type u_1} : Cat α → Modality → Cat α → Cat α

  X/ₘY looks right for a Y to give an X, at modality m.

• lslash {α : Type u_1} : Cat α → Modality → Cat α → Cat α

  X\ₘY looks left for a Y to give an X, at modality m.

def CCG.instReprCat.repr {α✝ : Type u_1} [Repr α✝] : Cat α✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CCG.instReprCat {α✝ : Type u_1} [Repr α✝] : Repr (Cat α✝)

Equations

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

@[instance_reducible]

instance CCG.instDecidableEqCat {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Cat α✝)

Equations

• CCG.instDecidableEqCat = CCG.instDecidableEqCat.decEq

def CCG.instDecidableEqCat.decEq {α✝ : Type u_1} [DecidableEq α✝] (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 a_3) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (CCG.Cat.atom a) (a_1.lslash a_2 a_3) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.rslash a_1 a_2) (CCG.Cat.atom a_3) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.rslash a_1 a_2) (a_3.lslash a_4 a_5) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.lslash a_1 a_2) (CCG.Cat.atom a_3) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.lslash a_1 a_2) (a_3.rslash a_4 a_5) = isFalse ⋯

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.«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.«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.«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))

Targets and arguments

structure CCG.Cat.Arg (α : Type u_2) : Type u_2

An argument of a category, a slash–category pair.

• side : Edge

  The side the slash looks to, right for / and left for \.

• modality : Modality

  The modality of the slash.

• cat : Cat α

  The argument category.

@[instance_reducible]

instance CCG.Cat.instReprArg {α✝ : Type u_2} [Repr α✝] : Repr (Arg α✝)

Equations

• CCG.Cat.instReprArg = { reprPrec := CCG.Cat.instReprArg.repr }

def CCG.Cat.instReprArg.repr {α✝ : Type u_2} [Repr α✝] : Arg α✝ → ℕ → Std.Format

Equations

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

def CCG.Cat.instDecidableEqArg.decEq {α✝ : Type u_2} [DecidableEq α✝] (x✝ x✝¹ : Arg α✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance CCG.Cat.instDecidableEqArg {α✝ : Type u_2} [DecidableEq α✝] : DecidableEq (Arg α✝)

Equations

• CCG.Cat.instDecidableEqArg = CCG.Cat.instDecidableEqArg.decEq

def CCG.Cat.push {α : Type u_1} (x : Cat α) : Arg α → Cat α

x.push a is x with a as its new outermost argument.

Equations

• x.push { side := Edge.right, modality := m, cat := y } = x.rslash m y
• x.push { side := Edge.left, modality := m, cat := y } = x.lslash m y

@[simp]

theorem CCG.Cat.push_right {α : Type u_1} (x y : Cat α) (m : Modality) : x.push { side := Edge.right, modality := m, cat := y } = x.rslash m y

@[simp]

theorem CCG.Cat.push_left {α : Type u_1} (x y : Cat α) (m : Modality) : x.push { side := Edge.left, modality := m, cat := y } = x.lslash m y

def CCG.Cat.pushArgs {α : Type u_1} (x : Cat α) (β : List (Arg α)) : Cat α

x.pushArgs β is the category xβ, which adds the arguments β to x innermost first, so that x.pushArgs [a₁, a₂] has a₂ as its outermost argument.

Equations

• x.pushArgs β = List.foldl CCG.Cat.push x β

@[simp]

theorem CCG.Cat.pushArgs_nil {α : Type u_1} (x : Cat α) : x.pushArgs [] = x

@[simp]

theorem CCG.Cat.pushArgs_cons {α : Type u_1} (x : Cat α) (a : Arg α) (β : List (Arg α)) : x.pushArgs (a :: β) = (x.push a).pushArgs β

@[simp]

theorem CCG.Cat.pushArgs_append {α : Type u_1} (x : Cat α) (β γ : List (Arg α)) : x.pushArgs (β ++ γ) = (x.pushArgs β).pushArgs γ

def CCG.Cat.target {α : Type u_1} : Cat α → α

The target of a category, its leftmost atom after stripping all arguments, which plays the role of a function's return type.

Equations

• (CCG.Cat.atom a).target = a
• (x_1.rslash a a_1).target = x_1.target
• (x_1.lslash a a_1).target = x_1.target

@[simp]

theorem CCG.Cat.target_atom {α : Type u_1} (a : α) : (atom a).target = a

@[simp]

theorem CCG.Cat.target_rslash {α : Type u_1} (x y : Cat α) (m : Modality) : (x.rslash m y).target = x.target

@[simp]

theorem CCG.Cat.target_lslash {α : Type u_1} (x y : Cat α) (m : Modality) : (x.lslash m y).target = x.target

@[simp]

theorem CCG.Cat.target_push {α : Type u_1} (x : Cat α) (a : Arg α) : (x.push a).target = x.target

@[simp]

theorem CCG.Cat.target_pushArgs {α : Type u_1} (x : Cat α) (β : List (Arg α)) : (x.pushArgs β).target = x.target

def CCG.Cat.args {α : Type u_1} : Cat α → List (Arg α)

The arguments of a category, innermost first.

Equations

• (CCG.Cat.atom a).args = []
• (x_1.rslash a a_1).args = x_1.args ++ [{ side := Edge.right, modality := a, cat := a_1 }]
• (x_1.lslash a a_1).args = x_1.args ++ [{ side := Edge.left, modality := a, cat := a_1 }]

@[simp]

theorem CCG.Cat.args_atom {α : Type u_1} (a : α) : (atom a).args = []

@[simp]

theorem CCG.Cat.args_rslash {α : Type u_1} (x y : Cat α) (m : Modality) : (x.rslash m y).args = x.args ++ [{ side := Edge.right, modality := m, cat := y }]

@[simp]

theorem CCG.Cat.args_lslash {α : Type u_1} (x y : Cat α) (m : Modality) : (x.lslash m y).args = x.args ++ [{ side := Edge.left, modality := m, cat := y }]

@[simp]

theorem CCG.Cat.args_push {α : Type u_1} (x : Cat α) (a : Arg α) : (x.push a).args = x.args ++ [a]

@[simp]

theorem CCG.Cat.args_pushArgs {α : Type u_1} (x : Cat α) (β : List (Arg α)) : (x.pushArgs β).args = x.args ++ β

@[simp]

theorem CCG.Cat.atom_target_pushArgs_args {α : Type u_1} (c : Cat α) : (atom c.target).pushArgs c.args = c

def CCG.Cat.equivTargetArgs {α : Type u_1} : Cat α ≃ α × List (Arg α)

Every category is uniquely its target followed by its arguments.

Equations

• CCG.Cat.equivTargetArgs = { toFun := fun (c : CCG.Cat α) => (c.target, c.args), invFun := fun (p : α × List (CCG.Cat.Arg α)) => (CCG.Cat.atom p.1).pushArgs p.2, left_inv := ⋯, right_inv := ⋯ }

theorem CCG.Cat.atom_pushArgs_eq_iff {α : Type u_1} {a : α} {β : List (Arg α)} {c : Cat α} : (atom a).pushArgs β = c ↔ a = c.target ∧ β = c.args

Type-raising

Type-raising is morpholexical in [Ste19], the work of case morphemes rather than a syntactic rule, so these build the categories that raised lexical entries carry.

def CCG.Cat.forwardTypeRaise {α : Type u_1} (x t : Cat α) : Cat α

forwardTypeRaise x t is t / (t \ x), the forward-raised (>T) category of x at target t.

Equations

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

def CCG.Cat.backwardTypeRaise {α : Type u_1} (x t : Cat α) : Cat α

backwardTypeRaise x t is t \ (t / x), the backward-raised (<T) category of x at target t.

Equations

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

The count invariant

def CCG.Cat.count {α : Type u_1} [DecidableEq α] (a : α) : Cat α → ℤ

The count of the atom a in a category ([vB86]) adds 1 for each occurrence in result position and subtracts 1 for each occurrence in argument position, so that every combinatory rule preserves it (CCG.Rule.count_eq).

Equations

• CCG.Cat.count a (CCG.Cat.atom a_1) = if a_1 = a then 1 else 0
• CCG.Cat.count a (x_1.rslash a_1 a_2) = CCG.Cat.count a x_1 - CCG.Cat.count a a_2
• CCG.Cat.count a (x_1.lslash a_1 a_2) = CCG.Cat.count a x_1 - CCG.Cat.count a a_2

@[simp]

theorem CCG.Cat.count_atom {α : Type u_1} [DecidableEq α] (a b : α) : count a (atom b) = if b = a then 1 else 0

@[simp]

theorem CCG.Cat.count_rslash {α : Type u_1} [DecidableEq α] (a : α) (x y : Cat α) (m : Modality) : count a (x.rslash m y) = count a x - count a y

@[simp]

theorem CCG.Cat.count_lslash {α : Type u_1} [DecidableEq α] (a : α) (x y : Cat α) (m : Modality) : count a (x.lslash m y) = count a x - count a y

@[simp]

theorem CCG.Cat.count_push {α : Type u_1} [DecidableEq α] (a : α) (x : Cat α) (b : Arg α) : count a (x.push b) = count a x - count a b.cat

theorem CCG.Cat.count_pushArgs {α : Type u_1} [DecidableEq α] (a : α) (x : Cat α) (β : List (Arg α)) : count a (x.pushArgs β) = count a x - (List.map (fun (x : Arg α) => count a x.cat) β).sum

The arguments of xβ count against it.