@[reducible, inline]

abbrev Semantics.Dynamic.CDRT.Register (E : Type u_1) : Type u_1

CDRT state: a register/assignment function.

Muskens names them "registers" but the type is Core.Assignment E; this alias preserves Muskens's vocabulary while sharing the simp set (Assignment.update_at, update_ne, update_overwrite, update_self) with H&K composition, DPL, Charlow continuations, and Spector's plural substrate.

Equations

• Semantics.Dynamic.CDRT.Register E = Core.Assignment E

def Semantics.Dynamic.CDRT.DProp (E : Type u_1) : Type u_1

Dynamic proposition: relates input and output states.

⟦φ⟧ : Register E → Register E → Prop

Equations

• Semantics.Dynamic.CDRT.DProp E = (Semantics.Dynamic.CDRT.Register E → Semantics.Dynamic.CDRT.Register E → Prop)

def Semantics.Dynamic.CDRT.SProp (E : Type u_1) : Type u_1

Static proposition (for embedding classical logic).

Equations

• Semantics.Dynamic.CDRT.SProp E = (Semantics.Dynamic.CDRT.Register E → Prop)

def Semantics.Dynamic.CDRT.DProp.ofStatic {E : Type u_1} (p : SProp E) : DProp E

Embed a static proposition as a dynamic one (test).

⟦p⟧(i, o) iff i = o ∧ p(i)

Equations

• Semantics.Dynamic.CDRT.DProp.ofStatic p i o = (i = o ∧ p i)

def Semantics.Dynamic.CDRT.DProp.seq {E : Type u_1} (φ ψ : DProp E) : DProp E

Dynamic conjunction: relational composition.

⟦φ; ψ⟧(i, o) iff ∃k. ⟦φ⟧(i, k) ∧ ⟦ψ⟧(k, o)

Equations

• (φ ;; ψ) i o = ∃ (k : Semantics.Dynamic.CDRT.Register E), φ i k ∧ ψ k o

def Semantics.Dynamic.CDRT.«term_;;_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Dynamic.CDRT.DProp.new {E : Type u_1} (n : ℕ) : DProp E

New discourse referent introduction.

[new n] extends the register at position n with an arbitrary value.

Equations

• Semantics.Dynamic.CDRT.DProp.new n i o = ∃ (e : E), o = fun (m : ℕ) => if m = n then e else i m

def Semantics.Dynamic.CDRT.DProp.neg {E : Type u_1} (φ : DProp E) : DProp E

Dynamic negation: test for failure.

⟦¬φ⟧(i, o) iff i = o ∧ ¬∃k. ⟦φ⟧(i, k)

Equations

• φ.neg i o = (i = o ∧ ¬∃ (k : Semantics.Dynamic.CDRT.Register E), φ i k)

def Semantics.Dynamic.CDRT.DProp.impl {E : Type u_1} (φ ψ : DProp E) : DProp E

Dynamic implication: if φ succeeds, ψ must succeed.

⟦φ → ψ⟧(i, o) iff i = o ∧ ∀k. (⟦φ⟧(i, k) → ∃m. ⟦ψ⟧(k, m))

Equations

• φ.impl ψ i o = (i = o ∧ ∀ (k : Semantics.Dynamic.CDRT.Register E), φ i k → ∃ (m : Semantics.Dynamic.CDRT.Register E), ψ k m)

def Semantics.Dynamic.CDRT.DProp.ddisj {E : Type u_1} (φ ψ : DProp E) : DProp E

Dynamic disjunction: φ or ψ.

⟦φ or ψ⟧(i, o) iff i = o ∧ (∃k. ⟦φ⟧(i, k) ∨ ⟦ψ⟧(i, k))

Disjunction is a test: it checks whether either disjunct is satisfiable without changing state. Corresponds to SEM2 (@cite{muskens-1996}, p. 148).

Equations

• φ.ddisj ψ i o = (i = o ∧ ∃ (k : Semantics.Dynamic.CDRT.Register E), φ i k ∨ ψ i k)

@[reducible, inline]

abbrev Semantics.Dynamic.CDRT.CDRTEntity (E : Type u_1) : Type u_1

Entity type: individuals.

Equations

• Semantics.Dynamic.CDRT.CDRTEntity E = E

def Semantics.Dynamic.CDRT.GQ (E : Type u_1) : Type u_1

Generalized quantifier type.

Equations

• Semantics.Dynamic.CDRT.GQ E = ((E → Semantics.Dynamic.CDRT.DProp E) → Semantics.Dynamic.CDRT.DProp E)

def Semantics.Dynamic.CDRT.indefinite {E : Type u_1} (n : ℕ) (p q : E → DProp E) : DProp E

Indefinite "a/an": introduces dref and applies predicate.

⟦a⟧ = λP.λQ. new n; P(rn); Q(rn)

where rn is the register lookup at n.

Equations

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

def Semantics.Dynamic.CDRT.pronoun {E : Type u_1} (n : ℕ) : Register E → E

Pronoun: lookup register value.

⟦heₙ⟧ = rn (returns the value at register n)

Equations

• Semantics.Dynamic.CDRT.pronoun n r = r n

def Semantics.Dynamic.CDRT.DProp.true_at {E : Type u_1} (φ : DProp E) (i : Register E) : Prop

A dynamic proposition is TRUE at state i if it can transition somewhere.

Equations

• φ.true_at i = ∃ (o : Semantics.Dynamic.CDRT.Register E), φ i o

def Semantics.Dynamic.CDRT.DProp.entails {E : Type u_1} (φ ψ : DProp E) : Prop

Dynamic entailment: φ entails ψ if ψ is true after φ.

Equations

• φ.entails ψ = ∀ (i o : Semantics.Dynamic.CDRT.Register E), φ i o → ψ.true_at o

theorem Semantics.Dynamic.CDRT.DProp.neg_output {E : Type u_1} {φ : DProp E} {i o : Register E} (h : φ.neg i o) : o = i

The output of a negated DProp always equals the input register.

theorem Semantics.Dynamic.CDRT.DProp.impl_true_at {E : Type u_1} (φ ψ : DProp E) (i : Register E) : (φ.impl ψ).true_at i ↔ ∀ (k : Register E), φ i k → ψ.true_at k

DProp.impl is true at i iff every antecedent extension satisfies the consequent.

theorem Semantics.Dynamic.CDRT.DProp.ofStatic_true_at {E : Type u_1} (p : SProp E) (i : Register E) : (ofStatic p).true_at i ↔ p i

A static DProp is true at i iff its static content holds.

CDRT-as-Dynamic-Ty2

CDRT's Register E = Nat → E is the same type as @cite{muskens-1996}'s state space S in Dynamic Ty2 with discourse referents Dref S E = S → E. Drefs in CDRT are register-lookups; DProp E and DRS (Register E) are the same type, so the embedding is a pair of identity functions.

def Semantics.Dynamic.CDRT.dref {E : Type u_1} (n : ℕ) : Core.Dref (Register E) E

CDRT register lookup as a Dynamic Ty2 dref.

Equations

• Semantics.Dynamic.CDRT.dref n r = r n

def Semantics.Dynamic.CDRT.toDRS {E : Type u_1} (φ : DProp E) : Core.DRS (Register E)

DProp E IS a DRS over Register E.

Equations

• Semantics.Dynamic.CDRT.toDRS φ = φ