Target-restricted CCG generates a non-context-free language

Formalisation of the construction in [KKS15], Example 2: a target-restricted combinatory categorial grammar — the formalism of [VSW94] and [WJ88], "VW-CCG" in the paper's terminology — that generates the non-context-free language aⁿbⁿcⁿ.

The point is theoretical. [KKS15] show that the CCG≡TAG weak equivalence holds for target-restricted CCG, where combinatory rules may be restricted per grammar (here, via the target restriction modelled in Syntax/CCG/Grammar: 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/Derivation's CCG.Derivation models a (rule-inventory) fragment of that unrestricted variant, so this construction genuinely needs the restricted model CCG.Grammar.

Atoms follow the paper (A, B, C, S) as the study's own atom type — CCG.Cat is parameterized over its atoms, so the construction needs no proxy inventory.

Main definitions

• exampleGrammar — the grammar G₁ of Example 2: six lexical entries, target restriction and start at S, degree bound 2.

Main statements

• cluster_derives — the b-cluster: G₁ derives bⁿ at category S/Cⁿ.
• peel_derives — peeling: each C argument is discharged by crossed-composing a c and backward-applying an a, wrapping the string as a … c.
• ccg_generates_anbnc — anbncStrings ⊆ exampleGrammar.language.

Implementation notes

These are the completeness direction (anbncStrings ⊆ exampleGrammar.language). The converse soundness (exampleGrammar.language ⊆ anbncStrings, an induction on Grammar.Derives) is stateable but 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.

inductive KuhlmannKollerSatta2015.Atom : Type

The atomic categories of the paper's Example 2 grammar.

• A : Atom
• B : Atom
• C : Atom
• S : Atom

  The distinguished atom the target restriction is stated at.

def KuhlmannKollerSatta2015.instReprAtom.repr : Atom → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KuhlmannKollerSatta2015.instReprAtom : Repr Atom

Equations

• KuhlmannKollerSatta2015.instReprAtom = { reprPrec := KuhlmannKollerSatta2015.instReprAtom.repr }

@[instance_reducible]

instance KuhlmannKollerSatta2015.instDecidableEqAtom : DecidableEq Atom

Equations

• KuhlmannKollerSatta2015.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev KuhlmannKollerSatta2015.Acat : CCG.Cat Atom

Equations

• KuhlmannKollerSatta2015.Acat = CCG.Cat.atom KuhlmannKollerSatta2015.Atom.A

@[reducible, inline]

abbrev KuhlmannKollerSatta2015.Bcat : CCG.Cat Atom

Equations

• KuhlmannKollerSatta2015.Bcat = CCG.Cat.atom KuhlmannKollerSatta2015.Atom.B

@[reducible, inline]

abbrev KuhlmannKollerSatta2015.Ccat : CCG.Cat Atom

Equations

• KuhlmannKollerSatta2015.Ccat = CCG.Cat.atom KuhlmannKollerSatta2015.Atom.C

@[reducible, inline]

abbrev KuhlmannKollerSatta2015.Scat : CCG.Cat Atom

Equations

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

def KuhlmannKollerSatta2015.exampleGrammar : CCG.Grammar Atom

The grammar G₁ of Example 2: the six lexical entries, target restriction and start at S, degree bound 2 — an instance of the modern capacity object ([SM21]: ε-free, degree at most 2).

Equations

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

def KuhlmannKollerSatta2015.clusterCat : ℕ → CCG.Cat Atom

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

Equations

• KuhlmannKollerSatta2015.clusterCat 0 = KuhlmannKollerSatta2015.Scat
• KuhlmannKollerSatta2015.clusterCat n.succ = (KuhlmannKollerSatta2015.clusterCat n).rslash CCG.Modality.dot KuhlmannKollerSatta2015.Ccat

theorem KuhlmannKollerSatta2015.target_clusterCat (n : ℕ) : (clusterCat n).target = Atom.S

The cluster category always has target S.

@[simp]

theorem KuhlmannKollerSatta2015.acat_ne_clusterCat (k : ℕ) : Acat ≠ clusterCat k

No non-S atom is a cluster category: targets differ.

@[simp]

theorem KuhlmannKollerSatta2015.bcat_ne_clusterCat (k : ℕ) : Bcat ≠ clusterCat k

@[simp]

theorem KuhlmannKollerSatta2015.ccat_ne_clusterCat (k : ℕ) : Ccat ≠ clusterCat k

The construction, as Derives inductions

theorem KuhlmannKollerSatta2015.fc2Chain_derives (j : ℕ) : exampleGrammar.Derives ((clusterCat (j + 1)).rslash CCG.Modality.dot Bcat) (List.replicate (j + 1) "b")

Chain of degree-2 compositions: b₁ = S/C/B composed with j copies of B/C/B derives bʲ⁺¹ at S/Cʲ⁺¹/B.

theorem KuhlmannKollerSatta2015.cluster_derives {n : ℕ} : 1 ≤ n → exampleGrammar.Derives (clusterCat n) (List.replicate n "b")

The b-cluster: G₁ derives bⁿ at category clusterCat n, for n ≥ 1.

theorem KuhlmannKollerSatta2015.peel_derives (k : ℕ) {w : List String} : exampleGrammar.Derives (clusterCat k) w → exampleGrammar.Derives Scat (List.replicate k "a" ++ w ++ List.replicate k "c")

Peeling: from a derivation of w at clusterCat k, crossed-composing a c and backward-applying an a k times derives aᵏ w cᵏ at S.

Soundness

The converse induction: every pair the grammar derives has one of the shapes of the completeness construction, so the language contains nothing beyond aⁿbⁿcⁿ.

def KuhlmannKollerSatta2015.Reachable : CCG.Cat Atom → List String → Prop

The derivable category/string pairs of G₁: the six lexical shapes, the degree-2 chain categories, the clusters (wrapped by i peels), and the peel intermediates.

Equations

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

theorem KuhlmannKollerSatta2015.reachable_of_derives {c : CCG.Cat Atom} {w : List String} (h : exampleGrammar.Derives c w) : Reachable c w

Every pair G₁ derives is Reachable: the rule induction. The target gate kills every primary whose target is not S; the schema equation then forces one of the four rule instances of the completeness construction.

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 : anbncStrings ⊆ exampleGrammar.language

G₁ generates aⁿbⁿcⁿ ([KKS15], Ex. 2): every string in the non-context-free language is in the grammar's language. This is the completeness half of CCG ⊋ CFG; the language anbnc it covers is not context-free (AnBnCn.anbnc_not_contextFree).

theorem KuhlmannKollerSatta2015.language_subset_anbnc : exampleGrammar.language ⊆ anbncStrings

Soundness: G₁ derives nothing beyond aⁿbⁿcⁿ.

theorem KuhlmannKollerSatta2015.language_eq_anbnc : exampleGrammar.language = anbncStrings

The language of G₁ is exactly aⁿbⁿcⁿ ([KKS15], Ex. 2): completeness and soundness together.