Questions/LiftedTypes.lean

@cite{barker-shan-2014} @cite{groenendijk-stokhof-1984} @cite{partee-1987} @cite{partee-rooth-1983}

Lifted Question Types (@cite{groenendijk-stokhof-1984}, Chapter VI, Section 6; @cite{partee-rooth-1983}).

The Problem

Coordination of questions poses a type-theoretic puzzle:

• "Who came?" has type ⟨s,⟨s,t⟩⟩ (partition)
• "Who came or who left?" should coordinate two questions

But the disjunction of two equivalence relations is NOT an equivalence relation! If w ~₁ v and v ~₂ u, we don't get w ~₁ u or w ~₂ u.

The Solution: Flexible Types

@cite{partee-rooth-1983} propose:

1. Categories have a basic type plus predictable lifted types
2. Lifting rules are general procedures (not ad hoc)
3. Interpret at minimal type unless higher type is needed
4. Avoid "generalize to worst case"

For questions:

• Core type: Partitions (equivalence relations)
• Lifted type: Sets of properties of questions

Lifting

The lift operation:

lift : GSQuestion W → LiftedQuestion W
lift(Q) = λP. P(Q)

A lifted question is the set of all properties that hold of the underlying question.

Coordination in Lifted Types

Once lifted, coordination is straightforward:

Q₁ ∨ Q₂ = λP. P ∈ Q₁ ∨ P ∈ Q₂ -- property holds of either
Q₁ ∧ Q₂ = λP. P ∈ Q₁ ∧ P ∈ Q₂ -- property holds of both

This avoids the transitivity problem entirely.

Connection to Continuations

Lifted questions form a continuation monad. In Barker & Shan's tower notation, an expression's type is written as a vertical tower:

  C | B
  ─────
    A

Reading counter-clockwise from the bottom: the expression functions locally as A, takes scope over B, and returns C. The flat equivalent is C ⫽ (A ⫽ B).

For questions:

• Core type: GSQuestion W (the A)
• Lifted type: (GSQuestion W → Prop) → Prop (= Cont Prop (GSQuestion W))

Monad Operations

The continuation monad has three key operations:

• pure (= lift): λq. λP. P(q) — wrap a value for any continuation
• bind (>>=): λm. λf. λP. m(λq. f(q)(P)) — sequence scope effects
• run: λm. m(λ_. True) — close off with trivial continuation

Why This Matters for Natural Language

Barker & Shan argue continuations unify:

1. Generalized quantifiers: DPs as (e → t) → t
2. Dynamic semantics: Sentences as context updates
3. Scope displacement: Why quantifiers can outscope their syntactic position

The key insight: expressions denote functions on their own semantic context, enabling non-local effects while maintaining compositional, left-to-right evaluation.

def Semantics.Questions.LiftedTypes.QuestionProperty (W : Type u_1) : Type u_1

A property of questions: something that can be true or false of a GSQuestion.

Examples:

• "resolves decision problem D"
• "has more than 2 cells"
• "refines question Q'"

Equations

• Semantics.Questions.LiftedTypes.QuestionProperty W = (Semantics.Questions.GSQuestion W → Prop)

def Semantics.Questions.LiftedTypes.LiftedQuestion (W : Type u_1) : Type u_1

A lifted question: a set of properties (Montague-style generalized quantifier over questions).

In the Partee & Rooth framework, lifting a question Q produces the set of all properties that Q has:

lift(Q) = {P | P(Q)}

Coordination then works via set operations on properties.

Equations

• Semantics.Questions.LiftedTypes.LiftedQuestion W = (Semantics.Questions.LiftedTypes.QuestionProperty W → Prop)

def Semantics.Questions.LiftedTypes.LiftedQuestion.lift {W : Type u_1} (q : GSQuestion W) : LiftedQuestion W

Lift a core question to the lifted type.

lift(Q) = λP. P(Q)

The lifted question is the characteristic function of Q's properties.

Equations

• Semantics.Questions.LiftedTypes.LiftedQuestion.lift q P = P q

def Semantics.Questions.LiftedTypes.LiftedQuestion.isPrincipal {W : Type u_1} (lq : LiftedQuestion W) : Prop

