Kuhlmann, Koller and Satta (2015): Lexicalization and Generative Power in CCG

This file formalizes Example 2 of [KKS15], the grammar G₁ in the formalism of [VSW94] and [WJ88] whose rules of application and of composition of degree at most 2 are restricted to primary inputs with target S, and proves that its language is aⁿbⁿcⁿ without the empty word (language_eq_anbncn_sub_one). The completeness half follows the paper's derivation: the bs are composed into a cluster S/C/…/C (cluster_derives), and each C argument is peeled off by crossed-composing a c and backward-applying an a (peel_derives). The soundness half is an induction on derivability showing that every derivable pair has one of the shapes that construction produces (reachable_of_derives). The language is therefore not context-free (not_isContextFree_language), the fact the proof of Theorem 3 invokes.

The paper's results turn on two properties of rule restrictions, which are stated here for the substrate's rule systems: prefix-closedness (Definition 2) and the absence of target restrictions (Definition 3). Every target-restricted rule system is prefix-closed, so the rule system of G₁ is (Example 6), but it is not without target restrictions (Example 8). This is the configuration the paper's Theorems 2 and 3 separate: prefix-closed grammars with target restrictions are weakly equivalent to tree-adjoining grammar, and without them they cannot generate aⁿbⁿcⁿ.

Implementation notes

The atoms A, B, C, S and the letters a, b, c are the study's own types, since CCG.Grammar is parameterized over both. The lexical entry for c is C\A, the direction the paper's derivation of aⁿbⁿcⁿ requires. The language is stated against Language.anbncn, and the empty word drops out because no CCG grammar derives it (CCG.Grammar.Derives.ne_nil).

TODO

• Theorems 1–4 and the main lemma (a Parikh-equivalent context-free sublanguage for every prefix-closed grammar without target restrictions) are not formalized.

References

• [KKS15]
• [VSW94]
• [WJ88]
• [SM21]

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

inductive KuhlmannKollerSatta2015.Letter : Type

The terminal letters of the paper's Example 2 grammar.

• a : Letter
• b : Letter
• c : Letter

@[instance_reducible]

instance KuhlmannKollerSatta2015.instReprLetter : Repr Letter

Equations

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

def KuhlmannKollerSatta2015.instReprLetter.repr : Letter → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KuhlmannKollerSatta2015.instDecidableEqLetter : DecidableEq Letter

Equations

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

def KuhlmannKollerSatta2015.exampleGrammar : CCG.Grammar Letter Atom

The grammar G₁ of Example 2 has six lexical entries, its target restriction and start at S, and degree bound 2, an instance of the ε-free degree-2 normal form of [SM21].

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

@[simp]

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

The cluster category always has target S.

The construction, as Derives inductions

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

Composing b₁ = S/C/B with j copies of B/C/B at degree 2 derives bʲ⁺¹ at S/Cʲ⁺¹/B.

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

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

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

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 Letter → Prop

The category/string pairs that G₁ derives, namely 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 Letter} (h : exampleGrammar.Derives c w) : Reachable c w

Every pair G₁ derives is Reachable, by rule induction. The target gate admits only primaries with target S, and a secondary Yβ over an atom Y has Y as its target and β as its arguments, so each rule step is one of the four instances of the completeness construction.

Rule restrictions (§3.1, §3.3)

def KuhlmannKollerSatta2015.PrefixClosed {α : Type u_1} (R : CCG.RuleSystem α) : Prop

A rule system is prefix-closed (Definition 2) when every permitted instance X/Y Yβ ⇒ Xβ of composition stays permitted for every prefix β' of the argument sequence β, that is, with the outermost arguments of the secondary input already consumed, at the lowered degree.

Equations

• KuhlmannKollerSatta2015.PrefixClosed R = ∀ (x : CCG.Cat α) (a : CCG.Cat.Arg α) (β β' : List (CCG.Cat.Arg α)), β' <+: β → R x a β → R x a β'

def KuhlmannKollerSatta2015.WithoutTargetRestrictions {α : Type u_1} (R : CCG.RuleSystem α) : Prop

A rule system is without target restrictions (Definition 3) when every permitted instance X/Y Yβ ⇒ Xβ stays permitted under any change of the primary input's result category X.

Equations

• KuhlmannKollerSatta2015.WithoutTargetRestrictions R = ∀ (x x' : CCG.Cat α) (a : CCG.Cat.Arg α) (β : List (CCG.Cat.Arg α)), R x a β → R x' a β

theorem KuhlmannKollerSatta2015.targetRestricted_prefixClosed {α : Type u_1} (s : α) (d : ℕ) : PrefixClosed (CCG.RuleSystem.targetRestricted s d)

A target-restricted rule system is prefix-closed: it looks only at the degree and the primary input's target.

theorem KuhlmannKollerSatta2015.exampleGrammar_prefixClosed : PrefixClosed exampleGrammar.rules

G₁ is prefix-closed (Example 6).

theorem KuhlmannKollerSatta2015.exampleGrammar_not_withoutTargetRestrictions : ¬WithoutTargetRestrictions exampleGrammar.rules

G₁ is not without target restrictions (Example 8), since application of S/C to C is permitted but application of B/C to C is not.

Generative-capacity result

theorem KuhlmannKollerSatta2015.anbncn_sub_one_subset_language : Language.anbncn Letter.a Letter.b Letter.c - 1 ≤ exampleGrammar.language

G₁ generates every nonempty word of aⁿbⁿcⁿ ([KKS15], Example 2), the completeness half of the example.

theorem KuhlmannKollerSatta2015.language_subset_anbncn : exampleGrammar.language ≤ Language.anbncn Letter.a Letter.b Letter.c

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

theorem KuhlmannKollerSatta2015.language_eq_anbncn_sub_one : exampleGrammar.language = Language.anbncn Letter.a Letter.b Letter.c - 1

The language of G₁ is aⁿbⁿcⁿ without the empty word ([KKS15], Example 2).

theorem KuhlmannKollerSatta2015.not_isContextFree_language : ¬exampleGrammar.language.IsContextFree

The language of G₁ is not context-free, since it contains aⁿbⁿcⁿ for every n ≥ 1 and each of its words has as many a as b as c. The proof of Theorem 3 of [KKS15] invokes this standard fact (p. 202) without proving it.