Asher & Lascarides 2003: SDRT Right Frontier Constraint worked example

[AL03]

Example (21) from p. 149 — the discourse where the book explicitly enumerates which attachment sites are available under the Right Frontier Constraint, and which are excluded. We replicate it against the SDRT substrate to verify that availableAttachmentPoints returns exactly the book-predicted set.

The example (21), p. 149

π₀:
  ├─ π₃, π₄
  │  ├─ π₃: K_π₃
  │  ├─ ⇓(π₃, π₄)              ← subordinating topic relation
  │  └─ π₄:
  │     ├─ π₁, π₂
  │     ├─ π₁: K_π₁
  │     ├─ π₂: K_π₂
  │     └─ Background(π₁, π₂)   ← coordinating

Reading the labelling F:

• F(π₀) ⊇ ⇓(π₃, π₄) — the topic relation lives at the top level
• F(π₄) ⊇ Background(π₁, π₂) — the coordinated pair lives inside π₄
• F(π₁), F(π₂), F(π₃) are atomic clausal contents K_πᵢ

What the book asserts (p. 149)

"assuming that π₂ in (21) is LAST, the available attachment sites are π₂ (by condition 1), π₄ (by condition 2a), π₃ (by condition 2b and 3) and π₀ (by condition 3). But π₁ is not available."

Why π₁ is not available

π₁ and π₂ are siblings under Background, which is coordinating (not subordinating). After attaching to π₂ (LAST), the only way to reach π₁ would be through a subordinating relation — but Background doesn't qualify. Walking up via outscoping reaches π₄ (which contains both π₁ and π₂), and from π₄ we reach π₃ via the subordinating ⇓ relation. But π₁ is on the wrong side of a coordinating sibling boundary.

Substrate note