A lifted question is "principal" if it comes from lifting a core question.

Equations

• lq.isPrincipal = ∃ (q : Semantics.Questions.GSQuestion W), lq = Semantics.Questions.LiftedTypes.LiftedQuestion.lift q

The Continuation Monad

The type LiftedQuestion W = (GSQuestion W → Prop) → Prop is the continuation monad Cont Prop specialized to questions. We provide:

1. pure (alias for lift): the monadic unit
2. bind (>>=): monadic sequencing
3. map: functorial action
4. run: evaluate by closing off the continuation

The monad laws (left/right identity, associativity) hold by construction.

@[reducible, inline]

abbrev Semantics.Questions.LiftedTypes.LiftedQuestion.pure {W : Type u_1} : GSQuestion W → LiftedQuestion W

Pure: alias for lift, emphasizing the monadic structure.

In B&S tower notation, this is the LIFT type-shifter:

  A LIFT B | B
phrase ⟹ phrase
  x []
                    ───
                     x

Semantically: ⟦pure(x)⟧ = λκ.κ(x)

Equations

• Semantics.Questions.LiftedTypes.LiftedQuestion.pure = Semantics.Questions.LiftedTypes.LiftedQuestion.lift

def Semantics.Questions.LiftedTypes.LiftedQuestion.bind {W : Type u_1} (lq : LiftedQuestion W) (f : GSQuestion W → LiftedQuestion W) : LiftedQuestion W

Bind (>>=): monadic sequencing for lifted questions.

Allows a lifted question to "feed into" a function that produces another lifted question, with proper handling of the continuation.

m >>= f = λP. m(λq. f(q)(P))

In B&S terms, this corresponds to the combination schema where the left element's scope effect wraps around the right's result.

Equations

• lq.bind f P = lq fun (q : Semantics.Questions.GSQuestion W) => f q P

def Semantics.Questions.LiftedTypes.LiftedQuestion.map {W : Type u_1} (f : GSQuestion W → GSQuestion W) (lq : LiftedQuestion W) : LiftedQuestion W

Map: functorial action on lifted questions.

Applies a function to the underlying question(s) without changing scope structure.

Equations

• Semantics.Questions.LiftedTypes.LiftedQuestion.map f lq P = lq fun (q : Semantics.Questions.GSQuestion W) => P (f q)

def Semantics.Questions.LiftedTypes.LiftedQuestion.run {W : Type u_1} (lq : LiftedQuestion W) : Prop

Run: evaluate a lifted question by closing off the continuation.

Applies the trivial continuation (constant True), effectively asking "does there exist a question satisfying the lifted question?"

For principal lifted questions, this always returns True. This corresponds to B&S's LOWER when we don't need the value back.

Equations

• lq.run = lq fun (x : Semantics.Questions.GSQuestion W) => True

def Semantics.Questions.LiftedTypes.LiftedQuestion.«term_>>=_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.bind_left_id {W : Type u_1} (q : GSQuestion W) (f : GSQuestion W → LiftedQuestion W) : (pure q).bind f = f q

Left identity: pure q >>= f = f q

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.bind_right_id {W : Type u_1} (lq : LiftedQuestion W) : lq.bind pure = lq

Right identity: m >>= pure = m

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.bind_assoc {W : Type u_1} (lq : LiftedQuestion W) (f g : GSQuestion W → LiftedQuestion W) : (lq.bind f).bind g = lq.bind fun (q : GSQuestion W) => (f q).bind g

Associativity: (m >>= f) >>= g = m >>= (λx. f x >>= g)

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.lift_bind {W : Type u_1} (q : GSQuestion W) (f : GSQuestion W → LiftedQuestion W) : (lift q).bind f = f q

Lift distributes over bind (naturality).

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.map_via_bind {W : Type u_1} (f : GSQuestion W → GSQuestion W) (lq : LiftedQuestion W) : map f lq = lq.bind fun (q : GSQuestion W) => pure (f q)

Map can be defined via bind and pure.

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.run_principal {W : Type u_1} (q : GSQuestion W) : (lift q).run = True

Run of a principal lifted question is True.

