@[reducible, inline]

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

CDRT state: a register/assignment function.

Registers are indexed by natural numbers and store entity values.

Equations

• Semantics.Dynamic.CDRT.Register E = (ℕ → 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)

@[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.