Documentation

Linglib.Theories.Dialogue.KOS.CooperInfoState

KOS-TIS ↔ Cooper-2023-InfoState Genealogy #

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

A genuine cross-framework bridge: @cite{cooper-2023}'s InfoState (§2.6) is a simplified successor to @cite{ginzburg-2012}'s TIS. The projection tisToInfoState makes the simplification explicit by forgetting QUD, Pending, and genre information.

This is not a TTR-typed instantiation file — that's the sibling KOS/Austinian.lean. This file is anchored on the post-2012 framework comparison: a chronologically-later author (Cooper 2023) proposing a slimmed-down successor to a chronologically-earlier formalism (Ginzburg 2012). The projection witnesses that Cooper's representation is recoverable from Ginzburg's by quotient.

Correspondence (tisToInfoState) #

TIS (Ginzburg 2012)InfoState (Cooper 2023)
priv.agendaagenda
dgb.moves.getLast?latestUtterance
dgb.factscommitments
dgb.qud(not represented)
dgb.pending(not represented)
priv.genre(not represented)

The deletions are exactly what @cite{cooper-2023} drops to make TTR dialogue tractable for incremental processing.

source
def Dialogue.KOS.CooperInfoState.tisToInfoState {P : Type u_1} {QContent : Type u_2} {Fact Cont SignT : Type} (tis : TIS P Fact QContent Cont) (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.
Instances For
    source
    theorem Dialogue.KOS.CooperInfoState.tisToInfoState_commitments {P : Type u_1} {QContent : Type u_2} {Fact Cont SignT : Type} (tis : TIS P Fact QContent Cont) (f : IllocMove Fact QContent → SignT) :
    (tisToInfoState tis f).commitments = tis.dgb.facts

    The projection preserves commitments (= FACTS).

    source
    theorem Dialogue.KOS.CooperInfoState.tisToInfoState_agenda {P : Type u_1} {QContent : Type u_2} {Fact Cont SignT : Type} (tis : TIS P Fact QContent Cont) (f : IllocMove Fact QContent → SignT) :
    (tisToInfoState tis f).agenda = List.map f tis.priv.agenda

    The projection preserves the agenda map.

    source
    theorem Dialogue.KOS.CooperInfoState.tisToInfoState_latest {P : Type u_1} {QContent : Type u_2} {Fact Cont SignT : Type} (tis : TIS P Fact QContent Cont) (f : IllocMove Fact QContent → SignT) :
    (tisToInfoState tis f).latestUtterance = Option.map f tis.dgb.latestMove

    The projection preserves the latest utterance.