The CCG syntax-semantics interface

A typing of the atoms extends to every category, sending X/Y and X\Y to the function type from the type of Y to that of X and ignoring slash modalities, which control combinatory potential rather than meaning. Since a Derivation is indexed by its category, its interpretation needs no run-time category checks: a rule instance X/Y Yβ ⇒ Xβ composes its daughters' meanings beneath the arguments β, Curry's combinator Bⁿ for n the length of β, so application is function application and first-order composition is Steedman's B. Type-raising and coordination are lexical, so their meanings (the Montague lift, generalized conjunction) come from the lexicon. A lexicon returns meanings at the queried category, so the interface is sound by typing rather than by a theorem.

Main definitions

• CCG.Cat.toTy: the semantic type of a category under a typing of its atoms.
• CCG.SemLexicon: a semantic lexicon, giving a word an optional meaning at each category.
• CCG.composeUnder: composition beneath an argument sequence, Curry's Bⁿ.
• CCG.Derivation.interp: the meaning of a derivation, none only when a word is missing from the lexicon.

Main statements

• CCG.Derivation.interp_fcomp_assoc, CCG.Derivation.interp_fapp_fcomp and their backward mirrors: in every rule system, reassociating a composition-application chain does not change its interpretation, the source of CCG's spurious ambiguity.

References

• [Ste00a]
• [Ste19]
• [Kar89]
• [PS87a]

Type correspondence

def CCG.Cat.toTy {α : Type u_2} (τ : α → Montague.Ty) : Cat α → Montague.Ty

c.toTy τ is the semantic type of the category c when each atom a has type τ a.

Equations

• CCG.Cat.toTy τ (CCG.Cat.atom a) = τ a
• CCG.Cat.toTy τ (x_1.rslash a y) = (CCG.Cat.toTy τ y ⇒ CCG.Cat.toTy τ x_1)
• CCG.Cat.toTy τ (x_1.lslash a y) = (CCG.Cat.toTy τ y ⇒ CCG.Cat.toTy τ x_1)

@[simp]

theorem CCG.Cat.toTy_forwardTypeRaise {α : Type u_2} (τ : α → Montague.Ty) (x t : Cat α) : toTy τ (x.forwardTypeRaise t) = ((toTy τ x ⇒ toTy τ t) ⇒ toTy τ t)

A forward type-raised category T/(T\X) denotes a function over functions from the type of X.

@[simp]

theorem CCG.Cat.toTy_backwardTypeRaise {α : Type u_2} (τ : α → Montague.Ty) (x t : Cat α) : toTy τ (x.backwardTypeRaise t) = ((toTy τ x ⇒ toTy τ t) ⇒ toTy τ t)

A backward type-raised category T\(T/X) denotes the same type as its forward counterpart.

Derivation interpretation

def CCG.SemLexicon (T : Type u_1) {α : Type u_2} (τ : α → Montague.Ty) (E W : Type) : Type (max (max u_1 u_2) 0)

A semantic lexicon gives a word an optional meaning at each category, of that category's type under the atom typing τ. Type-raised and coordinating entries carry the meanings of type-raising and coordination.

Equations

• CCG.SemLexicon T τ E W = (T → (c : CCG.Cat α) → Option (Montague.Ty.Domain E W (CCG.Cat.toTy τ c)))

def CCG.composeUnder {α : Type u_2} (τ : α → Montague.Ty) {E W : Type} (β : List (Cat.Arg α)) {x y : Cat α} : Montague.Ty.Domain E W (Cat.toTy τ y ⇒ Cat.toTy τ x) → Montague.Ty.Domain E W (Cat.toTy τ (y.pushArgs β)) → Montague.Ty.Domain E W (Cat.toTy τ (x.pushArgs β))

composeUnder τ β f g composes f with g beneath the arguments β, Curry's combinator Bⁿ for n the length of β: it takes the arguments of g, outermost first, and applies f to the result.

Equations

• CCG.composeUnder τ [] x✝¹ x✝ = x✝¹ x✝
• CCG.composeUnder τ ({ side := Edge.right, modality := m, cat := z } :: β) x✝¹ x✝ = CCG.composeUnder τ β (fun (x : Montague.Ty.Domain E W (CCG.Cat.toTy τ (x✝².rslash m z))) => x✝¹ ∘ x) x✝
• CCG.composeUnder τ ({ side := Edge.left, modality := m, cat := z } :: β) x✝¹ x✝ = CCG.composeUnder τ β (fun (x : Montague.Ty.Domain E W (CCG.Cat.toTy τ (x✝².lslash m z))) => x✝¹ ∘ x) x✝

def CCG.Rule.sem {α : Type u_2} (τ : α → Montague.Ty) {E W : Type} {R : RuleSystem α} {l r c : Cat α} : Rule R l r c → Montague.Ty.Domain E W (Cat.toTy τ l) → Montague.Ty.Domain E W (Cat.toTy τ r) → Montague.Ty.Domain E W (Cat.toTy τ c)

r.sem τ is the meaning of the rule r as an operation on its daughters' meanings, the primary composed with the secondary beneath the arguments the rule passes on.

