Documentation

Linglib.Core.Question.Partition.Constructors

Partition-Question Constructors #

@cite{groenendijk-stokhof-1984}

@cite{groenendijk-stokhof-1984} partition semantics for questions.

Core Idea #

A question denotes an equivalence relation on worlds:

⟦?x.P(x)⟧ = λw.λv. [λx.P(w)(x) = λx.P(v)(x)]

Two worlds are equivalent iff the predicate has the same extension in both. This induces a partition of logical space.

Architecture #

GSQuestion is an abbreviation for QUD. All partition lattice operations (refinement, coarsening, cells) are defined in Core/Question/Partition/ and apply to any equivalence-relation partition, not just question denotations.

This module provides question-specific constructors (polarQuestion, whQuestion, alternativeQuestion, etc.) and the legacy GSQuestion namespace alias.

source
@[reducible, inline]
abbrev Semantics.Questions.GSQuestion (W : Type u_1) :
Type u_1

A G&S-style question is exactly a QUD: an equivalence relation on worlds.

Two worlds are equivalent iff they give the same answer to the question. This induces a partition of the world space.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Semantics.Questions.GSQuestion.equiv {W : Type u_1} (q : GSQuestion W) (a b : W) :
    Bool

    Compatibility accessor: equiv is the same as sameAnswer.

    Equations
    Instances For
      source
      def Semantics.Questions.GSQuestion.«term_⊑_» :
      Lean.TrailingParserDescr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Semantics.Questions.GSQuestion.exact {W : Type u_1} [BEq W] [LawfulBEq W] :
        GSQuestion W

        The finest possible partition (identity). Each world is its own equivalence class. This is the "maximally informative" question.

        Equations
        Instances For
          source
          def Semantics.Questions.GSQuestion.trivial {W : Type u_1} :
          GSQuestion W

          The coarsest partition (all worlds equivalent). Conveys no information. This is the "tautological" question (always answered "yes").

          Equations
          Instances For
            source
            def Semantics.Questions.GSQuestion.ofProject {W : Type u_1} {A : Type} [BEq A] [LawfulBEq A] (f : W → A) :
            GSQuestion W

            Build a question from a projection function. Two worlds are equivalent iff they have the same value under projection.

            Example: ofProject (λ w => w.weather) asks "What's the weather?"

            Equations
            Instances For
              source
              def Semantics.Questions.GSQuestion.ofPredicate {W : Type u_1} (p : W → Bool) :
              GSQuestion W

              Build a question from a Boolean predicate (polar question). Partitions into {yes-worlds} and {no-worlds}.

              Equations
              Instances For
                source
                def Semantics.Questions.GSQuestion.toQUD {W : Type u_1} (q : GSQuestion W) :
                QUD W

                Convert to a Core.QUD (identity since GSQuestion = QUD).

                Equations
                Instances For
                  source
                  def Semantics.Questions.GSQuestion.ofQUD {W : Type u_1} (qud : QUD W) :
                  GSQuestion W

                  Convert from a QUD (identity since GSQuestion = QUD).

                  Equations
                  Instances For
                    source
                    theorem Semantics.Questions.GSQuestion.toQUD_ofQUD_roundtrip {W : Type u_1} (q : GSQuestion W) :
                    ofQUD q.toQUD = q
                    source
                    theorem Semantics.Questions.GSQuestion.ofQUD_toQUD_roundtrip {W : Type u_1} (qud : QUD W) :
                    (ofQUD qud).toQUD = qud
                    source
                    def Semantics.Questions.polarQuestion {W : Type u_1} (p : W → Bool) :
                    GSQuestion W

                    A yes/no (polar) question: partitions into {yes-worlds} and {no-worlds}.

                    Example: "Is it raining?" partitions worlds into rainy and not-rainy.

                    Equations
                    Instances For
                      source
                      theorem Semantics.Questions.polarQuestion_eq_ofProject {W : Type u_1} (p : W → Bool) :
                      polarQuestion p = GSQuestion.ofProject p

                      A polar question is equivalent to projecting onto Bool.

                      source
                      def Semantics.Questions.whQuestion {W A : Type} [BEq A] [LawfulBEq A] (f : W → A) :
                      GSQuestion W

                      A wh-question asks for the value of some function.

                      Example: "Who came?" = ofProject (λ w => w.guests) Two worlds are equivalent iff they have the same set of guests.

                      Equations
                      Instances For
                        source
                        def Semantics.Questions.alternativeQuestion {W : Type u_1} (alts : List (W → Bool)) :
                        GSQuestion W

                        An alternative question: which of these propositions is true?

                        Example: "Did John or Mary come?"

                        Equations
                        Instances For
                          source
                          theorem Semantics.Questions.polar_exhaustive {W : Type u_1} [DecidableEq W] (p : W → Bool) (w : W) :
                          QUD.numCells (polarQuestion p) [w] ≤ 2

                          The exhaustive interpretation of a polar question is complete: answering requires saying "yes" or "no", not "I don't know".