KOS ↔ TTR Bridge

@cite{ginzburg-2012} @cite{cooper-2023}

Connects the KOS dialogue framework (DGB, TIS, conversational rules) to TTR's type-theoretic content representations (CheckableAustinian propositions, TTRQuestions). This closes the loop between:

• Theories/Pragmatics/Dialogue/KOS/ — dialogue structure
• Theories/Semantics/TypeTheoretic/ — content types

Key Instantiations

1. DGB with Austinian facts: DGB String (BCheckableAustinian S) (TTRQuestion R)
2. Answerhood: a BCheckableAustinian S resolves a TTRQuestion R when the situation witnesses the question body
3. TIS ↔ InfoState genealogy: TIS (Ginzburg 2012) is a refinement of InfoState (Cooper 2023) — the public/private split is a record extension

structure Theories.Pragmatics.Dialogue.KOS.TTRBridge.TTRQuestionB (R : Type) : Type

A Bool-valued TTR question: stays in Type 0 for DGB compatibility.

TTRQuestion R (from TypeTheoretic/Discourse.lean) has body : R → Type, placing it in Type 1. Since DGB requires QContent : Type, we provide a decidable variant where the question body is Bool-valued.

The correspondence: TTRQuestionB R is to TTRQuestion R as BProp W is to Prop' W — the decidable/computable variant of the same concept.

• body : R → Bool

  The decidable question body

• name : String

  Name for display

def Theories.Pragmatics.Dialogue.KOS.TTRBridge.TTRQuestionB.polar (p : Bool) (name : String := "") : TTRQuestionB Unit

A polar Bool-question: is P true?

Equations

• Theories.Pragmatics.Dialogue.KOS.TTRBridge.TTRQuestionB.polar p name = { body := fun (x : Unit) => p, name := name }

def Theories.Pragmatics.Dialogue.KOS.TTRBridge.TTRQuestionB.wh {R : Type} (body : R → Bool) (name : String := "") : TTRQuestionB R

A wh-question: which x satisfies P?

Equations

• Theories.Pragmatics.Dialogue.KOS.TTRBridge.TTRQuestionB.wh body name = { body := body, name := name }

def Theories.Pragmatics.Dialogue.KOS.TTRBridge.TTRQuestionB.isResolved {R : Type} (q : TTRQuestionB R) (domain : List R) : Bool

A Bool-question is resolved when some element satisfies the body.

Equations

• q.isResolved domain = domain.any q.body

@[reducible, inline]

abbrev Theories.Pragmatics.Dialogue.KOS.TTRBridge.AustinianDGB (S R : Type) : Type

A DGB whose facts are checkable Austinian propositions and whose QUD entries are Bool-valued TTR questions.

@cite{ginzburg-2012} Ch. 4: FACTS is a set of Austinian propositions [sit = s, sit-type = T]. QUD is a poset of questions.

Equations

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

@[reducible, inline]

abbrev Theories.Pragmatics.Dialogue.KOS.TTRBridge.AustinianTIS (S R : Type) : Type

A TIS with Austinian content types.

Equations

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

instance Theories.Pragmatics.Dialogue.KOS.TTRBridge.austinianAnswerhood (S : Type) : Answerhood (Semantics.TypeTheoretic.BCheckableAustinian S) (TTRQuestionB S)

A BCheckableAustinian S resolves a TTRQuestionB S when the Austinian proposition is true at a situation that satisfies the question body.

@cite{ginzburg-2012} Ch. 4: "q is resolved relative to a DGB dgb iff the FACTS in dgb contextually entail an answer to q."

For a fact ⟨s, T⟩ and question Q: the fact resolves Q when T(s) is true AND Q.body(s) is true — the situation that makes the fact true also answers the question.

Equations

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

The TIS → InfoState Projection

@cite{cooper-2023}'s InfoState (§2.6) is a simplified version of @cite{ginzburg-2012}'s TIS. The correspondence:

TIS (Ginzburg 2012)	InfoState (Cooper 2023)
private_.agenda	agenda
dgb.moves.getLast?	latestUtterance
dgb.facts	commitments
dgb.qud	(not represented)
dgb.pending	(not represented)
private_.genre	(not represented)

TIS is a record extension of InfoState: it adds QUD, Pending, genre, and separates public from private.

