Semantic Equivalence and Spurious Ambiguity

CCG derivations fall into equivalence classes: multiple derivations yield identical interpretations due to the associativity of functional composition. This is sometimes called "spurious ambiguity" — but it's not really ambiguity, since all derivations in an equivalence class have the same meaning.

Key concepts

1. Semantic equivalence — two derivations are equivalent iff they have the same category and the same meaning.
2. Source of equivalence — the B combinator is associative (B (B f g) h = B f (B g h)), so (f ∘ g) ∘ h = f ∘ (g ∘ h) in the semantics.
3. Equivalence classes — for a string of n words there are Catalan(n-1) binary bracketings, all yielding the same meaning if built purely from composition.
4. Processing — a parser need only find one derivation per equivalence class.

structure CCG.Equivalence.DerivEquiv (E W : Type) : Type

Two derivations are semantically equivalent iff they span the same substring, have the same category, and have the same meaning.

This defines equivalence for "spurious ambiguity" analysis.

• cat : Cat

  First derivation's category

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

  First derivation's meaning

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

  Second derivation's meaning

• meanings_eq : self.meaning₁ = self.meaning₂

  The meanings are equal

def CCG.Equivalence.semanticallyEquivalent {E W : Type} (cm₁ cm₂ : (c : Cat) × Intensional.Denot E W (catToTy c)) : Prop

Semantic equivalence for category-meaning pairs.

Equations

• CCG.Equivalence.semanticallyEquivalent cm₁ cm₂ = ∃ (h : cm₁.fst = cm₂.fst), h ▸ cm₁.snd = cm₂.snd

theorem CCG.Equivalence.sem_equiv_refl {E W : Type} (cm : (c : Cat) × Intensional.Denot E W (catToTy c)) : semanticallyEquivalent cm cm

Semantic equivalence is reflexive.

theorem CCG.Equivalence.sem_equiv_symm {E W : Type} (cm₁ cm₂ : (c : Cat) × Intensional.Denot E W (catToTy c)) : semanticallyEquivalent cm₁ cm₂ → semanticallyEquivalent cm₂ cm₁

Semantic equivalence is symmetric.

theorem CCG.Equivalence.sem_equiv_trans {E W : Type} (cm₁ cm₂ cm₃ : (c : Cat) × Intensional.Denot E W (catToTy c)) : semanticallyEquivalent cm₁ cm₂ → semanticallyEquivalent cm₂ cm₃ → semanticallyEquivalent cm₁ cm₃

Semantic equivalence is transitive.

theorem CCG.Equivalence.B_assoc {α β γ δ : Type} (f : γ → δ) (g : β → γ) (h : α → β) : Combinator.B (Combinator.B f g) h = Combinator.B f (Combinator.B g h)

B (composition) is associative: (f ∘ g) ∘ h = f ∘ (g ∘ h)

theorem CCG.Equivalence.B_assoc_apply {α β γ δ : Type} (f : γ → δ) (g : β → γ) (h : α → β) (x : α) : Combinator.B (Combinator.B f g) h x = Combinator.B f (Combinator.B g h) x

Associativity stated pointwise.

theorem CCG.Equivalence.composition_order_irrelevant {α β γ δ : Type} (f : γ → δ) (g : β → γ) (h : α → β) (x : α) : f (g (h x)) = Combinator.B f (Combinator.B g h) x

Consequence: Two ways of composing three functions yield the same result.

This is why "Harry thinks that Anna married" can be derived by:

1. (Harry ∘ thinks) ∘ (that ∘ (Anna ∘ married))
2. Harry ∘ (thinks ∘ that) ∘ (Anna ∘ married)
3. Harry ∘ (thinks ∘ (that ∘ Anna)) ∘ married ... etc.

All yield the same predicate-argument structure.

structure CCG.Equivalence.ChartEntry (E W : Type) : Type

A chart entry: category + meaning for a span.

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

def CCG.Equivalence.chartEntriesMatch {E W : Type} (e₁ e₂ : ChartEntry E W) : Prop

Two chart entries match if they have the same span, category, and meaning.

Equations

• CCG.Equivalence.chartEntriesMatch e₁ e₂ = (e₁.leftPos = e₂.leftPos ∧ e₁.rightPos = e₂.rightPos ∧ ∃ (h : e₁.cat = e₂.cat), h ▸ e₁.meaning = e₂.meaning)

def CCG.Equivalence.chartEntriesSameCat {E W : Type} (e₁ e₂ : ChartEntry E W) : Bool

The matching relation is decidable for categories (not meanings in general).

Equations

• CCG.Equivalence.chartEntriesSameCat e₁ e₂ = (e₁.leftPos == e₂.leftPos && e₁.rightPos == e₂.rightPos && e₁.cat == e₂.cat)

structure CCG.Equivalence.EquivalenceClass (E W : Type) : Type

An equivalence class of derivations: all have the same meaning.

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

def CCG.Equivalence.reallyAmbiguous {E W : Type} (classes : List (EquivalenceClass E W)) : Prop

Real ambiguity: multiple equivalence classes for the same string.

Equations

• CCG.Equivalence.reallyAmbiguous classes = (classes.length > 1)

def CCG.Equivalence.spuriouslyAmbiguous {E W : Type} (derivCount : ℕ) (classes : List (EquivalenceClass E W)) : Prop

Spuriously ambiguous: multiple derivations but only one equivalence class.

Equations

• CCG.Equivalence.spuriouslyAmbiguous derivCount classes = (derivCount > 1 ∧ classes.length = 1)