CCG derivations

Steedman's Combinatory Projection Principle makes every syntactic combinatory rule binary, linearly ordered and type-dependent, applying to string-adjacent categories. Every such rule is an instance of one schema, forward composition X/Y Yβ ⇒ Xβ or its mirror Yβ X\Y ⇒ Xβ, whose degree is the length of the argument sequence β, with application at degree 0. A CCG formalism is a RuleSystem, which says which instances of the schema fire. The multimodal system of Baldridge and Steedman (RuleSystem.multimodal) is the modern inventory: degree at most 2, a secondary whose arguments all look one way, and a primary slash whose modality licenses harmonic composition (⋄) when they look its way and crossing composition (×) when they look the other way.

A Derivation T R c is a tree of lexical leaves, tokens of an alphabet T, and binary nodes labelled by rules of R, indexed by its category, so a value of Derivation T R c is a derivation of c. Type-raising and coordination are lexical, as in Steedman's morpholexical treatment: raised categories enter as leaves, and a conjunction is an entry of category (X \⋆ X) /⋆ X whose star slashes confine it to application. The substitution rules and the morphemic slash are not modeled.

Main definitions

• CCG.RuleSystem: which instances of the composition schema fire, with RuleSystem.multimodal the modern inventory.
• CCG.Rule: the instances of the schema a rule system permits.
• CCG.Derivation: derivations, with yield the token string, opCount the number of rule applications, HasComp whether composition occurs, and LexIn whether every leaf is drawn from a lexicon.

Main statements

• CCG.Derivation.count_eq_sum: van Benthem's count invariant.

References

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

Rule systems

@[reducible, inline]

abbrev CCG.RuleSystem (α : Type u_3) : Type u_3

A rule system says which instances of the composition schema fire. R x a β permits the primary x a, the category x with outermost argument a, to combine with a secondary a.cat β into x β, by a forward rule when a looks right and a backward rule when it looks left, and by application when β is empty.

Equations

• CCG.RuleSystem α = (CCG.Cat α → CCG.Cat.Arg α → List (CCG.Cat.Arg α) → Prop)

def CCG.RuleSystem.multimodal {α : Type u_2} : RuleSystem α

The multimodal rule system of [Bal02] and [Ste19] admits composition of degree at most 2 into a secondary whose arguments all look one way. The primary slash's modality must license harmonic composition (⋄) when they look its way and crossing composition (×) when they look the other way, and application fires at every modality.

Equations

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

@[instance_reducible]

instance CCG.instDecidableMultimodal {α : Type u_2} (x : Cat α) (a : Cat.Arg α) (β : List (Cat.Arg α)) : Decidable (RuleSystem.multimodal x a β)

Equations

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

@[simp]

theorem CCG.RuleSystem.multimodal_singleton {α : Type u_2} {x : Cat α} {a b : Cat.Arg α} : multimodal x a [b] ↔ a.modality ≤ if b.side = a.side then Modality.diamond else Modality.cross

First-order composition is harmonic when the secondary's argument looks the primary's way and crossing otherwise.

Rules and derivations

inductive CCG.Rule {α : Type u_2} (R : RuleSystem α) : Cat α → Cat α → Cat α → Type u_2

A Rule R l r c is an instance of the composition schema that the rule system R permits, combining a left constituent of category l with a right constituent of category r to give c. Its degree is the length of its argument sequence β.

• forward {α : Type u_2} {R : RuleSystem α} {x y : Cat α} {m : Modality} (β : List (Cat.Arg α)) (h : R x { side := Edge.right, modality := m, cat := y } β) : Rule R (x.rslash m y) (y.pushArgs β) (x.pushArgs β)

  Forward composition X/Y Yβ ⇒ Xβ (>Bⁿ), forward application > when β = [].

• backward {α : Type u_2} {R : RuleSystem α} {x y : Cat α} {m : Modality} (β : List (Cat.Arg α)) (h : R x { side := Edge.left, modality := m, cat := y } β) : Rule R (y.pushArgs β) (x.lslash m y) (x.pushArgs β)

  Backward composition Yβ X\Y ⇒ Xβ (<Bⁿ), backward application < when β = [].

def CCG.Rule.IsComp {α : Type u_2} {R : RuleSystem α} {l r c : Cat α} : Rule R l r c → Prop

The rule is a composition (of any degree or direction) rather than an application.