def Theories.Pragmatics.Dialogue.KOS.TTRBridge.tisToInfoState {P Fact QContent SignT : Type} (tis : TIS P Fact QContent) (moveToSign : IllocMove Fact QContent → SignT) : Semantics.TypeTheoretic.InfoState SignT (List Fact)

Project a TIS to a Cooper-style InfoState.

The projection loses QUD, Pending, and genre information — these are the components that @cite{ginzburg-2012} adds beyond @cite{cooper-2023}.

Equations

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

theorem Theories.Pragmatics.Dialogue.KOS.TTRBridge.tisToInfoState_commitments {P Fact QContent SignT : Type} (tis : TIS P Fact QContent) (f : IllocMove Fact QContent → SignT) : (tisToInfoState tis f).commitments = tis.dgb.facts

The projection preserves commitments (= FACTS).

inductive Theories.Pragmatics.Dialogue.KOS.TTRBridge.Weather : Type

A simple situation type for the example.

• sunny : Weather
• rainy : Weather
• cloudy : Weather

instance Theories.Pragmatics.Dialogue.KOS.TTRBridge.instReprWeather : Repr Weather

Equations

• Theories.Pragmatics.Dialogue.KOS.TTRBridge.instReprWeather = { reprPrec := Theories.Pragmatics.Dialogue.KOS.TTRBridge.instReprWeather.repr }

def Theories.Pragmatics.Dialogue.KOS.TTRBridge.instReprWeather.repr : Weather → ℕ → Std.Format

Equations

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

instance Theories.Pragmatics.Dialogue.KOS.TTRBridge.instDecidableEqWeather : DecidableEq Weather

Equations

• Theories.Pragmatics.Dialogue.KOS.TTRBridge.instDecidableEqWeather x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Theories.Pragmatics.Dialogue.KOS.TTRBridge.instBEqWeather : BEq Weather

Equations

• Theories.Pragmatics.Dialogue.KOS.TTRBridge.instBEqWeather = { beq := Theories.Pragmatics.Dialogue.KOS.TTRBridge.instBEqWeather.beq }

def Theories.Pragmatics.Dialogue.KOS.TTRBridge.instBEqWeather.beq : Weather → Weather → Bool

Equations

• Theories.Pragmatics.Dialogue.KOS.TTRBridge.instBEqWeather.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Theories.Pragmatics.Dialogue.KOS.TTRBridge.itIsRaining : Semantics.TypeTheoretic.BCheckableAustinian Weather

"It is raining" as an Austinian proposition: situation = rainy, type = isRainy.

Equations

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

theorem Theories.Pragmatics.Dialogue.KOS.TTRBridge.itIsRaining_true : itIsRaining.isTrue = true

The Austinian proposition "it is raining" is true (rainy satisfies isRainy).

def Theories.Pragmatics.Dialogue.KOS.TTRBridge.isItRaining : TTRQuestionB Weather

"Is it raining?" as a Bool-valued TTR question.

Equations

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

theorem Theories.Pragmatics.Dialogue.KOS.TTRBridge.raining_resolves : Answerhood.resolves itIsRaining isItRaining = true

The fact "it is raining" resolves the question "is it raining?": the situation (rainy) makes both the fact true and the question body true.

def Theories.Pragmatics.Dialogue.KOS.TTRBridge.itIsSunny : Semantics.TypeTheoretic.BCheckableAustinian Weather

"It is sunny" — an Austinian proposition that does NOT resolve "is it raining?".

Equations

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

theorem Theories.Pragmatics.Dialogue.KOS.TTRBridge.sunny_does_not_resolve_raining : Answerhood.resolves itIsSunny isItRaining = false

A true fact about a different situation does not resolve the raining question.

theorem Theories.Pragmatics.Dialogue.KOS.TTRBridge.atis_ask_qud : Theories.Pragmatics.Dialogue.KOS.TTRBridge.atis₁✝.dgb.qud = [isItRaining]

theorem Theories.Pragmatics.Dialogue.KOS.TTRBridge.atis_assert_resolves : Theories.Pragmatics.Dialogue.KOS.TTRBridge.atis₂✝.dgb.qud = []

theorem Theories.Pragmatics.Dialogue.KOS.TTRBridge.atis_has_fact : itIsRaining ∈ Theories.Pragmatics.Dialogue.KOS.TTRBridge.atis₂✝.dgb.facts

The fact is in FACTS after assertion.