[AL03]'s ⇓ topic-relation is not in the substrate's RhetoricalRelation enum (it's a structural relation the book uses informally; the headline truth-conditional inventory is Narration / Elaboration / Explanation / Result / Background / Contrast / Parallel + Consequence / Alternation / Correction). We encode ⇓ as .elaboration in the example below — both are subordinating, and the RFC's condition 2b only sees the isSubordinating projection. The example would behave identically with a hypothetical .topic constructor.

Rhetorical-Structure Substrate (SDRT core)

[AL03] The labelled discourse-structure record + SDRT-specific projections (kind, veridicality) on top of the framework-neutral Discourse.Coherence.CoherenceRelation enum. The Right Frontier Constraint lives in the sibling RightFrontier.lean.

@[reducible, inline]

abbrev Discourse.Rhetorical.RhetoricalRelation : Type

SDRT vocabulary alias for the unified coherence-relation enum.

Equations

• Discourse.Rhetorical.RhetoricalRelation = Discourse.Coherence.CoherenceRelation

Structural Kind: subordinating vs coordinating vs structural

inductive Discourse.Rhetorical.RelationKind : Type

Structural kind of a rhetorical relation (Asher-Lascarides §4.7). The Right Frontier Constraint gates new attachment points on the subordinating case.

• subordinating : RelationKind
• coordinating : RelationKind
• structural : RelationKind

@[implicit_reducible]

instance Discourse.Rhetorical.instDecidableEqRelationKind : DecidableEq RelationKind

Equations

• Discourse.Rhetorical.instDecidableEqRelationKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Discourse.Rhetorical.instReprRelationKind.repr : RelationKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Discourse.Rhetorical.instReprRelationKind : Repr RelationKind

Equations

• Discourse.Rhetorical.instReprRelationKind = { reprPrec := Discourse.Rhetorical.instReprRelationKind.repr }

@[implicit_reducible]

instance Discourse.Rhetorical.instInhabitedRelationKind : Inhabited RelationKind

Equations

• Discourse.Rhetorical.instInhabitedRelationKind = { default := Discourse.Rhetorical.instInhabitedRelationKind.default }

def Discourse.Coherence.CoherenceRelation.sdrtKind : CoherenceRelation → Rhetorical.RelationKind

SDRT structural kind of each coherence relation.

Equations

• Discourse.Coherence.CoherenceRelation.elaboration.sdrtKind = Discourse.Rhetorical.RelationKind.subordinating
• Discourse.Coherence.CoherenceRelation.explanation.sdrtKind = Discourse.Rhetorical.RelationKind.subordinating
• Discourse.Coherence.CoherenceRelation.occasion.sdrtKind = Discourse.Rhetorical.RelationKind.coordinating
• Discourse.Coherence.CoherenceRelation.result.sdrtKind = Discourse.Rhetorical.RelationKind.coordinating
• Discourse.Coherence.CoherenceRelation.background.sdrtKind = Discourse.Rhetorical.RelationKind.coordinating
• Discourse.Coherence.CoherenceRelation.consequence.sdrtKind = Discourse.Rhetorical.RelationKind.coordinating
• Discourse.Coherence.CoherenceRelation.alternation.sdrtKind = Discourse.Rhetorical.RelationKind.coordinating
• Discourse.Coherence.CoherenceRelation.correction.sdrtKind = Discourse.Rhetorical.RelationKind.coordinating
• Discourse.Coherence.CoherenceRelation.contrast.sdrtKind = Discourse.Rhetorical.RelationKind.structural
• Discourse.Coherence.CoherenceRelation.parallel.sdrtKind = Discourse.Rhetorical.RelationKind.structural

def Discourse.Coherence.CoherenceRelation.isSubordinating (R : CoherenceRelation) : Prop

The coherence relation is subordinating in SDRT's sense.

Equations

• R.isSubordinating = (R.sdrtKind = Discourse.Rhetorical.RelationKind.subordinating)

@[implicit_reducible]

instance Discourse.Coherence.instDecidablePredCoherenceRelationIsSubordinating : DecidablePred CoherenceRelation.isSubordinating

Equations

• Discourse.Coherence.instDecidablePredCoherenceRelationIsSubordinating R = Discourse.Coherence.instDecidablePredCoherenceRelationIsSubordinating._aux_1 R

Veridicality

inductive Discourse.Rhetorical.Veridicality : Type

Veridicality classification for rhetorical relations (Asher-Lascarides §4.8). Determines whether R(α, β) requires both arguments' contents to be true, neither, or one denied.

• veridical : Veridicality
• nonVeridical : Veridicality
• denialBearing : Veridicality

@[implicit_reducible]

instance Discourse.Rhetorical.instDecidableEqVeridicality : DecidableEq Veridicality

Equations

• Discourse.Rhetorical.instDecidableEqVeridicality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Discourse.Rhetorical.instReprVeridicality.repr : Veridicality → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Discourse.Rhetorical.instReprVeridicality : Repr Veridicality

Equations

• Discourse.Rhetorical.instReprVeridicality = { reprPrec := Discourse.Rhetorical.instReprVeridicality.repr }

@[implicit_reducible]

instance Discourse.Rhetorical.instInhabitedVeridicality : Inhabited Veridicality

Equations

• Discourse.Rhetorical.instInhabitedVeridicality = { default := Discourse.Rhetorical.instInhabitedVeridicality.default }

def Discourse.Coherence.CoherenceRelation.veridicality : CoherenceRelation → Rhetorical.Veridicality

Veridicality of each rhetorical relation per SDRT ([AL03], preface "What's New" + §4.8).

Equations

• Discourse.Coherence.CoherenceRelation.occasion.veridicality = Discourse.Rhetorical.Veridicality.veridical
• Discourse.Coherence.CoherenceRelation.elaboration.veridicality = Discourse.Rhetorical.Veridicality.veridical
• Discourse.Coherence.CoherenceRelation.explanation.veridicality = Discourse.Rhetorical.Veridicality.veridical
• Discourse.Coherence.CoherenceRelation.result.veridicality = Discourse.Rhetorical.Veridicality.veridical
• Discourse.Coherence.CoherenceRelation.background.veridicality = Discourse.Rhetorical.Veridicality.veridical
• Discourse.Coherence.CoherenceRelation.contrast.veridicality = Discourse.Rhetorical.Veridicality.veridical
• Discourse.Coherence.CoherenceRelation.parallel.veridicality = Discourse.Rhetorical.Veridicality.veridical
• Discourse.Coherence.CoherenceRelation.alternation.veridicality = Discourse.Rhetorical.Veridicality.nonVeridical
• Discourse.Coherence.CoherenceRelation.consequence.veridicality = Discourse.Rhetorical.Veridicality.nonVeridical
• Discourse.Coherence.CoherenceRelation.correction.veridicality = Discourse.Rhetorical.Veridicality.denialBearing

SDRS — Segmented Discourse Representation Structure

structure Discourse.Rhetorical.SDRSEdge (L : Type u_1) : Type u_1

A discourse-relation conjunct in an SDRS: R(source, target) is a conjunct in F(container)'s content. The container field distinguishes i-outscopes from generic endpoint relations.

• container : L
• source : L
• target : L
• relation : RhetoricalRelation

@[implicit_reducible]

instance Discourse.Rhetorical.instReprSDRSEdge {L✝ : Type u_1} [Repr L✝] : Repr (SDRSEdge L✝)

Equations

• Discourse.Rhetorical.instReprSDRSEdge = { reprPrec := Discourse.Rhetorical.instReprSDRSEdge.repr }

def Discourse.Rhetorical.instReprSDRSEdge.repr {L✝ : Type u_1} [Repr L✝] : SDRSEdge L✝ → ℕ → Std.Format

Equations

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

def Discourse.Rhetorical.instDecidableEqSDRSEdge.decEq {L✝ : Type u_1} [DecidableEq L✝] (x✝ x✝¹ : SDRSEdge L✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Discourse.Rhetorical.instDecidableEqSDRSEdge {L✝ : Type u_1} [DecidableEq L✝] : DecidableEq (SDRSEdge L✝)

Equations

• Discourse.Rhetorical.instDecidableEqSDRSEdge = Discourse.Rhetorical.instDecidableEqSDRSEdge.decEq

structure Discourse.Rhetorical.SDRS (L : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

A Segmented Discourse Representation Structure (Asher-Lascarides Def 13, ⟨A, F⟩ form). Polymorphic in label type L and content type α. Condition L5 ("unique parent") is intentionally omitted per the book p. 144.

• labels : List L
• content : L → α
• edges : List (SDRSEdge L)
• root : L
• last : L

def Discourse.Rhetorical.SDRS.initial {L : Type u_1} {α : Type u_2} (root : L) (rootContent : L → α) : SDRS L α

An empty SDRS with one root label, no edges; root is also LAST.

Equations

• Discourse.Rhetorical.SDRS.initial root rootContent = { labels := [root], content := rootContent, edges := [], root := root, last := root }

def Discourse.Rhetorical.SDRS.addEdge {L : Type u_1} {α : Type u_2} (s : SDRS L α) (e : SDRSEdge L) : SDRS L α

Add an edge to an SDRS. Does not add the labels — caller must ensure both source and target are already in labels.

Equations

• s.addEdge e = { labels := s.labels, content := s.content, edges := e :: s.edges, root := s.root, last := s.last }

def Discourse.Rhetorical.SDRS.attach {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) (newLabel : L) (newContent : α) (container parent : L) (relation : RhetoricalRelation) : SDRS L α

Attach a new labelled unit to parent via relation, recording the conjunct in container's content. The new unit becomes LAST.

Equations

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

Outscopes (i-outscopes from Def 14 condition 2a)

def Discourse.Rhetorical.iOutscopes {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) (γ α' : L) : Prop

iOutscopes s γ α' — γ immediately outscopes α': some edge with container γ mentions α' as source or target.

Equations

• Discourse.Rhetorical.iOutscopes s γ α' = ∃ (e : Discourse.Rhetorical.SDRSEdge L), e ∈ s.edges ∧ e.container = γ ∧ (e.source = α' ∨ e.target = α')

@[implicit_reducible]

instance Discourse.Rhetorical.instDecidableIOutscopes {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) (γ α' : L) : Decidable (iOutscopes s γ α')

Equations

• Discourse.Rhetorical.instDecidableIOutscopes s γ α' = id (List.decidableBEx (fun (e : Discourse.Rhetorical.SDRSEdge L) => e.container = γ ∧ (e.source = α' ∨ e.target = α')) s.edges)

Right Frontier Constraint

[AL03] Available-attachment-points constraint restricting where new discourse units attach in an SDRS. α = LAST is always available; labels γ that outscope α structurally or are connected via a subordinating relation are also available, transitively closed. The central structural constraint on SDRT anaphora resolution.

The single-step "<" relation (Def 14 conditions 2a + 2b)

def Discourse.Rhetorical.dominatesOneStep {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) (α' γ : L) : Prop

γ dominates α' in one step: γ outscopes α' (2a) or there is a subordinating-relation edge from γ to α' (2b).

Equations

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

@[implicit_reducible]

instance Discourse.Rhetorical.instDecidableDominatesOneStep {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) (α' γ : L) : Decidable (dominatesOneStep s α' γ)

Equations

• Discourse.Rhetorical.instDecidableDominatesOneStep s α' γ = id instDecidableOr

Available attachment points (Def 14, transitively closed)

def Discourse.Rhetorical.availableViaChain {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) (α' γ : L) : ℕ → Prop

availableViaChain s α γ n — γ dominates α via a chain of length ≤ n of dominatesOneStep steps. Bounded because the transitive closure on a finite SDRS terminates.

Equations

• One or more equations did not get rendered due to their size.
• Discourse.Rhetorical.availableViaChain s α' γ 0 = (α' = γ)

@[implicit_reducible]

instance Discourse.Rhetorical.instDecidableAvailableViaChain {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) (α' γ : L) (n : ℕ) : Decidable (availableViaChain s α' γ n)

Equations

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

def Discourse.Rhetorical.availableAttachmentPoints {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) : List L

Labels available for new attachment from s.last: those reachable via dominatesOneStep within s.labels.length steps.

Equations

• Discourse.Rhetorical.availableAttachmentPoints s = List.filter (fun (γ : L) => decide (Discourse.Rhetorical.availableViaChain s s.last γ s.labels.length)) s.labels

Structural theorems

theorem Discourse.Rhetorical.last_self_available {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) : availableViaChain s s.last s.last 0

LAST is always its own available attachment point (Def 14 condition 1). Holds at chain length 0.

theorem Discourse.Rhetorical.availableViaChain_mono {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) (α' γ : L) (n : ℕ) : availableViaChain s α' γ n → availableViaChain s α' γ (n + 1)

The available-via-chain relation is monotone in the chain length: longer chains include shorter ones.

theorem Discourse.Rhetorical.oneStep_available {L : Type u_1} {α : Type u_2} [DecidableEq L] (s : SDRS L α) (α' γ : L) (hγ : γ ∈ s.labels) (h : dominatesOneStep s α' γ) : availableViaChain s α' γ 1

α' < γ (one-step domination) implies γ is available from α' at chain length 1. Headline corollary of Def 14 condition 2.

@[reducible, inline]

abbrev AsherLascarides2003.Label : Type

Equations

• AsherLascarides2003.Label = ℕ

@[reducible, inline]

abbrev AsherLascarides2003.Content : Type

Equations

• AsherLascarides2003.Content = String

def AsherLascarides2003.example21 : Discourse.Rhetorical.SDRS Label Content

Example (21) from [AL03] p. 149, with LAST = π₂.

Labels: 0 = π₀, 1 = π₁, 2 = π₂, 3 = π₃, 4 = π₄.

Edges encode the labelled-discourse-structure conjuncts:

• ⟨0, 3, 4, .elaboration⟩ represents ⇓(π₃, π₄) ∈ F(π₀) (using .elaboration as a stand-in for ⇓; both subordinating).
• ⟨4, 1, 2, .background⟩ represents Background(π₁, π₂) ∈ F(π₄).

Plus container-marking edges so that iOutscopes recovers the box-containment structure:

• π₀ contains π₃ and π₄
• π₄ contains π₁ and π₂

These containment relations are conjuncts in the parent box's F-content (the book's "labels A and labelling F" representation — being a label inside a box IS a content fact about the parent). We encode them as additional outscoping conjuncts using the same edge structure.

For Example (21) specifically, the ⇓(π₃, π₄) and Background(π₁, π₂) edges already encode the containment (since these relations have π₃, π₄, π₁, π₂ as arguments and the relations themselves live in F(π₀) and F(π₄) respectively). No additional outscoping edges needed.

Equations

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

theorem AsherLascarides2003.pi_1_not_available_from_pi_2 : ¬1 ∈ Discourse.Rhetorical.availableAttachmentPoints example21

Book p. 149 headline claim: π₁ is NOT in the available attachment set from π₂ (Example 21).

The reason: π₁ and π₂ are siblings under Background, which is coordinating (not subordinating). RFC's condition 2b only opens up new attachment sites via subordinating relations, so the sibling-via-coordinating π₁ is unreachable from π₂'s right frontier.

theorem AsherLascarides2003.available_attachment_points_match : Discourse.Rhetorical.availableAttachmentPoints example21 = [0, 2, 3, 4]

The full available set from π₂ matches the book's prediction: {π₀, π₂, π₃, π₄}.