Equations

• (CCG.Rule.forward β h).IsComp = (β ≠ [])
• (CCG.Rule.backward β h).IsComp = (β ≠ [])

@[instance_reducible]

instance CCG.instDecidableIsComp {α : Type u_2} {R : RuleSystem α} {l r c : Cat α} (ru : Rule R l r c) : Decidable ru.IsComp

Equations

• CCG.instDecidableIsComp (CCG.Rule.forward β h) = { decide := !decide (β = []), reflects_decide := ⋯ }
• CCG.instDecidableIsComp (CCG.Rule.backward β h) = { decide := !decide (β = []), reflects_decide := ⋯ }

inductive CCG.Derivation {α : Type u_2} (T : Type u_3) (R : RuleSystem α) : Cat α → Type (max u_2 u_3)

A CCG derivation of category c is a lexical leaf or a binary Rule node over two derivations, which states the binarity of the Combinatory Projection Principle once. A value of Derivation T R c is a well-formed derivation, so "derives c" is typechecking.

• lex {α : Type u_2} {T : Type u_3} {R : RuleSystem α} (t : T) (c : Cat α) : Derivation T R c

  A lexical leaf, a token at category c.

• node {α : Type u_2} {T : Type u_3} {R : RuleSystem α} {l r c : Cat α} : Rule R l r c → Derivation T R l → Derivation T R r → Derivation T R c

  A binary rule application.

The named rules of degree at most 1. Each discharges its gate by decide when the categories are closed.

@[reducible, inline]

