Classical (rule-restricted) CCG

The classical CCG formalism of [VSW94] and [WJ88], in which combinatory rules may be restricted per grammar. Following [KKS15], the restriction modelled here is a target restriction: a rule fires only when the target of its primary input category (the leftmost atom, after stripping all arguments) is the distinguished atom S.

This is the substrate that makes the CCG≡TAG weak-equivalence — and constructions of CCGs for non-context-free languages — expressible. It is distinct from the unrestricted, universal-rule CCG of Syntax/CCG/Basic (CCG.DerivStep), which [KKS15] show is strictly weaker than TAG.

Main definitions

• CCG.Classical.target / targetIsS — the target of a category, and the restriction.
• fapp, bapp, fcomp1, fcomp2, fcompX1 — application and (harmonic/crossed) composition, each gated on target (primary) = S.
• CCG.Classical.Derivation — a derivation under these restricted rules, with cat/yield.

Implementation notes

These rules are the fragment of [KKS15]'s rule schema exercised by the constructions in Studies/KuhlmannKollerSatta2015 and Syntax/CCG/CrossSerial: forward/backward application, forward harmonic composition of degree 1–2, and forward crossed composition of degree 1. (The full schema also permits backward composition and degree-2 crossed composition; the harmonic/crossed distinction is a consequence of the slash directions, not a separate rule class. Those instances are simply not needed here.) The target restriction is fixed to S, the common case in [KKS15] Example 2 and in [Ste00a]; general VW-CCG permits other per-grammar restrictions.

def CCG.Classical.target : Cat → Atom

The target of a category: its leftmost atom (strip all arguments).

Equations

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

def CCG.Classical.targetIsS (c : Cat) : Bool

Whether a category's target is the distinguished atom S.

Equations

• CCG.Classical.targetIsS c = match CCG.Classical.target c with | CCG.Atom.S => true | x => false

@[simp]

theorem CCG.Classical.targetIsS_rslash (x y : Cat) : targetIsS (x.rslash y) = targetIsS x

@[simp]

theorem CCG.Classical.targetIsS_lslash (x y : Cat) : targetIsS (x.lslash y) = targetIsS x

Rule-restricted combinatory rules

Each rule is gated on target (primary) = S (the target restriction of [KKS15], Example 2).

def CCG.Classical.fapp : Cat → Cat → Option Cat

Forward application: (X/Y) Y ⇒ X, target of the functor S.

Equations

• CCG.Classical.fapp (x_2.rslash y) x✝ = if (CCG.Classical.targetIsS (x_2.rslash y) && y == x✝) = true then some x_2 else none
• CCG.Classical.fapp x✝¹ x✝ = none

def CCG.Classical.bapp : Cat → Cat → Option Cat

Backward application: Y (X\Y) ⇒ X, target of the functor S.

Equations

• CCG.Classical.bapp x✝ (x_2.lslash y') = if (CCG.Classical.targetIsS (x_2.lslash y') && x✝ == y') = true then some x_2 else none
• CCG.Classical.bapp x✝¹ x✝ = none

def CCG.Classical.fcomp1 : Cat → Cat → Option Cat

Forward composition, degree 1 (harmonic): (X/Y) (Y/Z) ⇒ X/Z, target S.

Equations

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

def CCG.Classical.fcomp2 : Cat → Cat → Option Cat

Forward composition, degree 2 (harmonic): (X/Y) (Y/Z/W) ⇒ X/Z/W, target S.

Equations

• CCG.Classical.fcomp2 (x_2.rslash y) ((y'.rslash z).rslash w) = if (CCG.Classical.targetIsS (x_2.rslash y) && y == y') = true then some ((x_2.rslash z).rslash w) else none
• CCG.Classical.fcomp2 x✝¹ x✝ = none

def CCG.Classical.fcompX1 : Cat → Cat → Option Cat

Forward crossed composition, degree 1: (X/Y) (Y\Z) ⇒ X\Z, target S.

Equations

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

Derivations

inductive CCG.Classical.Derivation : Type

A derivation under the rule-restricted rules.

• lex : Cat → String → Derivation
• fa : Derivation → Derivation → Derivation
• ba : Derivation → Derivation → Derivation
• fc1 : Derivation → Derivation → Derivation
• fc2 : Derivation → Derivation → Derivation
• fcx1 : Derivation → Derivation → Derivation

@[implicit_reducible]

instance CCG.Classical.instReprDerivation : Repr Derivation

Equations

• CCG.Classical.instReprDerivation = { reprPrec := CCG.Classical.instReprDerivation.repr }

def CCG.Classical.instReprDerivation.repr : Derivation → ℕ → Std.Format

Equations

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

def CCG.Classical.Derivation.cat : Derivation → Option Cat

The category derived, threading the restricted rules (none if any rule is illegal, e.g. its target restriction fails).

Equations

• (CCG.Classical.Derivation.lex a a_1).cat = some a
• (a.fa a_1).cat = do let a ← a.cat let b ← a_1.cat CCG.Classical.fapp a b
• (a.ba a_1).cat = do let a ← a.cat let b ← a_1.cat CCG.Classical.bapp a b
• (a.fc1 a_1).cat = do let a ← a.cat let b ← a_1.cat CCG.Classical.fcomp1 a b
• (a.fc2 a_1).cat = do let a ← a.cat let b ← a_1.cat CCG.Classical.fcomp2 a b
• (a.fcx1 a_1).cat = do let a ← a.cat let b ← a_1.cat CCG.Classical.fcompX1 a b

def CCG.Classical.Derivation.yield : Derivation → List String

Surface string: leaf forms left to right.

Equations

• (CCG.Classical.Derivation.lex a a_1).yield = [a_1]
• (a.fa a_1).yield = a.yield ++ a_1.yield
• (a.ba a_1).yield = a.yield ++ a_1.yield
• (a.fc1 a_1).yield = a.yield ++ a_1.yield
• (a.fc2 a_1).yield = a.yield ++ a_1.yield
• (a.fcx1 a_1).yield = a.yield ++ a_1.yield