def CCG.CrossSerial.VP : Cat

Verb phrase (infinitival)

Equations

• CCG.CrossSerial.VP = CCG.S.lslash CCG.NP

def CCG.CrossSerial.ControlV : Cat

Control verb: takes VP, gives VP (e.g., "helpen" = help)

Equations

• CCG.CrossSerial.ControlV = CCG.CrossSerial.VP.rslash CCG.CrossSerial.VP

def CCG.CrossSerial.PercV : Cat

Perception verb: takes VP, gives TV-like (e.g., "zag" = saw)

Equations

• CCG.CrossSerial.PercV = (CCG.S.lslash CCG.NP).rslash CCG.CrossSerial.VP

def CCG.CrossSerial.InfTV : Cat

Infinitival transitive: VP/NP (e.g., "zwemmen" when taking object)

Equations

• CCG.CrossSerial.InfTV = CCG.CrossSerial.VP.rslash CCG.NP

def CCG.CrossSerial.InfSubj : Cat

Infinitival verb needing subject (for cross-serial): (S\NP)/NP

In Dutch verb-raising constructions, the infinitive's subject appears in what looks like an object position. This category allows the embedded subject to be picked up via composition.

zwemmen : (S\NP)/NP — "swim" needing its subject as argument

This differs from the simple intransitive VP = S\NP.

Equations

• CCG.CrossSerial.InfSubj = (CCG.S.lslash CCG.NP).rslash CCG.NP

def CCG.CrossSerial.ControlVR : Cat

Verb-raising control verb: ((S\NP)/NP)/(S\NP)

In verb-raising constructions with 3+ verbs, each intermediate restructuring verb (helpen, laten) must provide an extra /NP slot for its own raised subject. Standard ControlV = (S\NP)/(S\NP) only passes through the complement's arguments; ControlVR adds an /NP so the verb's subject can be picked up via composition.

This is what enables the full cross-serial derivation:

• zwemmen : (S\NP)/NP — base: needs subject
• helpen : ((S\NP)/NP)/(S\NP) — VR: needs complement + passes NP
• zag : (S\NP)/(S\NP) — matrix: standard perception verb

Equations

• CCG.CrossSerial.ControlVR = ((CCG.S.lslash CCG.NP).rslash CCG.NP).rslash (CCG.S.lslash CCG.NP)

def CCG.CrossSerial.forwardComp2 : Cat → Cat → Option Cat

Forward Composition² (B²): X/Y (Y/Z)/W → (X/Z)/W

Allows "reaching through" one extra argument.

Equations

