Discourse Goals and Plans

@cite{bratman-1987} @cite{portner-2004} @cite{roberts-2023}

The interlocutors' publicly evident goals, plans, and priorities — the G component of @cite{roberts-2023}'s scoreboard K = ⟨I, M, ≺, CG, QUD, G⟩.

@cite{bratman-1987}: intentions are commitments to action, organized hierarchically into plans. Goals subserve other goals, and an agent's priorities induce a partial order over them.

@cite{portner-2004}'s ToDo list is a special case: an unstructured set of properties the addressee is committed to realizing. The present formalization follows @cite{roberts-2023} in giving G richer internal structure — conditional goals with priority ordering — while remaining compatible with Portner's interface (a GoalSet projects to a flat property list).

Key Design Choices

1. Goals are conditional: realized only when applicable circumstances obtain (@cite{roberts-2023} §2.1.1). We represent the condition as a proposition (the modal base propositions that must hold).
2. Goals carry priority: a natural number where lower = higher priority. @cite{roberts-2023}: "i's priorities are reflected in additional structure over G_i."
3. Goal sets are per-agent: G = {G_i | i ∈ I}, one set per interlocutor.

structure Core.Discourse.Goal (W : Type u_2) : Type u_2

A single goal: a proposition the agent is committed to realizing, conditional on certain circumstances obtaining.

@cite{roberts-2023} §2.1.1: "for all g ∈ G_i, g is a conditional goal, its presence in G_i representing i's intention to achieve the goal should certain conditions obtain in the actual world at some future time t' > t."

• content : W → Prop

  The content: what the agent aims to bring about

• condition : W → Prop

  The condition: circumstances under which this goal is active. λ _ => True for unconditional goals.

• priority : ℕ

  Priority level: 0 = highest priority. @cite{roberts-2023}: goals are hierarchically organized to reflect plans and priorities.

@[implicit_reducible]

instance Core.Discourse.instInhabitedGoal {a✝ : Type u_2} : Inhabited (Goal a✝)

Equations

• Core.Discourse.instInhabitedGoal = { default := Core.Discourse.instInhabitedGoal.default }

def Core.Discourse.instInhabitedGoal.default {a✝ : Type u_2} : Goal a✝

Equations

• Core.Discourse.instInhabitedGoal.default = { content := default, condition := default, priority := default }

structure Core.Discourse.GoalSet (W : Type u_2) : Type u_2

An agent's goal set: the publicly evident goals, plans, and priorities.

@cite{roberts-2023} §2.1.1: "G_i is the set of i's evident goals, including those which i is publicly committed at t to trying to realize." Goals are organized to reflect plans and priorities.

• goals : List (Goal W)

  The goals, ordered by priority (lower index = mentioned earlier, not necessarily higher priority — use Goal.priority for ranking).

@[implicit_reducible]

instance Core.Discourse.instInhabitedGoalSet {a✝ : Type u_2} : Inhabited (GoalSet a✝)

Equations

• Core.Discourse.instInhabitedGoalSet = { default := Core.Discourse.instInhabitedGoalSet.default }

def Core.Discourse.instInhabitedGoalSet.default {a✝ : Type u_2} : GoalSet a✝

Equations

• Core.Discourse.instInhabitedGoalSet.default = { goals := default }

def Core.Discourse.GoalSet.empty {W : Type u_1} : GoalSet W

The empty goal set.

Equations

• Core.Discourse.GoalSet.empty = { }

@[simp]

theorem Core.Discourse.GoalSet.empty_goals {W : Type u_1} : empty.goals = []

def Core.Discourse.GoalSet.add {W : Type u_1} (gs : GoalSet W) (g : Goal W) : GoalSet W

Add a goal to the set.

Equations

• gs.add g = { goals := g :: gs.goals }

@[simp]

theorem Core.Discourse.GoalSet.add_goals {W : Type u_1} (gs : GoalSet W) (g : Goal W) : (gs.add g).goals = g :: gs.goals