def Semantics.Questions.LiftedTypes.LiftedQuestion.disj {W : Type u_1} (lq1 lq2 : LiftedQuestion W) : LiftedQuestion W

Disjunction of lifted questions.

(Q₁ ∨ Q₂)(P) iff P holds of Q₁ or P holds of Q₂.

This is well-defined and doesn't require transitivity!

Equations

• lq1.disj lq2 P = (lq1 P ∨ lq2 P)

def Semantics.Questions.LiftedTypes.LiftedQuestion.conj {W : Type u_1} (lq1 lq2 : LiftedQuestion W) : LiftedQuestion W

Conjunction of lifted questions.

(Q₁ ∧ Q₂)(P) iff P holds of Q₁ and P holds of Q₂.

Equations

• lq1.conj lq2 P = (lq1 P ∧ lq2 P)

def Semantics.Questions.LiftedTypes.LiftedQuestion.disjCore {W : Type u_1} (q1 q2 : GSQuestion W) : LiftedQuestion W

Disjunction of core questions via lifting.

Equations

• Semantics.Questions.LiftedTypes.LiftedQuestion.disjCore q1 q2 = (Semantics.Questions.LiftedTypes.LiftedQuestion.lift q1).disj (Semantics.Questions.LiftedTypes.LiftedQuestion.lift q2)

def Semantics.Questions.LiftedTypes.LiftedQuestion.conjCore {W : Type u_1} (q1 q2 : GSQuestion W) : LiftedQuestion W

Conjunction of core questions via lifting.

Equations

• Semantics.Questions.LiftedTypes.LiftedQuestion.conjCore q1 q2 = (Semantics.Questions.LiftedTypes.LiftedQuestion.lift q1).conj (Semantics.Questions.LiftedTypes.LiftedQuestion.lift q2)

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.disj_bind_left {W : Type u_1} (lq1 lq2 : LiftedQuestion W) (f : GSQuestion W → LiftedQuestion W) : (lq1.disj lq2).bind f = (lq1.bind f).disj (lq2.bind f)

Disjunction distributes over bind from the left.

If we have Q₁ ∨ Q₂ and apply f to each, we get f(Q₁) ∨ f(Q₂).

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.conj_bind_left {W : Type u_1} (lq1 lq2 : LiftedQuestion W) (f : GSQuestion W → LiftedQuestion W) : (lq1.conj lq2).bind f = (lq1.bind f).conj (lq2.bind f)

Conjunction distributes over bind from the left.

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.disj_as_choice {W : Type u_1} (lq1 lq2 : LiftedQuestion W) (P : QuestionProperty W) : lq1.disj lq2 P ↔ lq1 P ∨ lq2 P

Disjunction of lifted questions via the alternative structure.

This shows disjunction is the "choice" operation for the continuation monad, corresponding to B&S's treatment of coordination in tower semantics.

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.map_disj {W : Type u_1} (f : GSQuestion W → GSQuestion W) (lq1 lq2 : LiftedQuestion W) : map f (lq1.disj lq2) = (map f lq1).disj (map f lq2)

Map preserves disjunction.

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.map_conj {W : Type u_1} (f : GSQuestion W → GSQuestion W) (lq1 lq2 : LiftedQuestion W) : map f (lq1.conj lq2) = (map f lq1).conj (map f lq2)

Map preserves conjunction.

def Semantics.Questions.LiftedTypes.LiftedQuestion.lower? {W : Type u_1} (_lq : LiftedQuestion W) : Option (GSQuestion W)

Lower a lifted question back to core type, if it's principal.

This is a partial operation: non-principal lifted questions (like disjunctions of non-equivalent questions) cannot be lowered.

Equations

• _lq.lower? = none

def Semantics.Questions.LiftedTypes.LiftedQuestion.isLowerable {W : Type u_1} (lq : LiftedQuestion W) : Prop

A lifted question can be lowered iff it's equivalent to some principal one.

Equations

• lq.isLowerable = ∃ (q : Semantics.Questions.GSQuestion W), ∀ (P : Semantics.Questions.LiftedTypes.QuestionProperty W), lq P ↔ P q

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.lift_injective {W : Type u_1} (q1 q2 : GSQuestion W) (h : lift q1 = lift q2) (P : QuestionProperty W) : P q1 ↔ P q2

