The Table Model

[FB10]

n-agent table-model substrate: a stack of at-issue items, per-agent commitment slates, and a common ground.

Main definitions

• Item A W — speaker, addressee, mood, alternatives.
• DiscourseState A W I — ⟨table, dc, cg⟩, polymorphic in the table-element type I (full model: I := Item A W).
• DiscourseState.IsStable — empty-table predicate.
• pushItem, popItem, addCommit, addToCG — primitive updates.

TODO

• Projected set ps(CommonGround), highlighting ([FR17]), item identity (for withdrawal).

structure Discourse.Commitment.Table.Item (A : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

An at-issue item on the conversational table.

• speaker : A

  Speaker of the utterance.

• addressee : A

  Addressee.

• mood : Semantics.Mood.IllocutionaryMood

  Illocutionary force.

• alternatives : List (W → Prop)

  Alternatives at issue: [p] for assertion, [p, ¬p] for polar question, the answer set for wh-questions.

structure Discourse.Commitment.Table.DiscourseState (A : Type u_1) (W : Type u_2) (I : Type u_3) : Type (max (max u_1 u_2) u_3)

The discourse structure (DS) of [FB10], polymorphic in the table-element type I (full model: I := Item A W).

• table : List I

  Stack of unresolved items, head = most recent.

• dc : A → TaggedSlate W

  Per-agent discourse commitments.

• cg : CommonGround W

  The common ground.

def Discourse.Commitment.Table.DiscourseState.empty {A : Type u_1} {W : Type u_2} {I : Type u_3} : DiscourseState A W I

Initial state: empty table, empty commitments, trivial CommonGround.

Equations

• Discourse.Commitment.Table.DiscourseState.empty = { table := [], dc := fun (x : A) => Discourse.Commitment.TaggedSlate.empty, cg := CommonGround.empty }

@[implicit_reducible]

instance Discourse.Commitment.Table.DiscourseState.instInhabited {A : Type u_1} {W : Type u_2} {I : Type u_3} : Inhabited (DiscourseState A W I)

Equations

• Discourse.Commitment.Table.DiscourseState.instInhabited = { default := Discourse.Commitment.Table.DiscourseState.empty }

def Discourse.Commitment.Table.DiscourseState.IsStable {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) : Prop

The state is stable when the table is empty.

Equations

• s.IsStable = (s.table.isEmpty = true)

@[implicit_reducible]

instance Discourse.Commitment.Table.DiscourseState.instDecidableIsStable {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) : Decidable s.IsStable

Equations

• s.instDecidableIsStable = Discourse.Commitment.Table.DiscourseState.instDecidableIsStable._aux_1 s

def Discourse.Commitment.Table.DiscourseState.contextSet {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) : Set W

Worlds compatible with the common ground.

Equations

• s.contextSet = s.cg.contextSet

Commitment accessors

First-class views of an agent's commitments, collapsing the (s.dc a).proj two-step that recurs across consumers.

def Discourse.Commitment.Table.DiscourseState.doxasticOf {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (a : A) : List (W → Prop)

Agent a's doxastic (act-as-if-believe) commitments, untagged.

Equations

• s.doxasticOf a = (s.dc a).doxasticContents

def Discourse.Commitment.Table.DiscourseState.Commits {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (a : A) (p : W → Prop) : Prop

a is doxastically committed to p.

Equations

• s.Commits a p = (p ∈ s.doxasticOf a)

def Discourse.Commitment.Table.DiscourseState.cgPropositions {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) : List (Set W)

The common-ground propositions.

Equations

• s.cgPropositions = s.cg.propositions

Primitive updates

def Discourse.Commitment.Table.DiscourseState.pushItem {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (i : I) : DiscourseState A W I

Equations

• s.pushItem i = { table := i :: s.table, dc := s.dc, cg := s.cg }

def Discourse.Commitment.Table.DiscourseState.popItem {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) : DiscourseState A W I

Equations

• s.popItem = { table := s.table.tail, dc := s.dc, cg := s.cg }

def Discourse.Commitment.Table.DiscourseState.addToCG {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (p : W → Prop) : DiscourseState A W I

Equations

• s.addToCG p = { table := s.table, dc := s.dc, cg := s.cg.add p }

def Discourse.Commitment.Table.DiscourseState.addCommit {A : Type u_1} {W : Type u_2} {I : Type u_3} [DecidableEq A] (s : DiscourseState A W I) (a : A) (p : W → Prop) (src : CommitmentSource := CommitmentSource.selfGenerated) (force : CommitmentForce := CommitmentForce.doxastic) : DiscourseState A W I

Add (p, src, force) to agent a's slate. Defaults: self-generated, doxastic — the standard assertion-driven cell.

Equations

• s.addCommit a p src force = { table := s.table, dc := Function.update s.dc a ((s.dc a).add p src force), cg := s.cg }

Basic theorems

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.empty_table {A : Type u_1} {W : Type u_2} {I : Type u_3} : empty.table = []

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.empty_dc {A : Type u_1} {W : Type u_2} {I : Type u_3} (a : A) : empty.dc a = TaggedSlate.empty

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.empty_cg {A : Type u_1} {W : Type u_2} {I : Type u_3} : empty.cg = CommonGround.empty

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.empty_isStable {A : Type u_1} {W : Type u_2} {I : Type u_3} : empty.IsStable

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.pushItem_table {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (i : I) : (s.pushItem i).table = i :: s.table

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.pushItem_dc {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (i : I) : (s.pushItem i).dc = s.dc

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.pushItem_cg {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (i : I) : (s.pushItem i).cg = s.cg

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.popItem_table {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) : s.popItem.table = s.table.tail

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.popItem_dc {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) : s.popItem.dc = s.dc

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.popItem_cg {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) : s.popItem.cg = s.cg

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.addToCG_cg {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (p : W → Prop) : (s.addToCG p).cg = s.cg.add p

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.addToCG_table {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (p : W → Prop) : (s.addToCG p).table = s.table

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.addToCG_dc {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (p : W → Prop) : (s.addToCG p).dc = s.dc

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.addCommit_table {A : Type u_1} {W : Type u_2} {I : Type u_3} [DecidableEq A] (s : DiscourseState A W I) (a : A) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce) : (s.addCommit a p src force).table = s.table

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.addCommit_cg {A : Type u_1} {W : Type u_2} {I : Type u_3} [DecidableEq A] (s : DiscourseState A W I) (a : A) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce) : (s.addCommit a p src force).cg = s.cg

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.addCommit_dc_self {A : Type u_1} {W : Type u_2} {I : Type u_3} [DecidableEq A] (s : DiscourseState A W I) (a : A) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce) : (s.addCommit a p src force).dc a = (s.dc a).add p src force

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.addCommit_dc_of_ne {A : Type u_1} {W : Type u_2} {I : Type u_3} [DecidableEq A] (s : DiscourseState A W I) {a b : A} (h : b ≠ a) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce) : (s.addCommit a p src force).dc b = s.dc b

Accessor reductions

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.doxasticOf_addCommit_self {A : Type u_1} {W : Type u_2} {I : Type u_3} [DecidableEq A] (s : DiscourseState A W I) (a : A) (p : W → Prop) (src : CommitmentSource) : (s.addCommit a p src).doxasticOf a = p :: s.doxasticOf a

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.doxasticOf_addCommit_of_ne {A : Type u_1} {W : Type u_2} {I : Type u_3} [DecidableEq A] (s : DiscourseState A W I) {a b : A} (h : b ≠ a) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce) : (s.addCommit a p src force).doxasticOf b = s.doxasticOf b

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.doxasticOf_pushItem {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (i : I) (a : A) : (s.pushItem i).doxasticOf a = s.doxasticOf a

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.doxasticOf_popItem {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (a : A) : s.popItem.doxasticOf a = s.doxasticOf a

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.cgPropositions_popItem {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) : s.popItem.cgPropositions = s.cgPropositions

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.doxasticOf_addToCG {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (p : W → Prop) (a : A) : (s.addToCG p).doxasticOf a = s.doxasticOf a

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.cgPropositions_addToCG {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (p : W → Prop) : (s.addToCG p).cgPropositions = p :: s.cgPropositions

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.cgPropositions_addCommit {A : Type u_1} {W : Type u_2} {I : Type u_3} [DecidableEq A] (s : DiscourseState A W I) (a : A) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce) : (s.addCommit a p src force).cgPropositions = s.cgPropositions

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.cgPropositions_pushItem {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (i : I) : (s.pushItem i).cgPropositions = s.cgPropositions

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.empty_doxasticOf {A : Type u_1} {W : Type u_2} {I : Type u_3} (a : A) : empty.doxasticOf a = []

@[simp]

theorem Discourse.Commitment.Table.DiscourseState.empty_cgPropositions {A : Type u_1} {W : Type u_2} {I : Type u_3} : empty.cgPropositions = []

theorem Discourse.Commitment.Table.DiscourseState.pushItem_not_isStable {A : Type u_1} {W : Type u_2} {I : Type u_3} (s : DiscourseState A W I) (i : I) : ¬(s.pushItem i).IsStable

@[implicit_reducible]

instance Discourse.Commitment.Table.instHasContextSetDiscourseState {A : Type u_1} {W : Type u_2} {I : Type u_3} : CommonGround.HasContextSet (DiscourseState A W I) W

Equations

• Discourse.Commitment.Table.instHasContextSetDiscourseState = { toContextSet := Discourse.Commitment.Table.DiscourseState.contextSet }

@[reducible, inline]

abbrev Discourse.Commitment.Table.ItemState (A : Type u_1) (W : Type u_2) : Type (max (max u_1 u_2) u_2 u_1)

The full Farkas-Bruce model: the table holds rich speech-act Items.

Equations

• Discourse.Commitment.Table.ItemState A W = Discourse.Commitment.Table.DiscourseState A W (Discourse.Commitment.Table.Item A W)

Farkas-Bruce dynamics

The [FB10] discourse moves — assertion, polar question, acceptance — over the 2-participant specialisation State W, with the plain speaker/listener commitment views (dcS/dcL) recovered from the per-agent slate so an F&B trace yields one-line equational facts.

@[reducible, inline]

abbrev Discourse.Commitment.Table.State (W : Type u_1) : Type u_1

The 2-participant Farkas-Bruce state, specialised over DiscourseRole.

Equations

• Discourse.Commitment.Table.State W = Discourse.Commitment.Table.ItemState Discourse.DiscourseRole W

def Discourse.Commitment.Table.assert {W : Type u_1} (ds : State W) (p : W → Prop) : State W

Speaker asserts p: doxastically commits to p and pushes a declarative item [p] onto the table.

Equations

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

def Discourse.Commitment.Table.polarQuestion {W : Type u_1} (ds : State W) (p : W → Prop) : State W

Speaker poses the polar question ?p: push interrogative item [p, ¬p]. No commitments added.

Equations

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

def Discourse.Commitment.Table.acceptTop {W : Type u_1} (ds : State W) : State W

Addressee accepts the head alternative of the top item: other-generated doxastic commit, add to common ground, pop.

Equations

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

def Discourse.Commitment.Table.DiscourseState.dcS {W : Type u_1} (ds : State W) : List (W → Prop)

Speaker's discourse commitments (F&B dcS); dot-accessible on State.

Equations

• Discourse.Commitment.Table.DiscourseState.dcS ds = Discourse.Commitment.Table.DiscourseState.doxasticOf ds Discourse.DiscourseRole.speaker

def Discourse.Commitment.Table.DiscourseState.dcL {W : Type u_1} (ds : State W) : List (W → Prop)

Addressee's discourse commitments (F&B dcL).

Equations

• Discourse.Commitment.Table.DiscourseState.dcL ds = Discourse.Commitment.Table.DiscourseState.doxasticOf ds Discourse.DiscourseRole.addressee

@[simp]

theorem Discourse.Commitment.Table.assert_cg {W : Type u_1} (ds : State W) (p : W → Prop) : (assert ds p).cg = ds.cg

@[simp]

theorem Discourse.Commitment.Table.assert_table {W : Type u_1} (ds : State W) (p : W → Prop) : (assert ds p).table = { speaker := DiscourseRole.speaker, addressee := DiscourseRole.addressee, mood := Semantics.Mood.IllocutionaryMood.declarative, alternatives := [p] } :: ds.table

theorem Discourse.Commitment.Table.assert_dc_speaker_doxasticContents {W : Type u_1} (ds : State W) (p : W → Prop) : p ∈ ((assert ds p).dc DiscourseRole.speaker).doxasticContents

theorem Discourse.Commitment.Table.assert_not_isStable {W : Type u_1} (ds : State W) (p : W → Prop) : ¬DiscourseState.IsStable (assert ds p)

@[simp]

theorem Discourse.Commitment.Table.polarQuestion_cg {W : Type u_1} (ds : State W) (p : W → Prop) : (polarQuestion ds p).cg = ds.cg

@[simp]

theorem Discourse.Commitment.Table.polarQuestion_table {W : Type u_1} (ds : State W) (p : W → Prop) : (polarQuestion ds p).table = { speaker := DiscourseRole.speaker, addressee := DiscourseRole.addressee, mood := Semantics.Mood.IllocutionaryMood.interrogative, alternatives := [p, fun (w : W) => ¬p w] } :: ds.table

@[simp]

theorem Discourse.Commitment.Table.polarQuestion_dc {W : Type u_1} (ds : State W) (p : W → Prop) (a : DiscourseRole) : (polarQuestion ds p).dc a = ds.dc a

theorem Discourse.Commitment.Table.polarQuestion_not_isStable {W : Type u_1} (ds : State W) (p : W → Prop) : ¬DiscourseState.IsStable (polarQuestion ds p)

theorem Discourse.Commitment.Table.accept_after_assert_cg {W : Type u_1} (ds : State W) (p : W → Prop) : (acceptTop (assert ds p)).cg = ds.cg.add p

@[simp]

theorem Discourse.Commitment.Table.empty_dcS {W : Type u_1} : DiscourseState.empty.dcS = []

@[simp]

theorem Discourse.Commitment.Table.empty_dcL {W : Type u_1} : DiscourseState.empty.dcL = []

@[simp]

theorem Discourse.Commitment.Table.assert_dcS {W : Type u_1} (ds : State W) (p : W → Prop) : DiscourseState.dcS (assert ds p) = p :: DiscourseState.dcS ds

@[simp]

theorem Discourse.Commitment.Table.assert_dcL {W : Type u_1} (ds : State W) (p : W → Prop) : DiscourseState.dcL (assert ds p) = DiscourseState.dcL ds

@[simp]

theorem Discourse.Commitment.Table.assert_cgPropositions {W : Type u_1} (ds : State W) (p : W → Prop) : DiscourseState.cgPropositions (assert ds p) = DiscourseState.cgPropositions ds

@[simp]

theorem Discourse.Commitment.Table.polarQuestion_dcS {W : Type u_1} (ds : State W) (p : W → Prop) : DiscourseState.dcS (polarQuestion ds p) = DiscourseState.dcS ds

@[simp]

theorem Discourse.Commitment.Table.polarQuestion_dcL {W : Type u_1} (ds : State W) (p : W → Prop) : DiscourseState.dcL (polarQuestion ds p) = DiscourseState.dcL ds

@[simp]

theorem Discourse.Commitment.Table.pushItem_dcS {W : Type u_1} (ds : State W) (i : Item DiscourseRole W) : (DiscourseState.pushItem ds i).dcS = DiscourseState.dcS ds

@[simp]

theorem Discourse.Commitment.Table.pushItem_dcL {W : Type u_1} (ds : State W) (i : Item DiscourseRole W) : (DiscourseState.pushItem ds i).dcL = DiscourseState.dcL ds

@[simp]

theorem Discourse.Commitment.Table.accept_after_assert_cgPropositions {W : Type u_1} (ds : State W) (p : W → Prop) : DiscourseState.cgPropositions (acceptTop (assert ds p)) = p :: DiscourseState.cgPropositions ds

After asserting p and accepting it, p reaches the common ground.

@[simp]

theorem Discourse.Commitment.Table.accept_after_assert_dcL {W : Type u_1} (ds : State W) (p : W → Prop) : DiscourseState.dcL (acceptTop (assert ds p)) = p :: DiscourseState.dcL ds

Acceptance adds p to the addressee's commitments.

@[simp]

theorem Discourse.Commitment.Table.accept_after_assert_dcS {W : Type u_1} (ds : State W) (p : W → Prop) : DiscourseState.dcS (acceptTop (assert ds p)) = p :: DiscourseState.dcS ds

The speaker's assertion commitment survives acceptance.

@[simp]

theorem Discourse.Commitment.Table.accept_after_assert_table {W : Type u_1} (ds : State W) (p : W → Prop) : (acceptTop (assert ds p)).table = ds.table

After acceptance the table returns to its pre-assertion state.