CCG Syntax-Semantics Interface

This file defines the compositional interpretation of CCG derivations. Categories encode semantic types (catToTy, which ignores slash modalities — they control combinatory potential, not meaning), and because Derivation is intrinsically typed, Derivation.interp needs no run-time category checks and no casts: application is function application and every composition rule is a B-combinator composition of the daughters' meanings ([Ste19]). Type-raising and coordination are lexical, so their semantic action (T, generalized conjunction) enters through the lexicon. A lexicon is well-typed by construction — it returns meanings at the queried category — so soundness of the interface is a typing fact rather than a theorem.

Main definitions

• catToTy: maps CCG categories to semantic types.
• SemLexicon: a semantic lexicon — for each word and category, optionally a meaning at that category.
• Derivation.interp: the meaning of a derivation of category c, at type catToTy c; none only when a word is missing from the lexicon.

Main statements

• Derivation.interp_fcomp_assoc, Derivation.interp_fapp_fcomp (and backward mirrors): spurious ambiguity — reassociating a composition-application chain cannot change a constituent's interpretation ([Ste00a]; the matching-entry tests of [Kar89] and [PS87a] exploit exactly this invariance).

Worked toy-fragment derivations and the non-constituent-coordination semantics theorems live in Studies/Steedman2000.lean.

Type correspondence

def CCG.catToTy : Cat Atom → Intensional.Ty

Map CCG categories to semantic types. Slash modalities are ignored: they control combinatory potential, not meaning.

Equations

• CCG.catToTy (CCG.Cat.atom CCG.Atom.S) = Intensional.Ty.t
• CCG.catToTy (CCG.Cat.atom CCG.Atom.NP) = Intensional.Ty.e
• CCG.catToTy (CCG.Cat.atom CCG.Atom.N) = (Intensional.Ty.e ⇒ Intensional.Ty.t)
• CCG.catToTy (CCG.Cat.atom CCG.Atom.PP) = (Intensional.Ty.e ⇒ Intensional.Ty.t)
• CCG.catToTy (x_1.rslash a y) = (CCG.catToTy y ⇒ CCG.catToTy x_1)
• CCG.catToTy (x_1.lslash a y) = (CCG.catToTy y ⇒ CCG.catToTy x_1)

theorem CCG.forward_app_type_preservation (x y : Cat Atom) (m : Modality) : catToTy (x.rslash m y) = (catToTy y ⇒ catToTy x)

Forward application preserves semantic typing: if X/Y combines with Y to give X, then (σ→τ) applied to σ gives τ.

theorem CCG.backward_app_type_preservation (x y : Cat Atom) (m : Modality) : catToTy (x.lslash m y) = (catToTy y ⇒ catToTy x)

Backward application preserves semantic typing: if Y combines with X\Y to give X, then (σ→τ) applied to σ gives τ.

theorem CCG.tv_type_is_relation : catToTy TV = (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)

Type correspondence for transitive verbs

theorem CCG.iv_type_is_property : catToTy IV = (Intensional.Ty.e ⇒ Intensional.Ty.t)

Type correspondence for intransitive verbs

theorem CCG.forward_type_raise_type (x t : Cat Atom) : catToTy (x.forwardTypeRaise t) = ((catToTy x ⇒ catToTy t) ⇒ catToTy t)

Type correspondence for forward type-raising: T/(T\X) denotes a function over X-seeking functions.

theorem CCG.backward_type_raise_type (x t : Cat Atom) : catToTy (x.backwardTypeRaise t) = ((catToTy x ⇒ catToTy t) ⇒ catToTy t)

Type correspondence for backward type-raising, identical to the forward case.

Derivation interpretation

def CCG.SemLexicon (E W : Type) : Type

Semantic lexicon: for each word and queried category, optionally a meaning at that category — well-typed by construction. Raised and coordinating entries carry their semantic action here (T, generalized conjunction), per the morpholexical treatment of [Ste19].

Equations

• CCG.SemLexicon E W = (String → (c : CCG.Cat CCG.Atom) → Option (Intensional.Denot E W (CCG.catToTy c)))

def CCG.Rule.sem {E W : Type} {l r c : Cat Atom} : Rule Atom l r c → Intensional.Denot E W (catToTy l) → Intensional.Denot E W (catToTy r) → Intensional.Denot E W (catToTy c)

The semantic action of a rule — the "rule-to-rule relation" of [Ste19]: application applies, every composition rule is a B-combinator composition of the daughters' meanings (second-order rules compose under one argument).

Equations