Equations

• CCG.Rule.sem τ (CCG.Rule.forward β h) f g = CCG.composeUnder τ β f g
• CCG.Rule.sem τ (CCG.Rule.backward β h) g f = CCG.composeUnder τ β f g

def CCG.Derivation.interp {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {τ : α → Montague.Ty} {E W : Type} (lex : SemLexicon T τ E W) {c : Cat α} : Derivation T R c → Option (Montague.Ty.Domain E W (Cat.toTy τ c))

d.interp lex is the meaning of the derivation d. A leaf takes its meaning from lex and a rule node combines its daughters' meanings by Rule.sem, so the result is none only when a word is missing from the lexicon.

Equations

• One or more equations did not get rendered due to their size.
• CCG.Derivation.interp lex (CCG.Derivation.lex f x✝) = lex f x✝

Spurious ambiguity

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

theorem CCG.Derivation.interp_fcomp_assoc {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {τ : α → Montague.Ty} {E W : Type} (lex : SemLexicon T τ E W) {x y z w : Cat α} {m n p : Modality} (d₁ : Derivation T R (x.rslash m y)) (d₂ : Derivation T R (y.rslash n z)) (d₃ : Derivation T R (z.rslash p w)) (h₁ : R x { side := Edge.right, modality := m, cat := y } [{ side := Edge.right, modality := n, cat := z }]) (h₂ : R x { side := Edge.right, modality := n, cat := z } [{ side := Edge.right, modality := p, cat := w }]) (h₃ : R y { side := Edge.right, modality := n, cat := z } [{ side := Edge.right, modality := p, cat := w }]) (h₄ : R x { side := Edge.right, modality := m, cat := y } [{ side := Edge.right, modality := p, cat := w }]) : interp lex ((d₁.fcomp d₂ h₁).fcomp d₃ h₂) = interp lex (d₁.fcomp (d₂.fcomp d₃ h₃) h₄)

Reassociating a forward-composition chain preserves its interpretation, since composition is associative.

theorem CCG.Derivation.interp_fapp_fcomp {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {τ : α → Montague.Ty} {E W : Type} (lex : SemLexicon T τ E W) {x y z : Cat α} {m n : Modality} (d₁ : Derivation T R (x.rslash m y)) (d₂ : Derivation T R (y.rslash n z)) (d₃ : Derivation T R z) (h₁ : R x { side := Edge.right, modality := m, cat := y } [{ side := Edge.right, modality := n, cat := z }]) (h₂ : R x { side := Edge.right, modality := n, cat := z } []) (h₃ : R y { side := Edge.right, modality := n, cat := z } []) (h₄ : R x { side := Edge.right, modality := m, cat := y } []) : interp lex ((d₁.fcomp d₂ h₁).fapp d₃ h₂) = interp lex (d₁.fapp (d₂.fapp d₃ h₃) h₄)

Composing and then applying has the interpretation of applying twice, since (f ∘ g) x = f (g x).

theorem CCG.Derivation.interp_bcomp_assoc {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {τ : α → Montague.Ty} {E W : Type} (lex : SemLexicon T τ E W) {x y z w : Cat α} {m n p : Modality} (d₁ : Derivation T R (y.lslash p z)) (d₂ : Derivation T R (x.lslash n y)) (d₃ : Derivation T R (w.lslash m x)) (h₁ : R x { side := Edge.left, modality := n, cat := y } [{ side := Edge.left, modality := p, cat := z }]) (h₂ : R w { side := Edge.left, modality := m, cat := x } [{ side := Edge.left, modality := p, cat := z }]) (h₃ : R w { side := Edge.left, modality := m, cat := x } [{ side := Edge.left, modality := n, cat := y }]) (h₄ : R w { side := Edge.left, modality := n, cat := y } [{ side := Edge.left, modality := p, cat := z }]) : interp lex ((d₁.bcomp d₂ h₁).bcomp d₃ h₂) = interp lex (d₁.bcomp (d₂.bcomp d₃ h₃) h₄)

Reassociating a backward-composition chain preserves its interpretation.

theorem CCG.Derivation.interp_bapp_bcomp {T : Type u_1} {α : Type u_2} {R : RuleSystem α} {τ : α → Montague.Ty} {E W : Type} (lex : SemLexicon T τ E W) {x y w : Cat α} {m n : Modality} (d₁ : Derivation T R y) (d₂ : Derivation T R (x.lslash n y)) (d₃ : Derivation T R (w.lslash m x)) (h₁ : R x { side := Edge.left, modality := n, cat := y } []) (h₂ : R w { side := Edge.left, modality := m, cat := x } []) (h₃ : R w { side := Edge.left, modality := m, cat := x } [{ side := Edge.left, modality := n, cat := y }]) (h₄ : R w { side := Edge.left, modality := n, cat := y } []) : interp lex ((d₁.bapp d₂ h₁).bapp d₃ h₂) = interp lex (d₁.bapp (d₂.bcomp d₃ h₃) h₄)

Applying twice has the interpretation of backward-composing first and then applying.