Asher & Lascarides 2003: the right frontier

In Segmented Discourse Representation Theory a discourse is a set of labelled constituents whose contents include rhetorical relations between labels. New information may attach only at an available label: the last label, any label whose content contains a relation mentioning an available label, and any label linked to an available one by a subordinating relation — Elaboration, Explanation, or the topic relation — but not by a coordinating one such as Narration or Background. In the book's five-sentence narrative, an evening elaborated by a meal and a dance competition, with the meal elaborated by salmon and cheese, the salmon clause is off the frontier once the competition is last, so It was a beautiful pink cannot continue the discourse. In the book's abstract example, a topic over a constituent containing two units related by Background, the first of those units is the one label not available.

Main definitions

• Rel, Rel.Subordinating: rhetorical relations, including the topic relation ⇓.
• SDRS, SDRS.Above, SDRS.Available: labelled structures, one-step ascent on the frontier, and availability as its reflexive-transitive closure from the last label.
• example17, example21: the two worked structures and their frontiers.

References

• [AL03]

Rhetorical relations

inductive AsherLascarides2003.Rel : Type

The rhetorical relations of the worked structures, with the topic relation ⇓ between a summarizing constituent and the one it summarizes.

• narration : Rel
• background : Rel
• elaboration : Rel
• explanation : Rel
• topic : Rel

@[instance_reducible]

instance AsherLascarides2003.instDecidableEqRel : DecidableEq Rel

Equations

• AsherLascarides2003.instDecidableEqRel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev AsherLascarides2003.Rel.Subordinating (r : Rel) : Prop

Elaboration, Explanation, and the topic relation subordinate; Narration and Background coordinate.

Equations

• r.Subordinating = (r = AsherLascarides2003.Rel.elaboration ∨ r = AsherLascarides2003.Rel.explanation ∨ r = AsherLascarides2003.Rel.topic)

Structures and the right frontier

structure AsherLascarides2003.Edge (L : Type u_2) : Type u_2

A relation conjunct R(source, target) in the content of container.

• container : L
• source : L
• target : L
• relation : Rel

def AsherLascarides2003.instDecidableEqEdge.decEq {L✝ : Type u_2} [DecidableEq L✝] (x✝ x✝¹ : Edge L✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance AsherLascarides2003.instDecidableEqEdge {L✝ : Type u_2} [DecidableEq L✝] : DecidableEq (Edge L✝)

Equations

• AsherLascarides2003.instDecidableEqEdge = AsherLascarides2003.instDecidableEqEdge.decEq

structure AsherLascarides2003.SDRS (L : Type u_2) : Type u_2

A segmented discourse representation structure: its relation conjuncts and last label.

• edges : List (Edge L)
• last : L

def AsherLascarides2003.SDRS.Above {L : Type u_1} (s : SDRS L) (α γ : L) : Prop

One step up the frontier from α to γ: a relation in γ's content mentions α, or a subordinating relation runs from γ to α.

Equations

• s.Above α γ = ((∃ e ∈ s.edges, e.container = γ ∧ (e.source = α ∨ e.target = α)) ∨ ∃ e ∈ s.edges, e.source = γ ∧ e.target = α ∧ e.relation.Subordinating)

@[instance_reducible]

instance AsherLascarides2003.instDecidableAboveOfDecidableEq {L : Type u_1} [DecidableEq L] (s : SDRS L) (α γ : L) : Decidable (s.Above α γ)

Equations

• AsherLascarides2003.instDecidableAboveOfDecidableEq s α γ = id inferInstance

def AsherLascarides2003.SDRS.Available {L : Type u_1} (s : SDRS L) : L → Prop

A label is available for attachment when it lies on the right frontier: reachable from the last label by ascending.

Equations

• s.Available = Relation.ReflTransGen s.Above s.last

The worked examples

def AsherLascarides2003.example17 : SDRS ℕ

The structure of the five-sentence narrative: the evening 1 elaborated by 6, in which the meal 2 is narrated with the competition 5 and elaborated by 7, in which the salmon 3 is narrated with the cheese 4; the competition is last.

Equations

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

theorem AsherLascarides2003.available17_iff (γ : ℕ) : example17.Available γ ↔ γ ∈ [0, 1, 5, 6]

The frontier of the narrative is the competition, the constituent containing it, the evening it elaborates, and the root.

def AsherLascarides2003.antecedentLabel? (r : Datum) : Option ℕ

The label of the constituent introducing a row's pronoun antecedent.

Equations

• AsherLascarides2003.antecedentLabel? r = match r.feature? "antecedentLabel" with | some "3" => some 3 | x => none

theorem AsherLascarides2003.rows_continuation (r : Datum) : r ∈ Examples.all → ∀ a ∈ antecedentLabel? r, r.judgment = Judgment.acceptable ↔ example17.Available a

A continuation whose pronoun needs an antecedent off the frontier is not acceptable.

def AsherLascarides2003.example21 : SDRS ℕ

The abstract example: a topic 3 over a constituent 4 whose content relates 1 and 2 by Background, with 2 last.

Equations

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

theorem AsherLascarides2003.available21_iff (γ : ℕ) : example21.Available γ ↔ γ ∈ [0, 2, 3, 4]

The frontier is the last label, the constituent containing it, the topic above that, and the root; the Background sibling 1 is not on it.