Classical CCG generates a non-context-free language

Formalisation of the construction in [KKS15], Example 2: a rule-restricted combinatory categorial grammar — the classical formalism of [VSW94] and [WJ88] — that generates the non-context-free language aⁿbⁿcⁿ.

The point is theoretical. [KKS15] show that the CCG≡TAG weak equivalence holds for classical CCG, where combinatory rules may be restricted per grammar (here, via the target restriction modelled in Syntax/CCG/Classical: every rule fires only when the target of its primary input category is S). For lexicalized CCG without target restrictions they prove the power is strictly below TAG: such a CCG that covers aⁿbⁿcⁿ also admits extra permuted strings, so it cannot generate the language exactly. Syntax/CCG/Basic's CCG.DerivStep models a (rule-inventory) fragment of that unrestricted variant, so this construction genuinely needs the restricted model CCG.Classical.

Atoms follow the paper (A, B, C, S); we realise them with the project's CCG.Cat atoms as A = NP, B = N, C = PP, S = S — abstract placeholders, the content is generative capacity, not syntax.

Main definitions

• build — the n-indexed CCG.Classical.Derivation of aⁿbⁿcⁿ (cluster of degree-2 compositions, peeled to S by crossed-composition with c and backward-application with a).

Main statements

• build_cat — (build n).cat = some S for n ≥ 1.
• build_yield — (build n).yield = aⁿbⁿcⁿ.
• ccg_generates_anbnc — every aⁿbⁿcⁿ string is generated.

Implementation notes

These are the completeness direction (every target string is generated). The converse soundness (the target-restricted rules generate only count-matched strings) is an all-derivations induction not formalised here; with it, relabelling {"a","b","c"} → ThreeSymbol and AnBnCn.anbnc_not_contextFree would establish that the grammar's language is itself non-context-free.

@[reducible, inline]

abbrev KuhlmannKollerSatta2015.Acat : CCG.Cat

Abstract atom A, realised as NP.

Equations

• KuhlmannKollerSatta2015.Acat = CCG.NP

@[reducible, inline]

abbrev KuhlmannKollerSatta2015.Bcat : CCG.Cat

Abstract atom B, realised as N.

Equations

• KuhlmannKollerSatta2015.Bcat = CCG.N

@[reducible, inline]

abbrev KuhlmannKollerSatta2015.Ccat : CCG.Cat

Abstract atom C, realised as PP.

Equations

• KuhlmannKollerSatta2015.Ccat = CCG.PP

The grammar G₁ of Example 2

def KuhlmannKollerSatta2015.aLex : CCG.Classical.Derivation

a := A.

Equations

• KuhlmannKollerSatta2015.aLex = CCG.Classical.Derivation.lex KuhlmannKollerSatta2015.Acat "a"

def KuhlmannKollerSatta2015.cLex : CCG.Classical.Derivation

c := C\A.

Equations

• KuhlmannKollerSatta2015.cLex = CCG.Classical.Derivation.lex (KuhlmannKollerSatta2015.Ccat.lslash KuhlmannKollerSatta2015.Acat) "c"

def KuhlmannKollerSatta2015.clusterCat : ℕ → CCG.Cat

The cluster category S/C/…/C with n forward C-arguments.

Equations

• KuhlmannKollerSatta2015.clusterCat 0 = CCG.S
• KuhlmannKollerSatta2015.clusterCat n.succ = (KuhlmannKollerSatta2015.clusterCat n).rslash KuhlmannKollerSatta2015.Ccat

def KuhlmannKollerSatta2015.fc2Chain : ℕ → CCG.Classical.Derivation

Chain of degree-2 compositions: b₁ = S/C/B composed with j copies of B/C/B, giving S/Cʲ⁺¹/B and yield bʲ⁺¹.

Equations

• One or more equations did not get rendered due to their size.
• KuhlmannKollerSatta2015.fc2Chain 0 = CCG.Classical.Derivation.lex ((CCG.S.rslash KuhlmannKollerSatta2015.Ccat).rslash KuhlmannKollerSatta2015.Bcat) "b"

def KuhlmannKollerSatta2015.clusterDeriv : ℕ → CCG.Classical.Derivation

The b-cluster derivation for n ≥ 1, with category clusterCat n, yield bⁿ.

Equations

• KuhlmannKollerSatta2015.clusterDeriv 0 = CCG.Classical.Derivation.lex CCG.S "b"
• KuhlmannKollerSatta2015.clusterDeriv 1 = CCG.Classical.Derivation.lex (CCG.S.rslash KuhlmannKollerSatta2015.Ccat) "b"
• KuhlmannKollerSatta2015.clusterDeriv n.succ.succ = (KuhlmannKollerSatta2015.fc2Chain n).fc1 (CCG.Classical.Derivation.lex (KuhlmannKollerSatta2015.Bcat.rslash KuhlmannKollerSatta2015.Ccat) "b")