• CCG.Rule.fapp.sem f x✝ = f x✝
• CCG.Rule.bapp.sem x✝ f = f x✝
• (CCG.Rule.fcomp h).sem f g = Combinator.B f g
• (CCG.Rule.bcomp h).sem g f = Combinator.B f g
• (CCG.Rule.fcompx h).sem f g = Combinator.B f g
• (CCG.Rule.bcompx h).sem g f = Combinator.B f g
• (CCG.Rule.fcomp2 h).sem f g = fun (w : Intensional.Denot E W (CCG.catToTy w)) (z : Intensional.Denot E W (CCG.catToTy z)) => f (g w z)
• (CCG.Rule.bcomp2 h).sem g f = fun (w : Intensional.Denot E W (CCG.catToTy w)) (z : Intensional.Denot E W (CCG.catToTy z)) => f (g w z)
• (CCG.Rule.fcompx2 h).sem f g = fun (w : Intensional.Denot E W (CCG.catToTy w)) (z : Intensional.Denot E W (CCG.catToTy z)) => f (g w z)
• (CCG.Rule.bcompx2 h).sem g f = fun (w : Intensional.Denot E W (CCG.catToTy w)) (z : Intensional.Denot E W (CCG.catToTy z)) => f (g w z)

def CCG.Derivation.interp {E W : Type} (lex : SemLexicon E W) {c : Cat Atom} : Derivation Atom c → Option (Intensional.Denot E W (catToTy c))

Interpret a derivation compositionally: leaves consult the lexicon and each rule node acts by its Rule.sem. The category bookkeeping is carried by Derivation's index, so no run-time category checks (and no casts) are needed; the result is none only when a word is missing from the lexicon.

Equations

• CCG.Derivation.interp lex (CCG.Derivation.lex f x✝) = lex f x✝
• CCG.Derivation.interp lex (CCG.Derivation.node ru d₁ d₂) = do let __do_lift ← CCG.Derivation.interp lex d₁ let __do_lift_1 ← CCG.Derivation.interp lex d₂ some (ru.sem __do_lift __do_lift_1)

Spurious ambiguity

Composition is semantically associative, so left- and right-branching derivations of the same composition-application chain receive the same interpretation — with no assumption on the lexicon. This is the local source of CCG's "spurious ambiguity" ([Ste00a]; the matching-entry tests of [Kar89] and [PS87a] exploit exactly this invariance): a chart parser may keep one derivation per equivalence class, because reassociating fcomp/fapp (or bcomp/bapp) nodes cannot change what a constituent means.

theorem CCG.Derivation.interp_fcomp_assoc {E W : Type} (lex : SemLexicon E W) {x y z w : Cat Atom} {m n p : Modality} (hm : m ≤ Modality.diamond) (hn : n ≤ Modality.diamond) (d₁ : Derivation Atom (x.rslash m y)) (d₂ : Derivation Atom (y.rslash n z)) (d₃ : Derivation Atom (z.rslash p w)) : interp lex (fcomp hn (fcomp hm d₁ d₂) d₃) = interp lex (fcomp hm d₁ (fcomp hn d₂ d₃))

Reassociating a forward-composition chain preserves interpretation: B is semantically associative.

theorem CCG.Derivation.interp_fapp_fcomp {E W : Type} (lex : SemLexicon E W) {x y z : Cat Atom} {m n : Modality} (hm : m ≤ Modality.diamond) (d₁ : Derivation Atom (x.rslash m y)) (d₂ : Derivation Atom (y.rslash n z)) (d₃ : Derivation Atom z) : interp lex ((fcomp hm d₁ d₂).fapp d₃) = interp lex (d₁.fapp (d₂.fapp d₃))

Composing before applying is the same as applying twice: B f g x = f (g x), lifted to derivations.

theorem CCG.Derivation.interp_bcomp_assoc {E W : Type} (lex : SemLexicon E W) {x y z w : Cat Atom} {m n p : Modality} (hm : m ≤ Modality.diamond) (hn : n ≤ Modality.diamond) (d₁ : Derivation Atom (y.lslash p z)) (d₂ : Derivation Atom (x.lslash n y)) (d₃ : Derivation Atom (w.lslash m x)) : interp lex (bcomp hm (bcomp hn d₁ d₂) d₃) = interp lex (bcomp hn d₁ (bcomp hm d₂ d₃))

Reassociating a backward-composition chain preserves interpretation — the mirror of interp_fcomp_assoc.

theorem CCG.Derivation.interp_bapp_bcomp {E W : Type} (lex : SemLexicon E W) {x y w : Cat Atom} {m n : Modality} (hm : m ≤ Modality.diamond) (d₁ : Derivation Atom y) (d₂ : Derivation Atom (x.lslash n y)) (d₃ : Derivation Atom (w.lslash m x)) : interp lex ((d₁.bapp d₂).bapp d₃) = interp lex (d₁.bapp (bcomp hm d₂ d₃))

Applying twice is the same as backward-composing first — the mirror of interp_fapp_fcomp.