CCG categories

This file defines the categories of Combinatory Categorial Grammar in their modern form ([Ste19]): atoms plus directional slashes, each slash carrying a Baldridge modality ([Bal02]) — the shared substrate of the rule theory (Syntax/CCG/Derivation) and the capacity theory (Syntax/CCG/Grammar).

Categories are stated over an arbitrary type α of atomic categories, so a grammar needing featured atoms (agreement, case) can instantiate a richer inventory than the featureless core CCG.Atom. Each slash carries a Modality from the Baldridge hierarchy — dot (unrestricted), diamond (order-preserving), cross (permuting), star (application-only) — ordered by restrictiveness: a rule class indexed m applies to a functor whose slash has modality s iff s ≤ m. The lexicon controls combinatory potential through the modalities it assigns, the modern replacement for per-grammar rule restrictions (compare CCG.Grammar).

Main definitions

• Modality: the Baldridge slash modalities, a bounded partial order (dot = ⊥, star = ⊤, diamond and cross incomparable).
• Cat: categories over an atom type α — atoms plus modality-carrying slashes.
• Cat.generalizedForwardComp, Cat.generalizedBackwardComp: the degree-n composition schema (modality-blind, for CCG.Grammar).
• Cat.forwardTypeRaise, Cat.backwardTypeRaise: raised categories, for lexicons.
• Cat.target: a category's leftmost atom, the locus of per-grammar rule restrictions.

Notation

• X / Y, X \ Y: slashes with the unrestricted modality dot (absence of an annotation means unrestricted, as in [Ste19]).
• 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 Lean's division, categories are written fully parenthesized ((S \ NP) / NP) rather than relying on the Steedman left-to-right reading.

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

  Unrestricted (written as an unannotated slash): combines by any rule.

• diamond : Modality

  Order-preserving ⋄: licenses application and harmonic composition.

• cross : Modality

  Permuting ×: licenses application and crossing composition.

• star : Modality

  ⋆: licenses 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

• x✝¹.instDecidableLE x✝ = decidable_of_iff (x✝¹ = CCG.Modality.dot ∨ x✝¹ = x✝ ∨ x✝ = CCG.Modality.star) ⋯

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

Categories

inductive CCG.Atom : Type

The core atomic categories of the English fragment (S, NP, N, PP, as in [Ste00a]), stated without features.

• S : Atom

  Sentence.

• NP : Atom

  Noun phrase.

• N : Atom

  Common noun.

• PP : Atom

  Prepositional phrase.

@[instance_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✝

@[instance_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 u_1) : Type u_1

CCG categories over a type α of atomic categories: atoms plus directional slashes, each carrying a Modality.

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

  An atomic category.

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

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

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

  X\ₘY: looking 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))

def CCG.S : Cat Atom

Equations

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

def CCG.NP : Cat Atom

Equations

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

def CCG.N : Cat Atom

Equations

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

def CCG.PP : Cat Atom

Equations

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

def CCG.IV : Cat Atom

Equations

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

def CCG.TV : Cat Atom

Equations

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

def CCG.Det : Cat Atom

Equations

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

The generalized composition schema

def CCG.Cat.generalizedForwardComp {α : Type u_1} [DecidableEq α] : ℕ → Cat α → Cat α → Option (Cat α)

generalizedForwardComp n f g is forward composition of degree n (>Bⁿ): when f = X/Y and g = Y|Z₁…|Zₙ, the result is X|Z₁…|Zₙ with each argument keeping its own slash direction and modality, and none otherwise. Modality-blind — the schema of the grammars in Syntax/CCG/Grammar, where rule control is per-grammar rather than lexical.

Equations

