KOS: Worked Examples

[Gin12] Ch. 4 ex. 66, ex. 68

Public worked examples demonstrating the substrate operations on concrete inputs. Earlier these lived inline in Gameboard/Rules.lean as private defs; they are public here so consumers (study files, the TTR-typed counterpart in Austinian.lean) can reference them.

Sections

• §1. Inquiry cycle (Bo): A asks "Is Bo here?", B asserts, A accepts
• §2. Check/Confirm cycle: A asserts, B checks, A confirms
• §3. AssertWithQUD cycle: full Assert protocol on the Bo example
• §4. Partition-based answerhood (RainWorld): typed propositions resolving a partition QUD via PropResolvesQUD

The string-based examples use a generic DecidableSupport String String instance (string equality as answerhood), and instantiate Cont = String for utterance content (since the worked examples don't exercise the LocProp Pending pipeline). See Austinian.lean for the TTR-typed counterpart over BCheckableAustinian S and TTRQuestionB R.

@[implicit_reducible]

instance Ginzburg2012.Examples.instDecidableSupportString : Question.DecidableSupport String String

String-based answerhood: a fact resolves a question if they match.

Equations

• Ginzburg2012.Examples.instDecidableSupportString = { supports := fun (fact question : String) => fact = question, decSupports := fun (a b : String) => decEq a b }

def Ginzburg2012.Examples.tis₀ : Discourse.Gameboard.TIS String String String String

Start: empty TIS.

Equations

• Ginzburg2012.Examples.tis₀ = Discourse.Gameboard.TIS.initial

def Ginzburg2012.Examples.tis₁ : Discourse.Gameboard.TIS String String String String

Step 1: A asks "Is Bo here?"

Equations

• Ginzburg2012.Examples.tis₁ = Ginzburg2012.Examples.tis₀.ask "Bo is here"

def Ginzburg2012.Examples.tis₂ : Discourse.Gameboard.TIS String String String String

Step 2: B asserts "Bo is here."

Equations

• Ginzburg2012.Examples.tis₂ = Ginzburg2012.Examples.tis₁.assertRule "Bo is here"

def Ginzburg2012.Examples.tis₃ : Discourse.Gameboard.TIS String String String String

Step 3: A accepts B's assertion.

Equations

• Ginzburg2012.Examples.tis₃ = Ginzburg2012.Examples.tis₂.accept "Bo is here"

theorem Ginzburg2012.Examples.inquiry_step1_qud : tis₁.dgb.qud = [Discourse.Gameboard.InfoStruc.fromQuestion "Bo is here"]

After Ask, QUD contains the question (wrapped as an InfoStruc with no FECs).

theorem Ginzburg2012.Examples.inquiry_step1_facts : tis₁.dgb.facts = []

After Ask, FACTS are unchanged.

theorem Ginzburg2012.Examples.inquiry_step1_moves : tis₁.dgb.moves = [Discourse.Gameboard.IllocMove.ask "Bo is here"]

After Ask, the move is recorded.

theorem Ginzburg2012.Examples.inquiry_step2_has_fact : "Bo is here" ∈ tis₂.dgb.facts

After Assert, the fact is in FACTS.

theorem Ginzburg2012.Examples.inquiry_step2_qud_empty : tis₂.dgb.qud = []

After Assert, QUD is empty (the question was resolved).

theorem Ginzburg2012.Examples.inquiry_step3_facts : tis₃.dgb.facts = ["Bo is here", "Bo is here"]

After Accept, the fact appears twice (once from assert, once from accept).

theorem Ginzburg2012.Examples.inquiry_cycle_moves : tis₃.dgb.moves = [Discourse.Gameboard.IllocMove.ask "Bo is here", Discourse.Gameboard.IllocMove.assert "Bo is here", Discourse.Gameboard.IllocMove.accept "Bo is here"]

Moves accumulate through the inquiry cycle.

def Ginzburg2012.Examples.checkTIS₀ : Discourse.Gameboard.TIS String String String String

A(1): Bo is in Essen. (Assert)

Equations

• Ginzburg2012.Examples.checkTIS₀ = Discourse.Gameboard.TIS.initial

def Ginzburg2012.Examples.checkTIS₁ : Discourse.Gameboard.TIS String String String String

Equations

• Ginzburg2012.Examples.checkTIS₁ = Ginzburg2012.Examples.checkTIS₀.assertRule "Bo is in Essen"

def Ginzburg2012.Examples.checkTIS₂ : Discourse.Gameboard.TIS String String String String

B(1b): Is he? (Check)

Equations

• Ginzburg2012.Examples.checkTIS₂ = Ginzburg2012.Examples.checkTIS₁.check "Bo is in Essen" "Bo is in Essen"

def Ginzburg2012.Examples.checkTIS₃ : Discourse.Gameboard.TIS String String String String

A(2): Confirm.

Equations

• Ginzburg2012.Examples.checkTIS₃ = Ginzburg2012.Examples.checkTIS₂.confirm "Bo is in Essen"

theorem Ginzburg2012.Examples.check_pushes : checkTIS₂.dgb.qud = [Discourse.Gameboard.InfoStruc.fromQuestion "Bo is in Essen"]

After Check, QUD has the polar question.

theorem Ginzburg2012.Examples.confirm_resolves : checkTIS₃.dgb.qud = []

After Confirm, the fact is in FACTS and QUD is resolved.

def Ginzburg2012.Examples.awq₀ : Discourse.Gameboard.TIS String String String String

Full inquiry cycle using the Ginzburg 2012 Assert protocol.

A: "Is Bo here?" (Ask) B: "Bo is here." (AssertWithQUD — pushes About("Bo is here") onto QUD) A: accepts (Accept + factUpdateQudDowndate)

Equations

• Ginzburg2012.Examples.awq₀ = Discourse.Gameboard.TIS.initial

def Ginzburg2012.Examples.awq₁ : Discourse.Gameboard.TIS String String String String

Equations

• Ginzburg2012.Examples.awq₁ = Ginzburg2012.Examples.awq₀.ask "Bo is here"

def Ginzburg2012.Examples.awq₂ : Discourse.Gameboard.TIS String String String String

Equations

• Ginzburg2012.Examples.awq₂ = Ginzburg2012.Examples.awq₁.assertWithQUD "Bo is here" "Bo is here"

theorem Ginzburg2012.Examples.awq_resolves_original_question : awq₂.dgb.qud = []

After assertWithQUD, the question from Ask is resolved (fact matches).

theorem Ginzburg2012.Examples.awq_has_fact : "Bo is here" ∈ awq₂.dgb.facts

The fact is in FACTS after assertWithQUD.

inductive Ginzburg2012.Examples.RainWorld : Type

Three-world scenario: is it raining?

• sunny : RainWorld
• rainy : RainWorld
• cloudy : RainWorld

@[implicit_reducible]

instance Ginzburg2012.Examples.instReprRainWorld : Repr RainWorld

Equations

• Ginzburg2012.Examples.instReprRainWorld = { reprPrec := Ginzburg2012.Examples.instReprRainWorld.repr }

def Ginzburg2012.Examples.instReprRainWorld.repr : RainWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Ginzburg2012.Examples.instDecidableEqRainWorld : DecidableEq RainWorld

Equations

• Ginzburg2012.Examples.instDecidableEqRainWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.Examples.isRainingQ : QUD RainWorld

"Is it raining?" — partition into rainy vs non-rainy.

Equations

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

inductive Ginzburg2012.Examples.RainProp : Type

A tagged proposition for the rain example: pairs a Set RainWorld with a tag enabling decidable equality and Bool-valued resolution.

• raining : RainProp
• sunny : RainProp

@[implicit_reducible]

instance Ginzburg2012.Examples.instDecidableEqRainProp : DecidableEq RainProp

Equations

• Ginzburg2012.Examples.instDecidableEqRainProp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.Examples.instReprRainProp.repr : RainProp → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Ginzburg2012.Examples.instReprRainProp : Repr RainProp

Equations

• Ginzburg2012.Examples.instReprRainProp = { reprPrec := Ginzburg2012.Examples.instReprRainProp.repr }

def Ginzburg2012.Examples.RainProp.toProp : RainProp → Set RainWorld

Equations

• Ginzburg2012.Examples.RainProp.raining.toProp = fun (w : Ginzburg2012.Examples.RainWorld) => w = Ginzburg2012.Examples.RainWorld.rainy
• Ginzburg2012.Examples.RainProp.sunny.toProp = fun (w : Ginzburg2012.Examples.RainWorld) => w = Ginzburg2012.Examples.RainWorld.sunny

@[implicit_reducible]

instance Ginzburg2012.Examples.instDecidablePredRainWorldToProp (rp : RainProp) : DecidablePred rp.toProp

Equations

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

def Ginzburg2012.Examples.itIsRaining : Set RainWorld

"It is raining" — true only in the rainy world.

Equations

• Ginzburg2012.Examples.itIsRaining w = (w = Ginzburg2012.Examples.RainWorld.rainy)

@[implicit_reducible]

instance Ginzburg2012.Examples.instDecidablePredRainWorldItIsRaining : DecidablePred itIsRaining

Equations

• Ginzburg2012.Examples.instDecidablePredRainWorldItIsRaining w = id inferInstance

def Ginzburg2012.Examples.itIsSunny : Set RainWorld

"It is sunny" — true only in the sunny world.

Equations

• Ginzburg2012.Examples.itIsSunny w = (w = Ginzburg2012.Examples.RainWorld.sunny)

@[implicit_reducible]

instance Ginzburg2012.Examples.instDecidablePredRainWorldItIsSunny : DecidablePred itIsSunny

Equations

• Ginzburg2012.Examples.instDecidablePredRainWorldItIsSunny w = id inferInstance

def Ginzburg2012.Examples.rainWorlds : List RainWorld

Equations

• Ginzburg2012.Examples.rainWorlds = [Ginzburg2012.Examples.RainWorld.sunny, Ginzburg2012.Examples.RainWorld.rainy, Ginzburg2012.Examples.RainWorld.cloudy]

theorem Ginzburg2012.Examples.raining_resolves_raining : Discourse.Gameboard.PropResolvesQUD rainWorlds itIsRaining isRainingQ

"It is raining" resolves "Is it raining?"

theorem Ginzburg2012.Examples.sunny_resolves_raining : Discourse.Gameboard.PropResolvesQUD rainWorlds itIsSunny isRainingQ

"It is sunny" also resolves "Is it raining?"

def Ginzburg2012.Examples.rainTIS₀ : Discourse.Gameboard.TIS String RainProp (QUD RainWorld) Unit

Full inquiry cycle with partition-based support (via RainProp tags).

Equations

• Ginzburg2012.Examples.rainTIS₀ = Discourse.Gameboard.TIS.initial

@[implicit_reducible]

instance Ginzburg2012.Examples.rainSupport : Question.DecidableSupport RainProp (QUD RainWorld)

Equations

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

def Ginzburg2012.Examples.rainTIS₁ : Discourse.Gameboard.TIS String RainProp (QUD RainWorld) Unit

Equations

• Ginzburg2012.Examples.rainTIS₁ = Ginzburg2012.Examples.rainTIS₀.ask Ginzburg2012.Examples.isRainingQ

theorem Ginzburg2012.Examples.rain_ask_qud : rainTIS₁.dgb.qud = [Discourse.Gameboard.InfoStruc.fromQuestion isRainingQ]

After asking, QUD has the partition question.

def Ginzburg2012.Examples.rainTIS₂ : Discourse.Gameboard.TIS String RainProp (QUD RainWorld) Unit

Equations

• Ginzburg2012.Examples.rainTIS₂ = Ginzburg2012.Examples.rainTIS₁.assertRule Ginzburg2012.Examples.RainProp.raining

theorem Ginzburg2012.Examples.rain_assert_resolves : rainTIS₂.dgb.qud = []

After asserting "It is raining", QUD is empty (resolved).