def CCG.GenerativeCapacity.categoryToSymbol (isArg : Bool) (pos : ℕ) : FourSymbol

Mapping from CCG categories to abstract symbols.

For the cross-serial pattern:

• NP maps to 'a' or 'b' (arguments)
• V maps to 'c' or 'd' (verbs)

Equations

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

structure CCG.GenerativeCapacity.SimpleAnnotatedDerivation : Type

A CCG derivation annotated with surface words.

Used here for the generative capacity proof; the full AnnotatedDerivation with binding information is in the bridge file Phenomena.FillerGap.CCG_CrossSerialBridge.

• deriv : CrossSerial.ExtDerivStep

  The derivation

• words : List String

  Surface words

instance CCG.GenerativeCapacity.instReprSimpleAnnotatedDerivation : Repr SimpleAnnotatedDerivation

Equations

• CCG.GenerativeCapacity.instReprSimpleAnnotatedDerivation = { reprPrec := CCG.GenerativeCapacity.instReprSimpleAnnotatedDerivation.repr }

def CCG.GenerativeCapacity.instReprSimpleAnnotatedDerivation.repr : SimpleAnnotatedDerivation → ℕ → Std.Format

Equations

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

def CCG.GenerativeCapacity.dutch_2v_deriv : SimpleAnnotatedDerivation

Simple annotated derivation for "Jan Piet zag zwemmen".

Equations

• CCG.GenerativeCapacity.dutch_2v_deriv = { deriv := CCG.CrossSerial.jan_zag_zwemmen_piet, words := ["Jan", "Piet", "zag", "zwemmen"] }

theorem CCG.GenerativeCapacity.ccg_produces_cross_serial_2v : ∃ (derivation : SimpleAnnotatedDerivation), derivation.words.length = 2 * 2

A CCG derivation for 2-fold cross-serial dependencies yields a string of length 2 * 2 = 4 (the "Jan Piet zag zwemmen" pattern).

The derivation structure (via B² composition) ensures that:

• 2 NPs yield the argument positions
• 2 Vs yield the verb positions
• The composition threads arguments through verbs correctly

theorem CCG.GenerativeCapacity.ccg_generates_cross_serial_language (n : ℕ) : ∃ (w : FourString), isInLanguage_anbncndn w = true ∧ w = makeString_anbncndn n

The language of CCG derivations for cross-serial dependencies includes {aⁿbⁿcⁿdⁿ}.

More precisely: for each n, there exists a CCG derivation whose yield corresponds to aⁿbⁿcⁿdⁿ.

theorem CCG.GenerativeCapacity.ccg_strictly_more_expressive_than_cfg : (∀ (n : ℕ), isInLanguage_anbncndn (makeString_anbncndn n) = true) ∧ ¬HasPumpingProperty4 isInLanguage_anbncndn

CCG is strictly more expressive than CFG.

1. CCG generates {aⁿbⁿcⁿdⁿ} (via generalized composition)
2. {aⁿbⁿcⁿdⁿ} lacks the CFL pumping property (hence is not context-free)
3. Therefore: CCG can generate languages that CFG cannot

theorem CCG.GenerativeCapacity.ccg_exceeds_cfg : Core.FormalLanguageType.contextFree < Core.FormalLanguageType.mildlyContextSensitive

CCG strictly exceeds context-free power: it generates {aⁿbⁿcⁿdⁿ}, which is not context-free.