Basic Question Types

Core types for question semantics shared across theoretical approaches.

@[reducible, inline]

abbrev Semantics.Questions.Question (W : Type u_1) : Type u_1

Partition-based question: list of mutually exclusive proposition cells.

Equations

• Semantics.Questions.Question W = List (W → Bool)

@[reducible, inline]

abbrev Semantics.Questions.Answer (W : Type u_1) : Type u_1

Answer: proposition as characteristic function on worlds.

Equations

• Semantics.Questions.Answer W = (W → Bool)

@[reducible, inline]

abbrev Semantics.Questions.Cell (W : Type u_1) : Type u_1

Cell in a question partition.

Equations

• Semantics.Questions.Cell W = (W → Bool)

def Semantics.Questions.trivialQuestion {W : Type u_1} : Question W

Equations

• Semantics.Questions.trivialQuestion = [fun (x : W) => true]

def Semantics.Questions.exactQuestion {W : Type u_1} [DecidableEq W] (worlds : List W) : Question W

Equations

• Semantics.Questions.exactQuestion worlds = List.map (fun (w v : W) => w == v) worlds

def Semantics.Questions.numCells {W : Type u_1} (q : Question W) : ℕ

Equations

• Semantics.Questions.numCells q = List.length q

def Semantics.Questions.consistentWith {W : Type u_1} (p : Answer W) (cell : Cell W) (worlds : List W) : Bool

Equations

• Semantics.Questions.consistentWith p cell worlds = worlds.any fun (w : W) => p w && cell w

def Semantics.Questions.cellOf {W : Type u_1} (q : Question W) (w : W) : Option (Cell W)

Equations

• Semantics.Questions.cellOf q w = List.find? (fun (cell : Semantics.Questions.Cell W) => cell w) q

def Semantics.Questions.filterWorlds {W : Type u_1} (worlds : List W) (p : W → Bool) : List W

Equations

• Semantics.Questions.filterWorlds worlds p = List.filter p worlds

def Semantics.Questions.questionProduct {W : Type u_1} (q1 q2 : Question W) : Question W

Product of two questions: cells are intersections.

Equations

• Semantics.Questions.questionProduct q1 q2 = List.flatMap (fun (c1 : W → Bool) => List.map (fun (c2 : W → Bool) (w : W) => c1 w && c2 w) q2) q1

instance Semantics.Questions.instMulQuestion {W : Type u_1} : Mul (Question W)

Equations

• Semantics.Questions.instMulQuestion = { mul := Semantics.Questions.questionProduct }

def Semantics.Questions.questionJoin {W : Type u_1} (q1 q2 : Question W) (worlds : List W) : Question W

Join of two questions: coarsest refinement of both.

Equations

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

def Semantics.Questions.answers {W : Type u_1} (p : Answer W) (q : Question W) (worlds : List W) : Bool

Equations

• Semantics.Questions.answers p q worlds = List.any q fun (cell : W → Bool) => worlds.all fun (w : W) => decide (p w = true → cell w = true)

def Semantics.Questions.partiallyAnswers {W : Type u_1} (p : Answer W) (q : Question W) (worlds : List W) : Bool

Equations

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

def Semantics.Questions.completelyAnswers {W : Type u_1} (p : Answer W) (q : Question W) (worlds : List W) : Bool

Equations

• Semantics.Questions.completelyAnswers p q worlds = ((List.filter (fun (cell : W → Bool) => worlds.any fun (w : W) => p w && cell w) q).length == 1)

def Semantics.Questions.pnot {W : Type u_1} (p : W → Bool) : W → Bool

Equations

• Semantics.Questions.pnot p w = !p w

def Semantics.Questions.pand {W : Type u_1} (p q : W → Bool) : W → Bool

Equations

• Semantics.Questions.pand p q w = (p w && q w)

def Semantics.Questions.por {W : Type u_1} (p q : W → Bool) : W → Bool

Equations

• Semantics.Questions.por p q w = (p w || q w)

def Semantics.Questions.pimplies {W : Type u_1} (p q : W → Bool) : W → Bool

Equations

• Semantics.Questions.pimplies p q w = (!p w || q w)

def Semantics.Questions.entails {W : Type u_1} (p q : W → Bool) (worlds : List W) : Bool

Equations

• Semantics.Questions.entails p q worlds = worlds.all fun (w : W) => !p w || q w