Semantic unification as sheaf gluing

Abramsky and Sadrzadeh model basic Discourse Representation Structures as a presheaf on a category of contexts — a finite vocabulary of relation symbols with a finite set of variables — and read anaphora resolution as sheaf gluing: the local theories of the parts of a discourse glue along a cover (the choice of which discourse referents to identify) exactly when some global theory restricts to each of them. The presheaf is DRT.presheaf, covers and gluing are DRT.Cover and DRT.Cover.IsGluing, and the paper's reading of a cover as DRT's merge followed by unification of referents is DRT.Cover.coe_conditions_toDRS_glue.

The paper's Proposition 1 says gluings are unique when they exist, its proof building the candidate DRT.Cover.pushforward. Uniqueness holds when every literal of the glued context factors through a cover map (DRT.Cover.IsGluing.unique), as in the first example (snores_unique), but fails on the paper's own second example, where John(b) is invisible to every restriction and may be added to the listed gluing (isGluing_beats_insert, not_isSeparatedFor_beats). What is unique is the least gluing, which glues whenever the vocabularies are pairwise disjoint and the cover maps injective (DRT.Cover.isGluing_glue); the two obstructions otherwise both occur in the paper: overlapping vocabularies in the discussion example (not_exists_isGluing_overlap) and inconsistency when it is merged with John (not_exists_isGluing_merged). The four linguistic examples are decided by kernel computation (isGluing_snores, isGluing_beats, isGluing_grey, isGluing_broke).

The probabilistic half composes the presheaf with the distribution functor distribution R of a semiring R, whose gluing is DRT.Cover.IsGluing (DRT.presheaf L V ⋙ distribution R). The bananas discourse instantiates the paper's ranking of covers by corpus frequencies: pushing the covering distribution forward along the gluing map (gluingDistribution) makes ripe bananas, cheeky monkeys the most likely resolution (gluingDistribution_ripe).

References

• [AS14]
• [KR93]
• [geach-1962]

The distribution functor

def AbramskySadrzadeh2014.Distribution (R : Type r) [AddCommMonoid R] [One R] (S : Type u) : Type (max u r)

Finitely supported R-weightings of S summing to 1 — the paper's D_R(S).

Equations

• AbramskySadrzadeh2014.Distribution R S = { d : S →₀ R // (d.sum fun (x : S) (m : R) => m) = 1 }

noncomputable def AbramskySadrzadeh2014.Distribution.map {R : Type r} [AddCommMonoid R] [One R] {S T : Type u} (f : S → T) (d : Distribution R S) : Distribution R T

The image distribution along a map.

Equations

• AbramskySadrzadeh2014.Distribution.map f d = ⟨Finsupp.mapDomain f ↑d, ⋯⟩

@[simp]

theorem AbramskySadrzadeh2014.Distribution.map_id {R : Type r} [AddCommMonoid R] [One R] {S : Type u} (d : Distribution R S) : map id d = d

theorem AbramskySadrzadeh2014.Distribution.map_comp {R : Type r} [AddCommMonoid R] [One R] {S T U : Type u} (f : S → T) (g : T → U) (d : Distribution R S) : map (g ∘ f) d = map g (map f d)

noncomputable def AbramskySadrzadeh2014.Distribution.ofWeights {ι : Type u} [Fintype ι] (w : ι → ℕ) (h : ∑ i : ι, w i ≠ 0) : Distribution ℚ ι

The distribution proportional to a weighting with nonzero total.

Equations

• AbramskySadrzadeh2014.Distribution.ofWeights w h = ⟨Finsupp.equivFunOnFinite.symm fun (i : ι) => ↑(w i) / ↑(∑ i : ι, w i), ⋯⟩

noncomputable def AbramskySadrzadeh2014.distribution (R : Type r) [AddCommMonoid R] [One R] : CategoryTheory.Functor (Type u) (Type (max u r))

The distribution functor D_R.

Equations

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

The paper's examples

inductive AbramskySadrzadeh2014.Rel : ℕ → Type

Relation symbols of the paper's examples, by arity.

• 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

@[instance_reducible]

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

Equations

• AbramskySadrzadeh2014.instDecidableEqRel = AbramskySadrzadeh2014.instDecidableEqRel.decEq

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.

@[reducible, inline]

abbrev AbramskySadrzadeh2014.lang : FirstOrder.Language

The relational language of the examples.

Equations

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

inductive AbramskySadrzadeh2014.Var : Type

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

The literal A(x̄), or ¬A(x̄) for pos := false.

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'

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.

@[reducible, inline]

abbrev AbramskySadrzadeh2014.snoresCtx : DRT.Context lang Var

The glued context of the first example.

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} merging 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)

s₁ = {John(x), sleeps(x)}, s₂ = {snores(y)}.

Equations

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

def AbramskySadrzadeh2014.snoresGluing : DRT.Theory snoresCtx

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} factors through the cover, so the gluing is unique.

Example 2: John beats his donkey.

@[reducible, inline]

