CCG derivations

This file defines the modern rule theory of CCG ([Ste19]): the combinatory rules as an indexed family, and intrinsically typed derivations over them.

The Combinatory Projection Principle: syntactic combinatory rules are binary, linearly ordered, type-dependent rules applying to string-adjacent categories. Rule is the modern rule inventory — application, first- and second-order composition in harmonic and crossing variants, each gated on the primary functor's slash modality — and Derivation therefore needs exactly one binary node constructor, so a value of Derivation α c is a derivation of category c and "derives c" is typechecking. Following [Ste19], type-raising is morpholexical — the work of case morphemes, not a syntactic rule — so raised categories enter as lexical leaves, and coordination is likewise lexical: a conjunction is an ordinary entry of category (X \⋆ X) /⋆ X whose star slashes confine it to application. Composition stops at second order, the chapter's full inventory. The substitution rules and the morphemic slash of [Ste19] are not modeled.

Main definitions

• Rule: the binary combinatory rules, indexed by left input, right input, and result category.
• Derivation: intrinsically typed derivations — a lexical leaf or a binary Rule node; Derivation.yield reads off the surface string, Derivation.opCount the number of rule applications, Derivation.HasComp whether composition occurs, and Derivation.LexIn whether every leaf is drawn from a given lexicon.

inductive CCG.Rule (α : Type u_2) : Cat α → Cat α → Cat α → Type u_2

Rule α l r c: a binary combinatory rule instance combining a left constituent of category l with a right constituent of category r to give c. Harmonic rules require the primary slash's modality ≤ diamond, crossing rules ≤ cross; application admits every modality.

• fapp {α : Type u_2} {x y : Cat α} {m : Modality} : Rule α (x.rslash m y) y x

  Forward application >: X/Y Y ⇒ X.

• bapp {α : Type u_2} {x y : Cat α} {m : Modality} : Rule α y (x.lslash m y) x

  Backward application <: Y X\Y ⇒ X.

• fcomp {α : Type u_2} {x y z : Cat α} {m n : Modality} (h : m ≤ Modality.diamond) : Rule α (x.rslash m y) (y.rslash n z) (x.rslash n z)

  Forward harmonic composition >B: X/⋄Y Y/Z ⇒ X/Z.

• bcomp {α : Type u_2} {x y z : Cat α} {m n : Modality} (h : m ≤ Modality.diamond) : Rule α (y.lslash n z) (x.lslash m y) (x.lslash n z)

  Backward harmonic composition <B: Y\Z X\⋄Y ⇒ X\Z.

• fcompx {α : Type u_2} {x y z : Cat α} {m n : Modality} (h : m ≤ Modality.cross) : Rule α (x.rslash m y) (y.lslash n z) (x.lslash n z)

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

• bcompx {α : Type u_2} {x y z : Cat α} {m n : Modality} (h : m ≤ Modality.cross) : Rule α (y.rslash n z) (x.lslash m y) (x.rslash n z)

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

• fcomp2 {α : Type u_2} {x y z w : Cat α} {m n p : Modality} (h : m ≤ Modality.diamond) : Rule α (x.rslash m y) ((y.rslash n z).rslash p w) ((x.rslash n z).rslash p w)

  Forward second-order composition >B²: X/⋄Y (Y/Z)/W ⇒ (X/Z)/W.

• bcomp2 {α : Type u_2} {x y z w : Cat α} {m n p : Modality} (h : m ≤ Modality.diamond) : Rule α ((y.lslash n z).lslash p w) (x.lslash m y) ((x.lslash n z).lslash p w)

  Backward second-order composition <B²: (Y\Z)\W X\⋄Y ⇒ (X\Z)\W.

• fcompx2 {α : Type u_2} {x y z w : Cat α} {m n p : Modality} (h : m ≤ Modality.cross) : Rule α (x.rslash m y) ((y.lslash n z).lslash p w) ((x.lslash n z).lslash p w)

  Forward crossing second-order composition >B²×: X/×Y (Y\Z)\W ⇒ (X\Z)\W.

