Accessibility of discourse referents

A discourse referent is accessible from a condition when it is declared in a box that is accessible where the condition occurs: the box containing the condition, the boxes it is nested in, and the antecedent of a conditional for its consequent (Kamp and Reyle, Def. 1.4.11, Def. 2.1.3, Def. 2.4.4). Accessibility is a property of occurrences: one box can occur twice in a DRS, at places with different accessible boxes. An occurrence is reached from the host by a walk that steps into the sub-boxes of complex conditions, collecting the boxes accessible at each step, and the walk is computed by a structural recursion that decides accessibility.

Main definitions

• DRT.ScopeStep, DRT.Occurrence: a step into a sub-box, collecting the accessible boxes, and the occurrences of boxes in a host.
• DRT.AccessibleFrom: a referent accessible from a condition (Def. 1.4.11).
• DRT.DRS.Accessible: a referent accessible where another is declared.
• DRT.AccessibleTo: a box accessible to another, in the sense of Geurts, Beaver and Maier.

Main statements

• DRT.DRS.mem_occurrences_iff: the computed occurrences are exactly those reached by the walk, so DRS.Accessible is decidable.

Implementation notes

Kamp and Reyle state Def. 2.1.3 and Def. 2.4.4 for DRS values. Read on values, they let a chain pass through a second occurrence of an equal box and make a referent accessible where no occurrence of the condition sees it, so the definitions here quantify over occurrences.

References

• [KR93]
• [vE06]
• [GBM24]

inductive DRT.ScopeStep {L : FirstOrder.Language} {V : Type w} : List (DRS L V) × DRS L V → List (DRS L V) × DRS L V → Prop

One step of the walk, from an occurrence of a box D whose accessible boxes are bs (innermost first, D included) into a sub-box of one of its complex conditions; the consequent of a conditional also sees the antecedent.

• neg {L : FirstOrder.Language} {V : Type w} {bs : List (DRS L V)} {D K : DRS L V} : Condition.neg K ∈ D.conditions → ScopeStep (bs, D) (K :: bs, K)
• impAnte {L : FirstOrder.Language} {V : Type w} {bs : List (DRS L V)} {D a c : DRS L V} : Condition.imp a c ∈ D.conditions → ScopeStep (bs, D) (a :: bs, a)
• impCons {L : FirstOrder.Language} {V : Type w} {bs : List (DRS L V)} {D a c : DRS L V} : Condition.imp a c ∈ D.conditions → ScopeStep (bs, D) (c :: a :: bs, c)
• disL {L : FirstOrder.Language} {V : Type w} {bs : List (DRS L V)} {D l r : DRS L V} : Condition.dis l r ∈ D.conditions → ScopeStep (bs, D) (l :: bs, l)
• disR {L : FirstOrder.Language} {V : Type w} {bs : List (DRS L V)} {D l r : DRS L V} : Condition.dis l r ∈ D.conditions → ScopeStep (bs, D) (r :: bs, r)

@[reducible, inline]

abbrev DRT.Occurrence {L : FirstOrder.Language} {V : Type w} (host : DRS L V) : List (DRS L V) × DRS L V → Prop

Occurrence host (bs, K) says the walk from host reaches an occurrence of K whose accessible boxes are bs.

Equations

• DRT.Occurrence host = Relation.ReflTransGen DRT.ScopeStep ([host], host)

theorem DRT.Occurrence.weakSubordinate {L : FirstOrder.Language} {V : Type w} {host K : DRS L V} {bs : List (DRS L V)} (h : Occurrence host (bs, K)) : WeakSubordinate K host

The occurrence of a box is an occurrence of a sub-DRS of the host.

