Abramsky and Sadrzadeh (2014): Semantic Unification: A Sheaf Theoretic Approach to Natural Language

Abramsky and Sadrzadeh model basic discourse representation structures as a presheaf on contexts, finite vocabularies of relation symbols with finite sets of variables (DRT.presheaf), and read anaphora resolution as gluing: the local theories of a discourse's parts glue along a cover, a choice of which referents to identify, when some global theory restricts to each of them.

Proposition 1 claims that a gluing is unique when it exists. The paper's own second example refutes it: John(b) is invisible to every restriction, so it can be added to the listed gluing (isGluing_beats_insert). Gluings are unique exactly along covers jointly surjective on literals (DRT.isSeparatedFor_iff), the covers of the Grothendieck topology the paper asks for but leaves aside, for which basic DRSs form a sheaf (DRT.isSheaf_literalCoverage). The proof of Proposition 1 builds the right candidate, the least gluing (DRT.Cover.exists_isGluing_iff): the discussion example fails because the candidate does not restrict back, Example 3's merged cover because it is inconsistent. The discussion's claim that disjoint vocabularies leave consistency as the only obstruction needs injective cover maps (not_forall_exists_isGluing_of_disjoint), and Example 3's vocabularies are not disjoint: Man occurs in two parts.

The probabilistic half composes the presheaf with a distribution functor. A distribution glues a family of point masses iff it is carried by the deterministic gluings (map_restrict_eq_dirac_iff), so the several multivalued gluings of §5.1 are mixtures of deterministic ones. In the bananas discourse the corpus frequencies weight the coverings, and the image of that distribution along the gluing map ranks ripe bananas, cheeky monkeys first (gluingMeasure_le).

Main statements

• not_isSeparatedFor_beats: Proposition 1 fails on Example 2.
• not_forall_exists_isGluing_of_disjoint: disjoint vocabularies and a consistent candidate do not make a gluing.
• map_restrict_eq_dirac_iff: the multivalued gluings of point masses.
• gluingMeasure_le, gluingProbability_rounds_iff: the most likely resolution, and the printed distribution rounds the computed one except for d(t₄) = 0.205, which is 10/48 ≈ 0.208.

Implementation notes

• Var is the paper's variable names; the substrate's sheaf theorem assumes infinitely many.
• D_R is formalised for probabilities, as image measures (Measure.map), not over an arbitrary semiring.
• The corpus frequencies and the printed probabilities are read from Data.Experiments.AbramskySadrzadeh2014.

References

• [AS14]
• [KR93]
• [Gea62]

The paper's examples

inductive AbramskySadrzadeh2014.Rel : ℕ → Type

Rel n lists the n-ary relation symbols of the paper's examples.

• R : Rel 1
• S : Rel 1
• john : Rel 1
• man : Rel 1
• sleeps : Rel 1
• snores : Rel 1
• donkey : Rel 1
• grey : Rel 1
• cup : Rel 1
• plate : Rel 1
• banana : Rel 1
• monkey : Rel 1
• ripe : Rel 1
• cheeky : Rel 1
• owns : Rel 2
• beats : Rel 2
• broke : Rel 2
• putOn : Rel 3
• gave : Rel 3

