Post-Suppositional Dynamic GQs

@cite{charlow-2021}

@cite{charlow-2021}'s §5: bi-dimensional meanings using a Writer-like monad. A PostSupp S A carries both a value and accumulated post-suppositional content (a DRS that constrains but doesn't change the assignment).

Modified numerals like "exactly 3" contribute their cardinality test as post-suppositional content, which is resolved after maximization. This automatically produces cumulative readings because post-suppositions from different quantifiers compose independently.

structure Semantics.Dynamic.DynamicGQ.PostSuppositional.PostSupp (S : Type u_2) (A : Type u_3) : Type (max u_2 u_3)

Bi-dimensional meaning: a value paired with post-suppositional content. The post-supposition is a DRS that will be conjoined at the discourse level, after all scope-taking is done.

• val : A

  The "at-issue" value

• postsup : Core.DynProp.DRS S

  Accumulated post-suppositional content

def Semantics.Dynamic.DynamicGQ.PostSuppositional.PostSupp.pure {S : Type u_2} {A : Type u_3} (a : A) : PostSupp S A

Pure: trivial post-supposition (equation 120). The post-suppositional DRS is the identity (test True).

Equations

• Semantics.Dynamic.DynamicGQ.PostSuppositional.PostSupp.pure a = { val := a, postsup := [fun (x : S) => True] }

def Semantics.Dynamic.DynamicGQ.PostSuppositional.PostSupp.bind {S : Type u_2} {A : Type u_3} {B : Type u_4} (m : PostSupp S A) (f : A → PostSupp S B) : PostSupp S B

Bind: sequence post-suppositions via dseq (equation 121). Post-suppositional content accumulates via dynamic conjunction.

Equations

• m.bind f = { val := (f m.val).val, postsup := m.postsup ⨟ (f m.val).postsup }

def Semantics.Dynamic.DynamicGQ.PostSuppositional.PostSupp.map {S : Type u_2} {A : Type u_3} {B : Type u_4} (f : A → B) (m : PostSupp S A) : PostSupp S B

Map: apply a function to the at-issue value, preserving post-suppositions.

Equations

• Semantics.Dynamic.DynamicGQ.PostSuppositional.PostSupp.map f m = { val := f m.val, postsup := m.postsup }

def Semantics.Dynamic.DynamicGQ.PostSuppositional.PostSupp.reify {S : Type u_1} (p : PostSupp S (Core.DynProp.DRS S)) : Core.DynProp.DRS S

Reify (bullet operator, equation 58): conjoin value and post-supposition. For a PostSupp S (DRS S), this produces a single DRS by sequencing the at-issue DRS with the post-suppositional constraint.

Equations

• p.reify = p.val ⨟ p.postsup

def Semantics.Dynamic.DynamicGQ.PostSuppositional.PostSupp.trueAt {S : Type u_1} (p : PostSupp S (Core.DynProp.DRS S)) (i : S) : Prop

Truth at an assignment for bi-dimensional meanings (equation 56): the at-issue content and post-suppositional content must both be satisfiable.

Equations

• p.trueAt i = ∃ (j : S), p.val i j ∧ ∃ (k : S), p.postsup j k

def Semantics.Dynamic.DynamicGQ.PostSuppositional.exactlyN_postsup {S : Type u_2} {E : Type u_3} [Core.DynamicTy2.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v : Core.DynamicTy2.Dref S E) (P : E → Prop) (n : ℕ) (Mvar' : Core.DynamicTy2.Dref S E → Core.DynProp.DRS S → Core.DynProp.DRS S) (Evar' : Core.DynamicTy2.Dref S E → (E → Prop) → Core.DynProp.DRS S) (CardTest' : Core.DynamicTy2.Dref S E → ℕ → Core.DynProp.DRS S) : PostSupp S (Core.DynProp.DRS S)

"Exactly N" as post-suppositional meaning (equation 53): ⟨M_v(E^v P; []), n_v⟩ The at-issue content introduces and maximizes v; the cardinality test is the post-supposition.

Equations

• Semantics.Dynamic.DynamicGQ.PostSuppositional.exactlyN_postsup v P n Mvar' Evar' CardTest' = { val := Mvar' v (Evar' v P), postsup := CardTest' v n }

theorem Semantics.Dynamic.DynamicGQ.PostSuppositional.PostSupp.bind_left_id {S : Type u_2} {A : Type u_3} {B : Type u_4} (a : A) (f : A → PostSupp S B) : (pure a).bind f = f a

Left identity for PostSupp bind.

theorem Semantics.Dynamic.DynamicGQ.PostSuppositional.PostSupp.reify_pure {S : Type u_2} (D : Core.DynProp.DRS S) : (pure D).reify = D ⨟ [fun (x : S) => True]

Reify of a pure post-supposition recovers the original DRS (modulo the trivial True test).

theorem Semantics.Dynamic.DynamicGQ.PostSuppositional.postsup_cumulative {S : Type u_2} {E : Type u_3} [Core.DynamicTy2.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Core.DynamicTy2.Dref S E) (_boys _movies : E → Prop) : True

Post-suppositional combination yields cumulative readings. TODO: Formalize the full derivation.