CCG Cross-Serial Bridge

@cite{bresnan-etal-1982} @cite{steedman-2000}

Connects CCG derivations (from Theories.Syntax.CCG.CrossSerial) to empirical cross-serial dependency data (from Phenomena.WordOrder.CrossSerial).

Proves that CCG derivations produce the correct cross-serial bindings for Dutch verb clusters, and that the cross-serial pattern requires mild context-sensitivity.

structure Steedman2000CrossSerial.AnnotatedDerivation : Type

A CCG derivation annotated with which NP binds to which verb.

• n : ℕ

  Number of NP-verb pairs

• deriv : CCG.CrossSerial.ExtDerivStep

  The derivation

• words : List String

  Surface words

• binding : Features.VerbClusterBinding self.n

  The NP-verb binding permutation

def Steedman2000CrossSerial.instReprAnnotatedDerivation.repr : AnnotatedDerivation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Steedman2000CrossSerial.instReprAnnotatedDerivation : Repr AnnotatedDerivation

Equations

• Steedman2000CrossSerial.instReprAnnotatedDerivation = { reprPrec := Steedman2000CrossSerial.instReprAnnotatedDerivation.repr }

def Steedman2000CrossSerial.dutch_jan_piet_zag_zwemmen : AnnotatedDerivation

Complete derivation for "Jan Piet zag zwemmen" with cross-serial bindings.

The derivation tree encodes the semantic dependencies:

• Jan combines with the matrix clause (subject of "zag")
• Piet is the argument picked up by zwemmen (subject of "zwemmen")

Equations

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

def Steedman2000CrossSerial.dutch_jan_piet_marie_zag_helpen_zwemmen : AnnotatedDerivation

Derivation for "Jan Piet Marie zag helpen zwemmen".

Uses the full B + B² derivation with verb-raising categories: helpen gets ControlVR = ((S\NP)/NP)/(S\NP) which passes through an /NP slot for its raised subject (Piet). The verb cluster composes via B and B² into ((S\NP)/NP)/NP, a 3-place predicate that absorbs Marie (outermost /NP → zwemmen), Piet (inner /NP → helpen), and Jan (\NP → zag) — yielding the cross-serial binding pattern.

Equations

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

theorem Steedman2000CrossSerial.ccg_produces_crossSerial_2 : dutch_jan_piet_zag_zwemmen.binding = Phenomena.WordOrder.CrossSerial.dutch_2np_2v.binding

CCG derivation for Dutch produces cross-serial bindings.

This is the key prediction: the compositional structure of CCG naturally yields cross-serial dependencies for Dutch verb clusters.

theorem Steedman2000CrossSerial.ccg_produces_crossSerial_3 : dutch_jan_piet_marie_zag_helpen_zwemmen.binding = Phenomena.WordOrder.CrossSerial.dutch_3np_3v.binding

theorem Steedman2000CrossSerial.ccg_crossSerial_complete : dutch_jan_piet_zag_zwemmen.deriv.cat = some CCG.S ∧ dutch_jan_piet_marie_zag_helpen_zwemmen.deriv.cat = some CCG.S ∧ dutch_jan_piet_zag_zwemmen.binding = Phenomena.WordOrder.CrossSerial.dutch_2np_2v.binding ∧ dutch_jan_piet_marie_zag_helpen_zwemmen.binding = Phenomena.WordOrder.CrossSerial.dutch_3np_3v.binding

Both cross-serial derivations are well-formed (yield S) and match the data.

theorem Steedman2000CrossSerial.ccg_predicts_dutch_pattern : Phenomena.WordOrder.CrossSerial.dutch_3np_3v.binding.pattern = Features.BindingPattern.crossSerial

CCG correctly predicts the pattern type for Dutch.