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.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

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.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

def CCG.CrossSerial.helpen_zwemmen_simple : ExtDerivStep

Equations

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

def CCG.CrossSerial.zag_helpen_zwemmen : ExtDerivStep

Equations

• CCG.CrossSerial.zag_helpen_zwemmen = CCG.CrossSerial.zag_lex.fapp CCG.CrossSerial.helpen_zwemmen_simple

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.zag_helpen_zwemmen

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"