def Core.Discourse.GoalSet.addSimple {W : Type u_1} (gs : GoalSet W) (content : W → Prop) (priority : ℕ := 0) : GoalSet W

Add an unconditional goal with given priority.

Equations

• gs.addSimple content priority = gs.add { content := content, priority := priority }

def Core.Discourse.GoalSet.remove {W : Type u_1} (gs : GoalSet W) (shouldRemove : Goal W → Bool) : GoalSet W

Remove goals whose content matches a predicate (e.g., realized or abandoned).

Equations

• gs.remove shouldRemove = { goals := List.filter (fun (g : Core.Discourse.Goal W) => !shouldRemove g) gs.goals }

@[simp]

theorem Core.Discourse.GoalSet.remove_goals {W : Type u_1} (gs : GoalSet W) (f : Goal W → Bool) : (gs.remove f).goals = List.filter (fun (g : Goal W) => !f g) gs.goals

noncomputable def Core.Discourse.GoalSet.activeGoals {W : Type u_1} (gs : GoalSet W) (w : W) : List (Goal W)

Goals active in circumstance w (condition satisfied).

Equations

• gs.activeGoals w = List.filter (fun (g : Core.Discourse.Goal W) => decide (g.condition w)) gs.goals

@[simp]

theorem Core.Discourse.GoalSet.activeGoals_empty {W : Type u_1} (w : W) : empty.activeGoals w = []

theorem Core.Discourse.GoalSet.mem_activeGoals_iff {W : Type u_1} (gs : GoalSet W) (w : W) (g : Goal W) : g ∈ gs.activeGoals w ↔ g ∈ gs.goals ∧ g.condition w

noncomputable def Core.Discourse.GoalSet.activeContents {W : Type u_1} (gs : GoalSet W) (w : W) : List (W → Prop)

Active goal contents at w, sorted by priority (ascending = most important first).

Equations

• gs.activeContents w = List.map Core.Discourse.Goal.content ((gs.activeGoals w).mergeSort fun (g₁ g₂ : Core.Discourse.Goal W) => decide (g₁.priority ≤ g₂.priority))

def Core.Discourse.GoalSet.toPropertyList {W : Type u_1} (gs : GoalSet W) : List (W → Prop)

Project to a flat list of contents (@cite{portner-2004} ToDo list interface).

Equations

• gs.toPropertyList = List.map Core.Discourse.Goal.content gs.goals

@[simp]

theorem Core.Discourse.GoalSet.toPropertyList_empty {W : Type u_1} : empty.toPropertyList = []

@[simp]

theorem Core.Discourse.GoalSet.toPropertyList_add {W : Type u_1} (gs : GoalSet W) (g : Goal W) : (gs.add g).toPropertyList = g.content :: gs.toPropertyList

def Core.Discourse.GoalSet.isEmpty {W : Type u_1} (gs : GoalSet W) : Bool

Whether the goal set is empty.

Equations

• gs.isEmpty = gs.goals.isEmpty

@[simp]

theorem Core.Discourse.GoalSet.empty_isEmpty {W : Type u_1} : empty.isEmpty = true

theorem Core.Discourse.GoalSet.isEmpty_iff {W : Type u_1} (gs : GoalSet W) : gs.isEmpty = true ↔ gs.goals = []

def Core.Discourse.GoalSet.size {W : Type u_1} (gs : GoalSet W) : ℕ

Number of goals.

Equations

• gs.size = gs.goals.length

@[simp]

theorem Core.Discourse.GoalSet.size_eq {W : Type u_1} (gs : GoalSet W) : gs.size = gs.goals.length

@[simp]

theorem Core.Discourse.GoalSet.empty_size {W : Type u_1} : empty.size = 0

@[simp]

theorem Core.Discourse.GoalSet.add_size {W : Type u_1} (gs : GoalSet W) (g : Goal W) : (gs.add g).size = gs.size + 1