• bcompx2 {α : Type u_2} {x y z w : Cat α} {m n p : Modality} (h : m ≤ Modality.cross) : Rule α ((y.rslash n z).rslash p w) (x.lslash m y) ((x.rslash n z).rslash p w)

  Backward crossing second-order composition <B²×: (Y/Z)/W X\×Y ⇒ (X/Z)/W.

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

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

Equations

• CCG.Rule.fapp.IsComp = False
• CCG.Rule.bapp.IsComp = False
• x✝.IsComp = True

@[instance_reducible]

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

Equations

• CCG.instDecidableIsComp CCG.Rule.fapp = isFalse ⋯
• CCG.instDecidableIsComp CCG.Rule.bapp = isFalse ⋯
• CCG.instDecidableIsComp (CCG.Rule.fcomp h) = isTrue trivial
• CCG.instDecidableIsComp (CCG.Rule.bcomp h) = isTrue trivial
• CCG.instDecidableIsComp (CCG.Rule.fcompx h) = isTrue trivial
• CCG.instDecidableIsComp (CCG.Rule.bcompx h) = isTrue trivial
• CCG.instDecidableIsComp (CCG.Rule.fcomp2 h) = isTrue trivial
• CCG.instDecidableIsComp (CCG.Rule.bcomp2 h) = isTrue trivial
• CCG.instDecidableIsComp (CCG.Rule.fcompx2 h) = isTrue trivial
• CCG.instDecidableIsComp (CCG.Rule.bcompx2 h) = isTrue trivial

inductive CCG.Derivation (α : Type u_2) : Cat α → Type u_2

A CCG derivation of category c, intrinsically typed: a lexical leaf, or a binary Rule node — the Combinatory Projection Principle's binarity, once. A value of Derivation α c is a well-formed derivation, so "derives c" is typechecking.

• lex {α : Type u_2} (form : String) (c : Cat α) : Derivation α c

  A lexical leaf: a surface form, at category c.

• node {α : Type u_2} {l r c : Cat α} : Rule α l r c → Derivation α l → Derivation α r → Derivation α c

  A binary rule application.

@[reducible, inline]

abbrev CCG.Derivation.fapp {α : Type u_1} {x y : Cat α} {m : Modality} (d₁ : Derivation α (x.rslash m y)) (d₂ : Derivation α y) : Derivation α x

Forward application >.

Equations

• d₁.fapp d₂ = CCG.Derivation.node CCG.Rule.fapp d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.bapp {α : Type u_1} {x y : Cat α} {m : Modality} (d₁ : Derivation α y) (d₂ : Derivation α (x.lslash m y)) : Derivation α x

Backward application <.

Equations

• d₁.bapp d₂ = CCG.Derivation.node CCG.Rule.bapp d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.fcomp {α : Type u_1} {x y z : Cat α} {m n : Modality} (h : m ≤ Modality.diamond) (d₁ : Derivation α (x.rslash m y)) (d₂ : Derivation α (y.rslash n z)) : Derivation α (x.rslash n z)

Forward harmonic composition >B.

Equations