abbrev CCG.Derivation.fapp {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {x y : Cat α} {m : Modality} (d₁ : Derivation T R (x.rslash m y)) (d₂ : Derivation T R y) (h : R x { side := Edge.right, modality := m, cat := y } [] := by decide) : Derivation T R x

Forward application >, X/Y Y ⇒ X.

Equations

• d₁.fapp d₂ h = CCG.Derivation.node (CCG.Rule.forward [] h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.bapp {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {x y : Cat α} {m : Modality} (d₁ : Derivation T R y) (d₂ : Derivation T R (x.lslash m y)) (h : R x { side := Edge.left, modality := m, cat := y } [] := by decide) : Derivation T R x

Backward application <, Y X\Y ⇒ X.

Equations

• d₁.bapp d₂ h = CCG.Derivation.node (CCG.Rule.backward [] h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.fcomp {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {x y z : Cat α} {m n : Modality} (d₁ : Derivation T R (x.rslash m y)) (d₂ : Derivation T R (y.rslash n z)) (h : R x { side := Edge.right, modality := m, cat := y } [{ side := Edge.right, modality := n, cat := z }] := by decide) : Derivation T R (x.rslash n z)

Forward harmonic composition >B, X/Y Y/Z ⇒ X/Z.

Equations

• d₁.fcomp d₂ h = CCG.Derivation.node (CCG.Rule.forward [{ side := Edge.right, modality := n, cat := z }] h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.bcomp {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {x y z : Cat α} {m n : Modality} (d₁ : Derivation T R (y.lslash n z)) (d₂ : Derivation T R (x.lslash m y)) (h : R x { side := Edge.left, modality := m, cat := y } [{ side := Edge.left, modality := n, cat := z }] := by decide) : Derivation T R (x.lslash n z)

Backward harmonic composition <B, Y\Z X\Y ⇒ X\Z.

Equations

• d₁.bcomp d₂ h = CCG.Derivation.node (CCG.Rule.backward [{ side := Edge.left, modality := n, cat := z }] h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.fcompx {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {x y z : Cat α} {m n : Modality} (d₁ : Derivation T R (x.rslash m y)) (d₂ : Derivation T R (y.lslash n z)) (h : R x { side := Edge.right, modality := m, cat := y } [{ side := Edge.left, modality := n, cat := z }] := by decide) : Derivation T R (x.lslash n z)

Forward crossing composition >B×, X/Y Y\Z ⇒ X\Z.

Equations

• d₁.fcompx d₂ h = CCG.Derivation.node (CCG.Rule.forward [{ side := Edge.left, modality := n, cat := z }] h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.bcompx {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {x y z : Cat α} {m n : Modality} (d₁ : Derivation T R (y.rslash n z)) (d₂ : Derivation T R (x.lslash m y)) (h : R x { side := Edge.left, modality := m, cat := y } [{ side := Edge.right, modality := n, cat := z }] := by decide) : Derivation T R (x.rslash n z)

Backward crossing composition <B×, Y/Z X\Y ⇒ X/Z.

Equations

• d₁.bcompx d₂ h = CCG.Derivation.node (CCG.Rule.backward [{ side := Edge.right, modality := n, cat := z }] h) d₁ d₂

def CCG.Derivation.yield {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {c : Cat α} : Derivation T R c → List T

The token string a derivation spells out, its leaves from left to right. Rule nodes concatenate their daughters, so the yield is independent of the derivation's combinatory structure.

Equations

• (CCG.Derivation.lex f c).yield = [f]
• (CCG.Derivation.node a d₁ d₂).yield = d₁.yield ++ d₂.yield

theorem CCG.Derivation.yield_ne_nil {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {c : Cat α} (d : Derivation T R c) : d.yield ≠ []

theorem CCG.Derivation.eq_lex_of_yield_eq_singleton {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {c : Cat α} {d : Derivation T R c} {t : T} (h : d.yield = [t]) : d = lex t c

A derivation spelling out a single token is that token's leaf.

def CCG.Derivation.opCount {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {c : Cat α} : Derivation T R c → ℕ

The number of combinatory rule applications in a derivation.

Equations

• (CCG.Derivation.lex f c).opCount = 0
• (CCG.Derivation.node a d₁ d₂).opCount = 1 + d₁.opCount + d₂.opCount

def CCG.Derivation.LexIn {T : Type u_1} {α : Type u_2} {R : RuleSystem α} (L : List (T × Cat α)) {c : Cat α} : Derivation T R c → Prop

Every lexical leaf of the derivation is an entry of the lexicon L.

Equations

• CCG.Derivation.LexIn L (CCG.Derivation.lex f c) = ((f, c) ∈ L)
• CCG.Derivation.LexIn L (CCG.Derivation.node a d₁ d₂) = (CCG.Derivation.LexIn L d₁ ∧ CCG.Derivation.LexIn L d₂)

@[instance_reducible]

instance CCG.Derivation.LexIn.decidable {T : Type u_1} {α : Type u_2} {R : RuleSystem α} [DecidableEq T] [DecidableEq α] (L : List (T × Cat α)) {c : Cat α} (d : Derivation T R c) : Decidable (LexIn L d)

Equations

• CCG.Derivation.LexIn.decidable L (CCG.Derivation.lex f c) = { decide := decide (List.elem (f, c) L = true), reflects_decide := ⋯ }
• CCG.Derivation.LexIn.decidable L (CCG.Derivation.node a d₁ d₂) = instDecidableAnd

The count invariant

theorem CCG.Rule.count_eq {α : Type u_2} {R : RuleSystem α} [DecidableEq α] (a : α) {l r c : Cat α} (ru : Rule R l r c) : Cat.count a c = Cat.count a l + Cat.count a r

Every combinatory rule preserves the count of every atom.

theorem CCG.Derivation.count_eq_sum {T : Type u_1} {α : Type u_2} {R : RuleSystem α} [DecidableEq α] (a : α) {L : List (T × Cat α)} {f : T → ℤ} (hL : ∀ p ∈ L, Cat.count a p.2 = f p.1) {c : Cat α} (d : Derivation T R c) : LexIn L d → Cat.count a c = (List.map f d.yield).sum

The count invariant of [vB86]. A derivation's category has the count of its leaves, so a string whose lexical counts do not sum to the count of a category has no derivation of that category from the lexicon, whatever the rule system.

def CCG.Derivation.HasComp {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {c : Cat α} : Derivation T R c → Prop

The derivation contains a composition node (of any degree or direction).

Equations

• (CCG.Derivation.lex f c).HasComp = False
• (CCG.Derivation.node a d₁ d₂).HasComp = (a.IsComp ∨ d₁.HasComp ∨ d₂.HasComp)

@[instance_reducible]

instance CCG.Derivation.HasComp.decidable {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {c : Cat α} (d : Derivation T R c) : Decidable d.HasComp

Equations

• CCG.Derivation.HasComp.decidable (CCG.Derivation.lex f c) = isFalse ⋯
• CCG.Derivation.HasComp.decidable (CCG.Derivation.node a d₁ d₂) = instDecidableOr