CCG Syntax-Semantics Interface

Syntactic categories directly encode semantic types and the combinatory rules correspond to function application and composition ([Ste00a]), so a derivation's meaning is read off compositionally from its structure.

Main definitions

• catToTy — maps CCG categories to semantic types
• SemLexEntry, SemLexicon — lexical entries with semantics
• DerivStep.interp — computes a meaning from a derivation compositionally: application is function application, composition is the B combinator, type-raising is the T combinator, coordination is generalized conjunction ([PR83])

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

Type correspondence

def CCG.catToTy : Cat → Intensional.Ty

Map CCG categories to semantic types

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 y) = (CCG.catToTy y ⇒ CCG.catToTy x_1)
• CCG.catToTy (x_1.lslash y) = (CCG.catToTy y ⇒ CCG.catToTy x_1)

structure CCG.SemLexEntry (E W : Type) : Type

A CCG lexical entry with semantics

• form : String
• cat : Cat
• sem : Intensional.Denot E W (catToTy self.cat)

Type preservation

CCG combinatory rules preserve semantic well-typedness: if the syntactic combination succeeds, the semantic combination is well-typed.

theorem CCG.forward_app_type_preservation (x y : Cat) : catToTy (x.rslash 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) : catToTy (x.lslash 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

Derivation interpretation

structure CCG.Interp (E W : Type) : Type

A semantic interpretation: category paired with its meaning

• cat : Cat
• meaning : Intensional.Denot E W (catToTy self.cat)

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

Semantic lexicon: maps words to interpretations

Equations

• CCG.SemLexicon E W = (String → CCG.Cat → Option (CCG.Interp E W))

def CCG.DerivStep.interp {E W : Type} (d : DerivStep) (lex : SemLexicon E W) : Option (Interp E W)

Interpret a CCG derivation, computing its meaning from the lexicon.

Every combinatory rule corresponds to a semantic operation: application is function application, composition is the B combinator, type-raising is the T combinator, and coordination is generalized conjunction (restricted to conjoinable types). Returns none if the derivation is ill-formed or uses unknown words.

Equations

• One or more equations did not get rendered due to their size.
• (CCG.DerivStep.lex entry).interp lex = lex entry.form entry.cat
• (d_2.ftr t).interp lex = do let __discr ← d_2.interp lex match __discr with | { cat := x, meaning := m } => some { cat := CCG.forwardTypeRaise x t, meaning := Combinator.T m }
• (d_2.btr t).interp lex = do let __discr ← d_2.interp lex match __discr with | { cat := x, meaning := m } => some { cat := CCG.backwardTypeRaise x t, meaning := Combinator.T m }

def CCG.getMeaning {E W : Type} (result : Option (Interp E W)) : Option Prop

Extract a sentence meaning (category S) from an interpretation result.

Equations

• CCG.getMeaning (some { cat := CCG.Cat.atom CCG.Atom.S, meaning := m }) = some m
• CCG.getMeaning result = none

def CCG.getPredicateMeaning {E W : Type} (result : Option (Interp E W)) : Option (E → Prop)

Extract a predicate meaning (category S/NP) from an interpretation result.

Equations

• CCG.getPredicateMeaning (some { cat := (CCG.Cat.atom CCG.Atom.S).rslash (CCG.Cat.atom CCG.Atom.NP), meaning := m }) = some m
• CCG.getPredicateMeaning result = none