def KuhlmannKollerSatta2015.peelStep (d : CCG.Classical.Derivation) : CCG.Classical.Derivation

One peel: crossed-compose with a c on the right, then backward-apply an a on the left — wrapping the yield with a … c and removing one C argument.

Equations

• KuhlmannKollerSatta2015.peelStep d = KuhlmannKollerSatta2015.aLex.ba (d.fcx1 KuhlmannKollerSatta2015.cLex)

def KuhlmannKollerSatta2015.peel : ℕ → CCG.Classical.Derivation → CCG.Classical.Derivation

Peel k times.

Equations

• KuhlmannKollerSatta2015.peel 0 x✝ = x✝
• KuhlmannKollerSatta2015.peel k.succ x✝ = KuhlmannKollerSatta2015.peel k (KuhlmannKollerSatta2015.peelStep x✝)

def KuhlmannKollerSatta2015.build (n : ℕ) : CCG.Classical.Derivation

The full derivation of aⁿbⁿcⁿ.

Equations

• KuhlmannKollerSatta2015.build n = KuhlmannKollerSatta2015.peel n (KuhlmannKollerSatta2015.clusterDeriv n)

Target invariant

theorem KuhlmannKollerSatta2015.targetIsS_clusterCat (n : ℕ) : CCG.Classical.targetIsS (clusterCat n) = true

The cluster category always has target S.

Category of the construction (completeness, part 1)

theorem KuhlmannKollerSatta2015.fc2Chain_cat (j : ℕ) : (fc2Chain j).cat = some ((clusterCat (j + 1)).rslash Bcat)

The degree-2 chain composes to S/Cʲ⁺¹/B.

theorem KuhlmannKollerSatta2015.clusterDeriv_cat {n : ℕ} : 1 ≤ n → (clusterDeriv n).cat = some (clusterCat n)

The cluster derivation has category clusterCat n for n ≥ 1.

theorem KuhlmannKollerSatta2015.peelStep_cat {d : CCG.Classical.Derivation} {k : ℕ} (h : d.cat = some (clusterCat (k + 1))) : (peelStep d).cat = some (clusterCat k)

One peel removes one C argument from a cluster.

theorem KuhlmannKollerSatta2015.peel_cat (k : ℕ) (d : CCG.Classical.Derivation) : d.cat = some (clusterCat k) → (peel k d).cat = some CCG.S

Peeling k times turns a clusterCat k derivation into one of category S.

theorem KuhlmannKollerSatta2015.build_cat {n : ℕ} (hn : 1 ≤ n) : (build n).cat = some CCG.S

Completeness, category part. The construction derives S for every n ≥ 1.

Yield of the construction (completeness, part 2)

theorem KuhlmannKollerSatta2015.fc2Chain_yield (j : ℕ) : (fc2Chain j).yield = List.replicate (j + 1) "b"

theorem KuhlmannKollerSatta2015.clusterDeriv_yield {n : ℕ} : 1 ≤ n → (clusterDeriv n).yield = List.replicate n "b"

theorem KuhlmannKollerSatta2015.peel_yield (k : ℕ) (d : CCG.Classical.Derivation) : (peel k d).yield = List.replicate k "a" ++ d.yield ++ List.replicate k "c"

theorem KuhlmannKollerSatta2015.build_yield {n : ℕ} (hn : 1 ≤ n) : (build n).yield = List.replicate n "a" ++ List.replicate n "b" ++ List.replicate n "c"

Completeness, yield part. The construction spells out aⁿbⁿcⁿ.

Generative-capacity result

def KuhlmannKollerSatta2015.anbncStrings : Set (List String)

The string language aⁿbⁿcⁿ (n ≥ 1) over {"a","b","c"}.

Equations

• KuhlmannKollerSatta2015.anbncStrings = {w : List String | ∃ (n : ℕ), 1 ≤ n ∧ w = List.replicate n "a" ++ List.replicate n "b" ++ List.replicate n "c"}

theorem KuhlmannKollerSatta2015.ccg_generates_anbnc (w : List String) (hw : w ∈ anbncStrings) : ∃ (d : CCG.Classical.Derivation), d.cat = some CCG.S ∧ d.yield = w

The construction generates aⁿbⁿcⁿ ([KKS15], Ex. 2): every string in the non-context-free language is the yield of a well-formed (target- restricted) CCG derivation. This is the completeness half of CCG ⊋ CFG; the language anbnc it covers is not context-free (AnBnCn.anbnc_not_contextFree).