• CCG.Derivation.fcomp h d₁ d₂ = CCG.Derivation.node (CCG.Rule.fcomp h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.bcomp {α : Type u_1} {x y z : Cat α} {m n : Modality} (h : m ≤ Modality.diamond) (d₁ : Derivation α (y.lslash n z)) (d₂ : Derivation α (x.lslash m y)) : Derivation α (x.lslash n z)

Backward harmonic composition <B.

Equations

• CCG.Derivation.bcomp h d₁ d₂ = CCG.Derivation.node (CCG.Rule.bcomp h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.fcompx {α : Type u_1} {x y z : Cat α} {m n : Modality} (h : m ≤ Modality.cross) (d₁ : Derivation α (x.rslash m y)) (d₂ : Derivation α (y.lslash n z)) : Derivation α (x.lslash n z)

Forward crossing composition >B×.

Equations

• CCG.Derivation.fcompx h d₁ d₂ = CCG.Derivation.node (CCG.Rule.fcompx h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.bcompx {α : Type u_1} {x y z : Cat α} {m n : Modality} (h : m ≤ Modality.cross) (d₁ : Derivation α (y.rslash n z)) (d₂ : Derivation α (x.lslash m y)) : Derivation α (x.rslash n z)

Backward crossing composition <B×.

Equations

• CCG.Derivation.bcompx h d₁ d₂ = CCG.Derivation.node (CCG.Rule.bcompx h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.fcomp2 {α : Type u_1} {x y z w : Cat α} {m n p : Modality} (h : m ≤ Modality.diamond) (d₁ : Derivation α (x.rslash m y)) (d₂ : Derivation α ((y.rslash n z).rslash p w)) : Derivation α ((x.rslash n z).rslash p w)

Forward second-order composition >B².

Equations

• CCG.Derivation.fcomp2 h d₁ d₂ = CCG.Derivation.node (CCG.Rule.fcomp2 h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.bcomp2 {α : Type u_1} {x y z w : Cat α} {m n p : Modality} (h : m ≤ Modality.diamond) (d₁ : Derivation α ((y.lslash n z).lslash p w)) (d₂ : Derivation α (x.lslash m y)) : Derivation α ((x.lslash n z).lslash p w)

Backward second-order composition <B².

Equations

• CCG.Derivation.bcomp2 h d₁ d₂ = CCG.Derivation.node (CCG.Rule.bcomp2 h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.fcompx2 {α : Type u_1} {x y z w : Cat α} {m n p : Modality} (h : m ≤ Modality.cross) (d₁ : Derivation α (x.rslash m y)) (d₂ : Derivation α ((y.lslash n z).lslash p w)) : Derivation α ((x.lslash n z).lslash p w)

Forward crossing second-order composition >B²×.

Equations

• CCG.Derivation.fcompx2 h d₁ d₂ = CCG.Derivation.node (CCG.Rule.fcompx2 h) d₁ d₂

@[reducible, inline]

abbrev CCG.Derivation.bcompx2 {α : Type u_1} {x y z w : Cat α} {m n p : Modality} (h : m ≤ Modality.cross) (d₁ : Derivation α ((y.rslash n z).rslash p w)) (d₂ : Derivation α (x.lslash m y)) : Derivation α ((x.rslash n z).rslash p w)

Backward crossing second-order composition <B²×.

Equations

• CCG.Derivation.bcompx2 h d₁ d₂ = CCG.Derivation.node (CCG.Rule.bcompx2 h) d₁ d₂

def CCG.Derivation.yield {α : Type u_1} {c : Cat α} : Derivation α c → List String

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

Rule nodes concatenate their daughters, so the yield is independent of the derivation's combinatory structure — the property that lets a CCG derivation witness a string language.

Equations

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

def CCG.Derivation.opCount {α : Type u_1} {c : Cat α} : Derivation α 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 {α : Type u_1} (L : List (String × Cat α)) {c : Cat α} : Derivation α 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 {α : Type u_1} [DecidableEq α] (L : List (String × Cat α)) {c : Cat α} (d : Derivation α c) : Decidable (LexIn L d)

Equations

• CCG.Derivation.LexIn.decidable L (CCG.Derivation.lex f c) = CCG.Derivation.LexIn.decidable._aux_1 L c f
• CCG.Derivation.LexIn.decidable L (CCG.Derivation.node a d₁ d₂) = instDecidableAnd

def CCG.Derivation.HasComp {α : Type u_1} {c : Cat α} : Derivation α c → Prop

The derivation contains a composition node (of any order 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 {α : Type u_1} {c : Cat α} (d : Derivation α 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