• CCG.Cat.generalizedForwardComp 0 (x_3.rslash a y) x✝ = if y = x✝ then some x_3 else none
• CCG.Cat.generalizedForwardComp n.succ x✝ (g.rslash m z) = Option.map (fun (x : CCG.Cat α) => x.rslash m z) (CCG.Cat.generalizedForwardComp n x✝ g)
• CCG.Cat.generalizedForwardComp n.succ x✝ (g.lslash m z) = Option.map (fun (x : CCG.Cat α) => x.lslash m z) (CCG.Cat.generalizedForwardComp n x✝ g)
• CCG.Cat.generalizedForwardComp x✝² x✝¹ x✝ = none

def CCG.Cat.generalizedBackwardComp {α : Type u_1} [DecidableEq α] : ℕ → Cat α → Cat α → Option (Cat α)

generalizedBackwardComp n g f is backward composition of degree n (<Bⁿ), the mirror of generalizedForwardComp: when g = Y|Z₁…|Zₙ and f = X\Y, the result is X|Z₁…|Zₙ, and none otherwise.

Equations

• CCG.Cat.generalizedBackwardComp 0 x✝ (x_3.lslash a y) = if y = x✝ then some x_3 else none
• CCG.Cat.generalizedBackwardComp n.succ (g.rslash m z) x✝ = Option.map (fun (x : CCG.Cat α) => x.rslash m z) (CCG.Cat.generalizedBackwardComp n g x✝)
• CCG.Cat.generalizedBackwardComp n.succ (g.lslash m z) x✝ = Option.map (fun (x : CCG.Cat α) => x.lslash m z) (CCG.Cat.generalizedBackwardComp n g x✝)
• CCG.Cat.generalizedBackwardComp x✝² x✝¹ x✝ = none

@[simp]

theorem CCG.Cat.generalizedForwardComp_atom {α : Type u_1} [DecidableEq α] (n : ℕ) (x : α) (b : Cat α) : generalizedForwardComp n (atom x) b = none

The schema requires an atomic primary to fail: an atom has no argument to cancel.

@[simp]

theorem CCG.Cat.generalizedForwardComp_lslash {α : Type u_1} [DecidableEq α] (n : ℕ) (x y : Cat α) (m : Modality) (b : Cat α) : generalizedForwardComp n (x.lslash m y) b = none

A leftward primary fails forward composition at every degree.

@[simp]

theorem CCG.Cat.generalizedBackwardComp_atom {α : Type u_1} [DecidableEq α] (n : ℕ) (a : Cat α) (x : α) : generalizedBackwardComp n a (atom x) = none

The mirror of generalizedForwardComp_atom.

@[simp]

theorem CCG.Cat.generalizedBackwardComp_rslash {α : Type u_1} [DecidableEq α] (n : ℕ) (a x y : Cat α) (m : Modality) : generalizedBackwardComp n a (x.rslash m y) = none

A rightward primary fails backward composition at every degree.

@[simp]

theorem CCG.Cat.generalizedForwardComp_succ_atom {α : Type u_1} [DecidableEq α] (n : ℕ) (f : Cat α) (x : α) : generalizedForwardComp (n + 1) f (atom x) = none

An atomic secondary offers no argument spine to peel.

@[simp]

theorem CCG.Cat.generalizedBackwardComp_succ_atom {α : Type u_1} [DecidableEq α] (n : ℕ) (x : α) (b : Cat α) : generalizedBackwardComp (n + 1) (atom x) b = none

The mirror of generalizedForwardComp_succ_atom.

Type-raising

Type-raising is morpholexical in [Ste19] — the work of case morphemes rather than a syntactic rule — so these build the categories raised lexical entries carry; there is no corresponding Derivation constructor.

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)

Targets

Each category has a target — its leftmost atom, "similar to the return type of a function" ([Ste19]) — the locus of the per-grammar rule restrictions of Syntax/CCG/Grammar.

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

The target of a category: its leftmost atom, after stripping all arguments.

Equations

• (CCG.Cat.atom a).target = a
• (a.rslash a_1 a_2).target = a.target
• (a.lslash a_1 a_2).target = a.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