abbrev AbramskySadrzadeh2014.beatsCtx : DRT.Context lang Var

The glued context of the second example.

Equations

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

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

The cover x ↦ a, y ↦ b, 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)

s₁ = {John(x)}, s₂ = {donkey(y)}, 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

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)}: John(b) factors through no cover map, so adding it changes no restriction and the listed gluing is not unique.

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

Example 3: John owns a donkey. It is grey.

@[reducible, inline]

abbrev AbramskySadrzadeh2014.greyCtx : DRT.Context lang Var

The glued context of the third example.

Equations

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

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

The covering contexts of the third example.

Equations

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

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

s₁ = {John(x), Man(x)}, s₂ = {donkey(y), ¬Man(y)}, 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 merging it with John: x ↦ a, y ↦ a, z ↦ b.

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 forces Man and ¬Man of one referent.

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

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

Equations

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

def AbramskySadrzadeh2014.greyGluing : DRT.Theory greyCtx

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

Example 4: John put the cup on the plate. He broke it.

@[reducible, inline]

abbrev AbramskySadrzadeh2014.brokeCtx : DRT.Context lang Var

The glued context of the fourth example.

Equations

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

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

The covering contexts of the fourth example.

Equations

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

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

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

Equations

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

inductive AbramskySadrzadeh2014.Broken : Type

The two plausible antecedents of it.

• 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

The referent of each antecedent.

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 extending 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

{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.

The discussion example: overlapping vocabularies

@[reducible, inline]

abbrev AbramskySadrzadeh2014.overlapCtx : DRT.Context lang Var

The glued context of the discussion example.

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 x ↦ z, u ↦ w and y ↦ z, v ↦ w, both parts carrying 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)

s₁ = {R(x), S(u)}, 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 are consistent but do not glue: S(z) restricts to S(x) ∉ s₁.

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

cheeky.*

@[reducible, inline]

abbrev AbramskySadrzadeh2014.ripeCtx : DRT.Context lang Var

The glued context of the bananas discourse.

Equations

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

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

The covering contexts of the bananas discourse.

Equations

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

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

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

Equations

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

inductive AbramskySadrzadeh2014.Antecedent : Type

The antecedents available to each they.

• banana : Antecedent
• monkey : Antecedent

@[instance_reducible]

instance AbramskySadrzadeh2014.instDecidableEqAntecedent : DecidableEq Antecedent

Equations

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

@[instance_reducible]

instance AbramskySadrzadeh2014.instFintypeAntecedent : Fintype Antecedent

Equations

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

def AbramskySadrzadeh2014.Antecedent.var : Antecedent → Var

The referent of each antecedent.

Equations

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

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

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

The covering c extending 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 : Antecedent × Antecedent) : DRT.Theory ripeCtx

The candidate global section t_c induced by the covering c.

Equations

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

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

theorem AbramskySadrzadeh2014.ripeGluing_injective : Function.Injective ripeGluing

def AbramskySadrzadeh2014.ripeFrequency : Antecedent → ℕ

British News corpus frequencies of ripe banana and ripe monkey.

Equations

• AbramskySadrzadeh2014.ripeFrequency AbramskySadrzadeh2014.Antecedent.banana = 14
• AbramskySadrzadeh2014.ripeFrequency AbramskySadrzadeh2014.Antecedent.monkey = 0

def AbramskySadrzadeh2014.cheekyFrequency : Antecedent → ℕ

British News corpus frequencies of cheeky banana and cheeky monkey.

Equations

• AbramskySadrzadeh2014.cheekyFrequency AbramskySadrzadeh2014.Antecedent.banana = 0
• AbramskySadrzadeh2014.cheekyFrequency AbramskySadrzadeh2014.Antecedent.monkey = 10

noncomputable def AbramskySadrzadeh2014.coveringDistribution : Distribution ℚ (Antecedent × Antecedent)

Each covering weighted by the summed frequencies of its mergings, normalised.

Equations

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

noncomputable def AbramskySadrzadeh2014.gluingDistribution : Distribution ℚ (DRT.Theory ripeCtx)

The distribution d over global sections: the covering distribution pushed forward along c ↦ t_c.

Equations

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

theorem AbramskySadrzadeh2014.coveringDistribution_apply (c : Antecedent × Antecedent) : ↑coveringDistribution c = (↑(ripeFrequency c.1) + ↑(cheekyFrequency c.2)) / 48

theorem AbramskySadrzadeh2014.gluingDistribution_apply (c : Antecedent × Antecedent) : ↑gluingDistribution (ripeGluing c) = (↑(ripeFrequency c.1) + ↑(cheekyFrequency c.2)) / 48

theorem AbramskySadrzadeh2014.gluingDistribution_ripe : ↑gluingDistribution (ripeGluing (Antecedent.banana, Antecedent.monkey)) = 1 / 2 ∧ ∀ (c : Antecedent × Antecedent), ↑gluingDistribution (ripeGluing c) ≤ 1 / 2

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