• CCG.CrossSerial.forwardComp2 (x_2.rslash y) ((y'.rslash z).rslash w) = if (y == y') = true then some ((x_2.rslash z).rslash w) else none
• CCG.CrossSerial.forwardComp2 x✝¹ x✝ = none

def CCG.CrossSerial.forwardComp3 : Cat → Cat → Option Cat

Forward Composition³ (B³): X/Y ((Y/Z)/W)/V → ((X/Z)/W)/V

Allows "reaching through" two extra arguments.

Equations

• CCG.CrossSerial.forwardComp3 (x_2.rslash y) (((y'.rslash z).rslash w).rslash v) = if (y == y') = true then some (((x_2.rslash z).rslash w).rslash v) else none
• CCG.CrossSerial.forwardComp3 x✝¹ x✝ = none

inductive CCG.CrossSerial.ExtDerivStep : Type

Extended derivation with generalized composition.

• lex : LexEntry → ExtDerivStep
• fapp : ExtDerivStep → ExtDerivStep → ExtDerivStep
• bapp : ExtDerivStep → ExtDerivStep → ExtDerivStep
• fcomp : ExtDerivStep → ExtDerivStep → ExtDerivStep
• fcomp2 : ExtDerivStep → ExtDerivStep → ExtDerivStep
• fcomp3 : ExtDerivStep → ExtDerivStep → ExtDerivStep
• ftr : ExtDerivStep → Cat → ExtDerivStep

@[implicit_reducible]

instance CCG.CrossSerial.instReprExtDerivStep : Repr ExtDerivStep

Equations

• CCG.CrossSerial.instReprExtDerivStep = { reprPrec := CCG.CrossSerial.instReprExtDerivStep.repr }

def CCG.CrossSerial.instReprExtDerivStep.repr : ExtDerivStep → Nat → Std.Format

Equations

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

def CCG.CrossSerial.ExtDerivStep.cat : ExtDerivStep → Option Cat

Get category from extended derivation

Equations

• (CCG.CrossSerial.ExtDerivStep.lex a).cat = some a.cat
• (a.fapp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.forwardApp c1 c2
• (a.bapp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.backwardApp c1 c2
• (a.fcomp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.forwardComp c1 c2
• (a.fcomp2 a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.CrossSerial.forwardComp2 c1 c2
• (a.fcomp3 a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.CrossSerial.forwardComp3 c1 c2
• (a.ftr a_1).cat = do let x ← a.cat some (CCG.forwardTypeRaise x a_1)

def CCG.CrossSerial.dutchLexicon : List LexEntry

Equations

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

def CCG.CrossSerial.jan_lex : ExtDerivStep

Equations

• CCG.CrossSerial.jan_lex = CCG.CrossSerial.ExtDerivStep.lex { form := "Jan", cat := CCG.NP }

def CCG.CrossSerial.piet_lex : ExtDerivStep

Equations

• CCG.CrossSerial.piet_lex = CCG.CrossSerial.ExtDerivStep.lex { form := "Piet", cat := CCG.NP }

def CCG.CrossSerial.marie_lex : ExtDerivStep

Equations

• CCG.CrossSerial.marie_lex = CCG.CrossSerial.ExtDerivStep.lex { form := "Marie", cat := CCG.NP }

def CCG.CrossSerial.karel_lex : ExtDerivStep

Equations

• CCG.CrossSerial.karel_lex = CCG.CrossSerial.ExtDerivStep.lex { form := "Karel", cat := CCG.NP }

def CCG.CrossSerial.zag_lex : ExtDerivStep

Equations

• CCG.CrossSerial.zag_lex = CCG.CrossSerial.ExtDerivStep.lex { form := "zag", cat := CCG.CrossSerial.PercV }

def CCG.CrossSerial.helpen_lex : ExtDerivStep

Equations

• CCG.CrossSerial.helpen_lex = CCG.CrossSerial.ExtDerivStep.lex { form := "helpen", cat := CCG.CrossSerial.ControlV }

def CCG.CrossSerial.laten_lex : ExtDerivStep

Equations

• CCG.CrossSerial.laten_lex = CCG.CrossSerial.ExtDerivStep.lex { form := "laten", cat := CCG.CrossSerial.ControlV }

def CCG.CrossSerial.zwemmen_vr : ExtDerivStep

zwemmen with InfSubj category for verb-raising

Equations

• CCG.CrossSerial.zwemmen_vr = CCG.CrossSerial.ExtDerivStep.lex { form := "zwemmen", cat := CCG.CrossSerial.InfSubj }

def CCG.CrossSerial.helpen_vr : ExtDerivStep

helpen with ControlVR category for verb-raising (3+ verb clusters)

Equations

• CCG.CrossSerial.helpen_vr = CCG.CrossSerial.ExtDerivStep.lex { form := "helpen", cat := CCG.CrossSerial.ControlVR }

def CCG.CrossSerial.laten_vr : ExtDerivStep

laten with ControlVR category for verb-raising

Equations

• CCG.CrossSerial.laten_vr = CCG.CrossSerial.ExtDerivStep.lex { form := "laten", cat := CCG.CrossSerial.ControlVR }

def CCG.CrossSerial.zag_comp_zwemmen : ExtDerivStep

Equations

• CCG.CrossSerial.zag_comp_zwemmen = CCG.CrossSerial.zag_lex.fcomp CCG.CrossSerial.zwemmen_vr

def CCG.CrossSerial.zag_zwemmen_piet : ExtDerivStep

Equations

• CCG.CrossSerial.zag_zwemmen_piet = CCG.CrossSerial.zag_comp_zwemmen.fapp CCG.CrossSerial.piet_lex

def CCG.CrossSerial.jan_zag_zwemmen_piet : ExtDerivStep

Equations

• CCG.CrossSerial.jan_zag_zwemmen_piet = CCG.CrossSerial.jan_lex.bapp CCG.CrossSerial.zag_zwemmen_piet

Full cross-serial derivation for 3 verbs

For "Jan Piet Marie zag helpen zwemmen" (Jan saw Piet help Marie swim), the cross-serial bindings are: Jan→zag, Piet→helpen, Marie→zwemmen.

The key is the verb-raising category ControlVR = ((S\NP)/NP)/(S\NP): helpen in verb-raising passes through an /NP slot for its raised subject (Piet), in addition to taking its VP complement. This lets B² thread both Piet's and Marie's argument slots through the verb cluster:

helpen_vr >B zwemmen_vr : ((S\NP)/NP)/(S\NP) >B (S\NP)/NP = ((S\NP)/NP)/NP
zag >B² result          : (S\NP)/(S\NP) >B² ((S\NP)/NP)/NP = ((S\NP)/NP)/NP
result + Marie          : ((S\NP)/NP)/NP + NP = (S\NP)/NP       — Marie→zwemmen
result + Piet           : (S\NP)/NP + NP = S\NP                 — Piet→helpen
Jan + result            : NP + S\NP = S                          — Jan→zag

The outermost /NP originates from zwemmen_vr, so Marie binds with zwemmen. The inner /NP originates from helpen_vr, so Piet binds with helpen. The \NP is zag's subject slot, so Jan binds with zag.

def CCG.CrossSerial.helpen_comp_zwemmen : ExtDerivStep

Equations

• CCG.CrossSerial.helpen_comp_zwemmen = CCG.CrossSerial.helpen_vr.fcomp CCG.CrossSerial.zwemmen_vr

def CCG.CrossSerial.zag_comp2_helpen_zwemmen : ExtDerivStep

Equations

• CCG.CrossSerial.zag_comp2_helpen_zwemmen = CCG.CrossSerial.zag_lex.fcomp2 CCG.CrossSerial.helpen_comp_zwemmen

def CCG.CrossSerial.verbs_marie : ExtDerivStep

Equations

• CCG.CrossSerial.verbs_marie = CCG.CrossSerial.zag_comp2_helpen_zwemmen.fapp CCG.CrossSerial.marie_lex

def CCG.CrossSerial.verbs_marie_piet : ExtDerivStep

Equations

• CCG.CrossSerial.verbs_marie_piet = CCG.CrossSerial.verbs_marie.fapp CCG.CrossSerial.piet_lex

def CCG.CrossSerial.jan_piet_marie_zag_helpen_zwemmen_deriv : ExtDerivStep

Equations

• CCG.CrossSerial.jan_piet_marie_zag_helpen_zwemmen_deriv = CCG.CrossSerial.jan_lex.bapp CCG.CrossSerial.verbs_marie_piet

theorem CCG.CrossSerial.two_np_derives_S : jan_zag_zwemmen_piet.cat = some S

The 2-NP cross-serial derivation yields category S.

theorem CCG.CrossSerial.three_np_derives_S : jan_piet_marie_zag_helpen_zwemmen_deriv.cat = some S

The 3-NP cross-serial derivation yields category S. This uses B (forward composition) and B² (generalized composition) to thread all three NP argument slots through the verb cluster.

theorem CCG.CrossSerial.verb_cluster_cat : zag_comp2_helpen_zwemmen.cat = some (((S.lslash NP).rslash NP).rslash NP)

Intermediate: the verb cluster composes into ((S\NP)/NP)/NP, a 3-place predicate needing Jan (\NP), Piet (/NP), Marie (/NP).

def CCG.CrossSerial.crossSerialLanguage (n : Nat) : List String

The cross-serial language {aⁿbⁿcⁿ | n ≥ 1} is NOT context-free.

CCG can generate this via generalized composition, proving CCG is mildly context-sensitive.

Equations

• CCG.CrossSerial.crossSerialLanguage n = List.replicate n "a" ++ List.replicate n "b" ++ List.replicate n "c"