Lifting preserves identity: lift is injective on extensionally equal questions.

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.disj_comm {W : Type u_1} (lq1 lq2 : LiftedQuestion W) : lq1.disj lq2 = lq2.disj lq1

Disjunction is commutative.

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.conj_comm {W : Type u_1} (lq1 lq2 : LiftedQuestion W) : lq1.conj lq2 = lq2.conj lq1

Conjunction is commutative.

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.disj_assoc {W : Type u_1} (lq1 lq2 lq3 : LiftedQuestion W) : (lq1.disj lq2).disj lq3 = lq1.disj (lq2.disj lq3)

Disjunction is associative.

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.conj_assoc {W : Type u_1} (lq1 lq2 lq3 : LiftedQuestion W) : (lq1.conj lq2).conj lq3 = lq1.conj (lq2.conj lq3)

Conjunction is associative.

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.lift_conj_refinement {W : Type u_1} (q1 q2 : GSQuestion W) : have q12 := QUD.compose q1 q2; ∀ (P : QuestionProperty W), (∀ (q q' : QUD W), q'.refines q → P q → P q') → (lift q1).conj (lift q2) P → lift q12 P

Lifting distributes over conjunction (principal case).

If Q₁ and Q₂ have a common refinement (Q₁ * Q₂ = compose), then: conj (lift Q₁) (lift Q₂) is equivalent to lift (Q₁ * Q₂) for "refinement properties".

def Semantics.Questions.LiftedTypes.LiftedQuestion.liftedRefines {W : Type u_1} (lq1 lq2 : LiftedQuestion W) : Prop

The refinement property, lifted to LiftedQuestion.

A lifted question "refines" another if it entails the other's properties.

Equations

• lq1.liftedRefines lq2 = ∀ (P : Semantics.Questions.LiftedTypes.QuestionProperty W), lq2 P → lq1 P

theorem Semantics.Questions.LiftedTypes.LiftedQuestion.lift_preserves_refinement {W : Type u_1} (q q' : GSQuestion W) (h : QUD.refines q q') (P : QuestionProperty W) (hMono : ∀ (q₁ q₂ : QUD W), q₁.refines q₂ → P q₂ → P q₁) (hP' : lift q' P) : lift q P

Lifting preserves refinement for refinement-monotone properties.

Since lift q = λ P => P q, the unrestricted liftedRefines (lift q) (lift q') reduces to ∀ P, P q' → P q, which is Leibniz equality — much stronger than partition refinement. The correct version restricts to properties that are monotone under refinement (finer partitions inherit them).

Counterexample for the unrestricted version: let P = "has exactly 1 cell". The trivial partition q' satisfies P, but the identity partition q (which refines q') does not.

def Semantics.Questions.LiftedTypes.LiftedQuestion.answers {W : Type u_1} (p : W → Prop) (lq : LiftedQuestion W) (worlds : List W) : Prop

An answer to a lifted question: a proposition that resolves some underlying question.

In the lifted setting, "p answers LQ" means: ∃Q ∈ LQ. p is an answer to Q

Note: Full definition requires a world list parameter for toCells.

Equations

• Semantics.Questions.LiftedTypes.LiftedQuestion.answers p lq worlds = lq fun (q : Semantics.Questions.GSQuestion W) => ∃ cell ∈ QUD.toCells q worlds, ∀ (w : W), cell w = true ↔ p w

def Semantics.Questions.LiftedTypes.LiftedQuestion.partiallyAnswers {W : Type u_1} (p : W → Prop) (lq : LiftedQuestion W) (worlds : List W) : Prop

Partial answerhood for lifted questions.

Equations

• Semantics.Questions.LiftedTypes.LiftedQuestion.partiallyAnswers p lq worlds = lq fun (q : Semantics.Questions.GSQuestion W) => ∃ cell ∈ QUD.toCells q worlds, ∀ (w : W), p w → cell w = true

def Semantics.Questions.LiftedTypes.«term_⊔_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Questions.LiftedTypes.«term_⊓_» : Lean.TrailingParserDescr

Equations

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