def AbramskySadrzadeh2014.instDecidableEqRel.decEq {a✝ : ℕ} (x✝ x✝¹ : Rel a✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance AbramskySadrzadeh2014.instDecidableEqRel {a✝ : ℕ} : DecidableEq (Rel a✝)

Equations

• AbramskySadrzadeh2014.instDecidableEqRel = AbramskySadrzadeh2014.instDecidableEqRel.decEq

@[reducible, inline]

abbrev AbramskySadrzadeh2014.lang : FirstOrder.Language

lang is the relational language of the examples.

Equations

• AbramskySadrzadeh2014.lang = { Functions := fun (x : ℕ) => Empty, Relations := AbramskySadrzadeh2014.Rel }

inductive AbramskySadrzadeh2014.Var : Type

Var lists the variables of the paper's examples.

• x : Var
• y : Var
• z : Var
• u : Var
• v : Var
• w : Var
• a : Var
• b : Var

@[instance_reducible]

instance AbramskySadrzadeh2014.instDecidableEqVar : DecidableEq Var

Equations

• AbramskySadrzadeh2014.instDecidableEqVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AbramskySadrzadeh2014.lit {c : DRT.Context lang Var} {n : ℕ} (r : Rel n) (args : Fin n → Var) (pos : Bool := true) (hr : ⟨n, r⟩ ∈ c.vocab := by decide +kernel) (h : ∀ (i : Fin n), args i ∈ c.vars := by decide +kernel) : DRT.Literal c

lit A x̄ is the literal A(x̄), and lit A x̄ false is ¬A(x̄).

Equations

• AbramskySadrzadeh2014.lit r args pos hr h = { rel := ⟨⟨n, r⟩, hr⟩, args := fun (i : Fin (↑⟨⟨n, r⟩, hr⟩).fst) => ⟨args i, ⋯⟩, pos := pos }

def AbramskySadrzadeh2014.hom {c c' : DRT.Context lang Var} (f : Var → Var) (hf : ∀ t ∈ c.vars, f t ∈ c'.vars := by decide +kernel) (hL : c.vocab ⊆ c'.vocab := by decide +kernel) : c ⟶ c'

hom f is the context morphism acting as f on variables.

Equations

• AbramskySadrzadeh2014.hom f hf hL = { incl := hL, map := fun (t : ↥c.vars) => ⟨f ↑t, ⋯⟩ }

Example 1: John sleeps. He snores. (Examples.ex1)

@[reducible, inline]

abbrev AbramskySadrzadeh2014.snoresCtx : DRT.Context lang Var

The first example glues over this context.

Equations

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

def AbramskySadrzadeh2014.snoresCover : DRT.Cover snoresCtx (Fin 2)

The cover {x} ↦ z ↤ {y} merges he with John.

Equations

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

def AbramskySadrzadeh2014.snoresSections (i : Fin 2) : DRT.Theory (snoresCover.part i)

The local sections are s₁ = {John(x), sleeps(x)} and s₂ = {snores(y)}.

Equations

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

def AbramskySadrzadeh2014.snoresGluing : DRT.Theory snoresCtx

The gluing is s = {John(z), sleeps(z), snores(z)}.

Equations

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

theorem AbramskySadrzadeh2014.isGluing_snores : snoresCover.IsGluing (DRT.presheaf lang Var) snoresSections snoresGluing

theorem AbramskySadrzadeh2014.snores_unique {s : DRT.Theory snoresCtx} (hs : snoresCover.IsGluing (DRT.presheaf lang Var) snoresSections s) : s = snoresGluing

Every literal over {z} renames a literal of a part, so the gluing is unique.

Example 2: John beats his donkey. (Examples.ex2)

@[reducible, inline]

abbrev AbramskySadrzadeh2014.beatsCtx : DRT.Context lang Var

The second example glues over this context.

Equations

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

def AbramskySadrzadeh2014.beatsCover : DRT.Cover beatsCtx (Fin 3)

The cover maps x ↦ a, y ↦ b, and u ↦ a, v ↦ b.

Equations

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

def AbramskySadrzadeh2014.beatsSections (i : Fin 3) : DRT.Theory (beatsCover.part i)

The local sections are s₁ = {John(x)}, s₂ = {donkey(y)} and s₃ = {owns(u, v), beats(u, v)}.

Equations

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

def AbramskySadrzadeh2014.beatsGluing : DRT.Theory beatsCtx

The paper's gluing is s = {John(a), donkey(b), owns(a, b), beats(a, b)}.

Equations

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

theorem AbramskySadrzadeh2014.isGluing_beats : beatsCover.IsGluing (DRT.presheaf lang Var) beatsSections beatsGluing

def AbramskySadrzadeh2014.beatsGluing' : DRT.Theory beatsCtx

s ∪ {John(b)} is a second gluing, since John(b) renames no literal of a part and adding it changes no restriction.

Equations

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

theorem AbramskySadrzadeh2014.isGluing_beats_insert : beatsCover.IsGluing (DRT.presheaf lang Var) beatsSections beatsGluing'

theorem AbramskySadrzadeh2014.not_isSeparatedFor_beats : ¬CategoryTheory.Presieve.IsSeparatedFor (DRT.presheaf lang Var) beatsCover.presieve

Proposition 1 fails for Example 2, whose cover is not jointly surjective on literals.

Example 3: John owns a donkey. It is grey. (Examples.ex3)

@[reducible, inline]

abbrev AbramskySadrzadeh2014.greyCtx : DRT.Context lang Var

The third example glues over this context.

Equations

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

def AbramskySadrzadeh2014.greyParts : Fin 3 → DRT.Context lang Var

The third example has these covering contexts; Man occurs in the first two.

Equations

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

def AbramskySadrzadeh2014.greySections (i : Fin 3) : DRT.Theory (greyParts i)

The local sections are s₁ = {John(x), Man(x)}, s₂ = {donkey(y), ¬Man(y)} and s₃ = {grey(z)}.

Equations

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

def AbramskySadrzadeh2014.mergedCover : DRT.Cover greyCtx (Fin 3)

The cover x ↦ a, y ↦ a, z ↦ b merges John's variable with the donkey's, the cover the paper rules out as inconsistent.

Equations

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

theorem AbramskySadrzadeh2014.not_exists_isGluing_merged : ¬∃ (s : (DRT.presheaf lang Var).obj (Opposite.op greyCtx)), mergedCover.IsGluing (DRT.presheaf lang Var) greySections s

Merging x and y makes the candidate hold Man and ¬Man of one referent.

def AbramskySadrzadeh2014.greyCover : DRT.Cover greyCtx (Fin 3)

The cover x ↦ a, y ↦ b, z ↦ b merges it with the donkey.

Equations

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

def AbramskySadrzadeh2014.greyGluing : DRT.Theory greyCtx

The gluing is s = {John(a), Man(a), donkey(b), ¬Man(b), grey(b)}.

Equations

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

theorem AbramskySadrzadeh2014.isGluing_grey : greyCover.IsGluing (DRT.presheaf lang Var) greySections greyGluing

theorem AbramskySadrzadeh2014.ex3_readings : (List.lookup "it = the donkey" Examples.ex3.readings = some Judgment.acceptable ↔ ∃ (s : (DRT.presheaf lang Var).obj (Opposite.op greyCtx)), greyCover.IsGluing (DRT.presheaf lang Var) greySections s) ∧ (List.lookup "it = John" Examples.ex3.readings = some Judgment.acceptable ↔ ∃ (s : (DRT.presheaf lang Var).obj (Opposite.op greyCtx)), mergedCover.IsGluing (DRT.presheaf lang Var) greySections s)

The two covers give Example 3's readings, it as the donkey and not as John.

Example 4: John put the cup on the plate. He broke it. (Examples.ex4)

@[reducible, inline]

abbrev AbramskySadrzadeh2014.brokeCtx : DRT.Context lang Var

The fourth example glues over this context.

Equations

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

def AbramskySadrzadeh2014.brokeParts : Fin 2 → DRT.Context lang Var

The fourth example has these covering contexts.

Equations

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

def AbramskySadrzadeh2014.brokeSections (i : Fin 2) : DRT.Theory (brokeParts i)

The local sections are s₁ = {John(x), Cup(y), Plate(z), PutOn(x, y, z)} and s₂ = {Broke(u, v)}.

Equations

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

inductive AbramskySadrzadeh2014.Broken : Type

It has two plausible antecedents.

• cup : Broken
• plate : Broken

@[instance_reducible]

instance AbramskySadrzadeh2014.instDecidableEqBroken : DecidableEq Broken

Equations

• AbramskySadrzadeh2014.instDecidableEqBroken x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AbramskySadrzadeh2014.instFintypeBroken : Fintype Broken

Equations

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

def AbramskySadrzadeh2014.Broken.var : Broken → Var

Each antecedent has a referent.

Equations

• AbramskySadrzadeh2014.Broken.cup.var = AbramskySadrzadeh2014.Var.y
• AbramskySadrzadeh2014.Broken.plate.var = AbramskySadrzadeh2014.Var.z

theorem AbramskySadrzadeh2014.Broken.var_mem (b : Broken) : b.var ∈ brokeCtx.vars

def AbramskySadrzadeh2014.brokeCover (b : Broken) : DRT.Cover brokeCtx (Fin 2)

The cover extends the identity on {x, y, z} by u ↦ x and v ↦ the chosen antecedent.

Equations

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

def AbramskySadrzadeh2014.brokeGluing (b : Broken) : DRT.Theory brokeCtx

The gluing is {John(x), Cup(y), Plate(z), PutOn(x, y, z), Broke(x, ·)}, with the chosen antecedent.

Equations

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

theorem AbramskySadrzadeh2014.isGluing_broke (b : Broken) : (brokeCover b).IsGluing (DRT.presheaf lang Var) brokeSections (brokeGluing b)

Either choice of antecedent yields a gluing.

theorem AbramskySadrzadeh2014.ex4_readings : (List.lookup "it = the cup" Examples.ex4.readings = some Judgment.acceptable ↔ ∃ (s : (DRT.presheaf lang Var).obj (Opposite.op brokeCtx)), (brokeCover Broken.cup).IsGluing (DRT.presheaf lang Var) brokeSections s) ∧ (List.lookup "it = the plate" Examples.ex4.readings = some Judgment.acceptable ↔ ∃ (s : (DRT.presheaf lang Var).obj (Opposite.op brokeCtx)), (brokeCover Broken.plate).IsGluing (DRT.presheaf lang Var) brokeSections s)

Both readings of Example 4 glue.

The discussion example: overlapping vocabularies

@[reducible, inline]

abbrev AbramskySadrzadeh2014.overlapCtx : DRT.Context lang Var

The discussion example glues over this context.

Equations

• AbramskySadrzadeh2014.overlapCtx = { vocab := {⟨1, AbramskySadrzadeh2014.Rel.R⟩, ⟨1, AbramskySadrzadeh2014.Rel.S⟩}, vars := {AbramskySadrzadeh2014.Var.z, AbramskySadrzadeh2014.Var.w} }

def AbramskySadrzadeh2014.overlapCover : DRT.Cover overlapCtx (Fin 2)

The cover maps x ↦ z, u ↦ w and y ↦ z, v ↦ w; both parts carry the whole vocabulary.

Equations

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

def AbramskySadrzadeh2014.overlapSections (i : Fin 2) : DRT.Theory (overlapCover.part i)

The local sections are s₁ = {R(x), S(u)} and s₂ = {S(y), R(v)}.

Equations

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

theorem AbramskySadrzadeh2014.not_exists_isGluing_overlap : ¬∃ (s : (DRT.presheaf lang Var).obj (Opposite.op overlapCtx)), overlapCover.IsGluing (DRT.presheaf lang Var) overlapSections s

The sections do not glue, since the candidate {R(z), S(w), S(z), R(w)} restricts along the first map to {R(x), S(x), R(u), S(u)} ≠ s₁.

def AbramskySadrzadeh2014.collapseCover : DRT.Cover { vocab := {⟨1, Rel.R⟩}, vars := {Var.z} } (Fin 1)

The one-part cover {x, u} ↦ {z} identifies two referents of one part.

Equations

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

def AbramskySadrzadeh2014.collapseSections (i : Fin 1) : DRT.Theory (collapseCover.part i)

The local section is s₁ = {R(x)}.

Equations

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

theorem AbramskySadrzadeh2014.not_forall_exists_isGluing_of_disjoint : ¬∀ (ι : Type) [inst : Fintype ι] (c : DRT.Context lang Var) (C : DRT.Cover c ι) (x : (i : ι) → DRT.Theory (C.part i)), (Pairwise fun (i j : ι) => Disjoint (C.part i).vocab (C.part j).vocab) → DRT.Literal.Consistent (C.pushforward x) → ∃ (s : (DRT.presheaf lang Var).obj (Opposite.op c)), C.IsGluing (DRT.presheaf lang Var) x s

Pairwise disjoint vocabularies and a consistent candidate do not make a gluing, against the discussion of Proposition 1: the candidate {R(z)} of the one-part cover {x, u} ↦ {z} restricts to {R(x), R(u)}. Injective cover maps suffice (DRT.Cover.isGluing_glue).

Multivalued gluing

@[instance_reducible]

instance AbramskySadrzadeh2014.instMeasurableSpaceTheory_studies {L : FirstOrder.Language} {V : Type u_1} (c : DRT.Context L V) : MeasurableSpace (DRT.Theory c)

Equations

• AbramskySadrzadeh2014.instMeasurableSpaceTheory_studies c = ⊤

instance AbramskySadrzadeh2014.instDiscreteMeasurableSpaceTheory_studies {L : FirstOrder.Language} {V : Type u_1} (c : DRT.Context L V) : DiscreteMeasurableSpace (DRT.Theory c)

theorem AbramskySadrzadeh2014.map_restrict_eq_dirac_iff {L : FirstOrder.Language} {V : Type u_1} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] {c : DRT.Context L V} {ι : Type u_2} {C : DRT.Cover c ι} {x : (i : ι) → DRT.Theory (C.part i)} [Countable ι] (d : MeasureTheory.Measure (DRT.Theory c)) [MeasureTheory.IsProbabilityMeasure d] : (∀ (i : ι), MeasureTheory.Measure.map (DRT.Theory.restrict (C.map i)) d = MeasureTheory.Measure.dirac (x i)) ↔ d {s : DRT.Theory c | ¬C.IsGluing (DRT.presheaf L V) x s} = 0

A probability measure on global theories glues the point masses δ_{sᵢ} in D ∘ F iff it is carried by the gluings of the sᵢ.

Probabilistic anaphora: *John gave the bananas to the monkeys. They were ripe. They were

cheeky.* (Examples.bananas)

@[reducible, inline]

abbrev AbramskySadrzadeh2014.ripeCtx : DRT.Context lang Var

The bananas discourse glues over this context.

Equations

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

def AbramskySadrzadeh2014.ripeParts : Fin 3 → DRT.Context lang Var

The bananas discourse has these covering contexts.

Equations

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

def AbramskySadrzadeh2014.ripeSections (i : Fin 3) : DRT.Theory (ripeParts i)

The local sections are s₁ = {John(x), Banana(y), Monkey(z), Gave(x, y, z)}, s₂ = {Ripe(u)} and s₃ = {Cheeky(v)}.

Equations

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

def AbramskySadrzadeh2014.Noun.var : Noun → Var

Each antecedent has a referent.

Equations

• AbramskySadrzadeh2014.Noun.banana.var = AbramskySadrzadeh2014.Var.y
• AbramskySadrzadeh2014.Noun.monkey.var = AbramskySadrzadeh2014.Var.z

theorem AbramskySadrzadeh2014.Noun.var_mem (a : Noun) : a.var ∈ ripeCtx.vars

def AbramskySadrzadeh2014.ripeCover (c : Noun × Noun) : DRT.Cover ripeCtx (Fin 3)

The covering c extends the identity on {x, y, z} by u ↦ c.1 and v ↦ c.2.

Equations

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

def AbramskySadrzadeh2014.ripeGluing (c : Noun × Noun) : DRT.Theory ripeCtx

The covering c induces the candidate global section t_c.

Equations

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

theorem AbramskySadrzadeh2014.isGluing_ripe (c : Noun × Noun) : (ripeCover c).IsGluing (DRT.presheaf lang Var) ripeSections (ripeGluing c)

theorem AbramskySadrzadeh2014.ripeGluing_injective : Function.Injective ripeGluing

def AbramskySadrzadeh2014.score (c : Noun × Noun) : ℕ

The score of a covering sums the corpus frequencies of its two mergings.

Equations

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

@[instance_reducible]

instance AbramskySadrzadeh2014.instMeasurableSpaceProdNoun_studies : MeasurableSpace (Noun × Noun)

Equations

• AbramskySadrzadeh2014.instMeasurableSpaceProdNoun_studies = ⊤

noncomputable def AbramskySadrzadeh2014.coveringMeasure : MeasureTheory.Measure (Noun × Noun)

The distribution over coverings weights each by its score, normalised.

Equations

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

noncomputable def AbramskySadrzadeh2014.gluingMeasure : MeasureTheory.Measure (DRT.Theory ripeCtx)

The paper's d ∈ D_R F(L, X) is the image of the covering distribution along c ↦ t_c.

Equations

• AbramskySadrzadeh2014.gluingMeasure = MeasureTheory.Measure.map AbramskySadrzadeh2014.ripeGluing AbramskySadrzadeh2014.coveringMeasure

theorem AbramskySadrzadeh2014.gluingMeasure_apply (c : Noun × Noun) : gluingMeasure {ripeGluing c} = ↑(score c) / 48

theorem AbramskySadrzadeh2014.gluingMeasure_le : gluingMeasure {ripeGluing (Noun.banana, Noun.monkey)} = 1 / 2 ∧ ∀ (t : DRT.Theory ripeCtx), gluingMeasure {t} ≤ gluingMeasure {ripeGluing (Noun.banana, Noun.monkey)}

Ripe bananas, cheeky monkeys (t₂) is the most likely resolution, with probability 1/2.

theorem AbramskySadrzadeh2014.gluingProbability_rounds_iff (c : Noun × Noun) : (gluingProbability c.1 c.2).probability.Rounds (score c) 48 ↔ c ≠ (Noun.monkey, Noun.monkey)

The printed d(t_c) is score c / 48 rounded, except d(t₄) = 0.205 for 10/48.