def DRT.scopeReferents {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (bs : List (DRS L V)) : Finset V

scopeReferents bs collects the referents declared by the boxes bs.

Equations

• DRT.scopeReferents bs = List.foldr (fun (B : DRT.DRS L V) (s : Finset V) => B.referents ∪ s) ∅ bs

@[simp]

theorem DRT.scopeReferents_nil {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : scopeReferents [] = ∅

@[simp]

theorem DRT.scopeReferents_cons {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (B : DRS L V) (bs : List (DRS L V)) : scopeReferents (B :: bs) = B.referents ∪ scopeReferents bs

def DRT.AccessibleFrom {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (host : DRS L V) (x : V) (γ : Condition L V) : Prop

The referent x is accessible from the condition γ in host when γ occurs in a box at an occurrence whose accessible boxes declare x (Def. 1.4.11, Def. 2.1.3).

Equations

• DRT.AccessibleFrom host x γ = ∃ (p : List (DRT.DRS L V) × DRT.DRS L V), DRT.Occurrence host p ∧ γ ∈ p.2.conditions ∧ x ∈ DRT.scopeReferents p.1

def DRT.DRS.Accessible {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (host : DRS L V) (u v : V) : Prop

v is accessible where u is declared when some occurrence of a box declaring u has v among its accessible referents.

Equations

• host.Accessible u v = ∃ (p : List (DRT.DRS L V) × DRT.DRS L V), DRT.Occurrence host p ∧ u ∈ p.2.referents ∧ v ∈ DRT.scopeReferents p.1

def DRT.AccessibleTo {L : FirstOrder.Language} {V : Type w} (host K₁ K₂ : DRS L V) : Prop

The box K₁ is accessible to K₂ in host when it is among the boxes accessible at some occurrence of K₂.

Equations

• DRT.AccessibleTo host K₁ K₂ = ∃ (bs : List (DRT.DRS L V)), DRT.Occurrence host (bs, K₂) ∧ K₁ ∈ bs

Computing the occurrences

The occurrences below a box are listed by structural recursion through the nested conditions, matching each box as ⟨U, cs⟩, so that the kernel evaluates the list and decide closes concrete accessibility claims.

def DRT.Condition.occurrences {L : FirstOrder.Language} {V : Type w} : Condition L V → List (DRS L V) → List (List (DRS L V) × DRS L V)

The occurrences of boxes below a condition, at accessible boxes bs.

Equations

• One or more equations did not get rendered due to their size.
• (DRT.Condition.atom a).occurrences x✝ = []
• (DRT.Condition.eq u v).occurrences x✝ = []

def DRT.Condition.occurrencesList {L : FirstOrder.Language} {V : Type w} : List (Condition L V) → List (DRS L V) → List (List (DRS L V) × DRS L V)

The occurrences of boxes below a list of conditions.

Equations

• DRT.Condition.occurrencesList [] x✝ = []
• DRT.Condition.occurrencesList (c :: cs) x✝ = c.occurrences x✝ ++ DRT.Condition.occurrencesList cs x✝

def DRT.DRS.occurrences {L : FirstOrder.Language} {V : Type w} (bs : List (DRS L V)) (K : DRS L V) : List (List (DRS L V) × DRS L V)

The occurrences of boxes at or below an occurrence of K at accessible boxes bs.

Equations

• DRT.DRS.occurrences bs K = (bs, K) :: DRT.Condition.occurrencesList K.conditions bs

theorem DRT.Condition.occurrences_neg {L : FirstOrder.Language} {V : Type w} (bs : List (DRS L V)) (K : DRS L V) : (neg K).occurrences bs = DRS.occurrences (K :: bs) K

theorem DRT.Condition.occurrences_imp {L : FirstOrder.Language} {V : Type w} (bs : List (DRS L V)) (a c : DRS L V) : (imp a c).occurrences bs = DRS.occurrences (a :: bs) a ++ DRS.occurrences (c :: a :: bs) c

theorem DRT.Condition.occurrences_dis {L : FirstOrder.Language} {V : Type w} (bs : List (DRS L V)) (l r : DRS L V) : (dis l r).occurrences bs = DRS.occurrences (l :: bs) l ++ DRS.occurrences (r :: bs) r

theorem DRT.Condition.mem_occurrencesList {L : FirstOrder.Language} {V : Type w} {cs : List (Condition L V)} {bs : List (DRS L V)} {p : List (DRS L V) × DRS L V} : p ∈ occurrencesList cs bs ↔ ∃ c ∈ cs, p ∈ c.occurrences bs

theorem DRT.DRS.mem_occurrences {L : FirstOrder.Language} {V : Type w} {bs : List (DRS L V)} {K : DRS L V} {p : List (DRS L V) × DRS L V} : p ∈ occurrences bs K ↔ p = (bs, K) ∨ ∃ c ∈ K.conditions, p ∈ c.occurrences bs

theorem DRT.Condition.occurrence_of_mem {L : FirstOrder.Language} {V : Type w} (c : Condition L V) {bs : List (DRS L V)} {D : DRS L V} {p : List (DRS L V) × DRS L V} : c ∈ D.conditions → p ∈ c.occurrences bs → Relation.ReflTransGen ScopeStep (bs, D) p

Everything listed below a condition of D is reached by the walk from (bs, D).

theorem DRT.DRS.mem_occurrences_iff {L : FirstOrder.Language} {V : Type w} {bs : List (DRS L V)} {K : DRS L V} {p : List (DRS L V) × DRS L V} : p ∈ occurrences bs K ↔ Relation.ReflTransGen ScopeStep (bs, K) p

The computed occurrences are exactly those the walk reaches.

@[instance_reducible]

instance DRT.instDecidableAccessible {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (host : DRS L V) (u v : V) : Decidable (host.Accessible u v)

Equations

• DRT.instDecidableAccessible host u v = decidable_of_iff (∃ p ∈ DRT.DRS.occurrences [host] host, u ∈ p.2.referents ∧ v ∈ DRT.scopeReferents p.1) ⋯