Weakest Precondition Calculus

@cite{muskens-1996}

§III.6 (pp. 172–175): The weakest precondition calculus provides a compositional algorithm for extracting first-order truth conditions from DRS meanings. Given a DRS D and a postcondition χ, wp D χ characterizes the input states from which D can transition to a state satisfying χ.

Compositional Rules

Rule	Theorem	Paper ref
wp [C] χ = C ∧ χ	wp_test	WP_{[]}
wp (D₁ ⨟ D₂) χ = wp D₁ (wp D₂ χ)	wp_seq	WP_{;}
wp [u] χ = ∃e, χ(extend i u e)	wp_randomAssign	WP_{[]} (∃ clause)
wp D ⊤ = closure D	wp_true_eq_closure	Proposition 2

Key Results

• Proposition 2: wp(K, ⊤) = ∃j K(i)(j) (truth = existential closure)
• Proposition 3: DRT entailment = entailment of truth conditions
• Corollary: DPL entailment = validity of dynamic implication

def Semantics.Dynamic.Core.WeakestPrecondition.wp {S : Type u_1} (D : DynProp.DRS S) (χ : DynProp.Condition S) : DynProp.Condition S

Weakest precondition of DRS D with postcondition χ.

wp D χ i holds iff there exists an output state j such that D transitions from i to j and χ holds at j.

Equations

• Semantics.Dynamic.Core.WeakestPrecondition.wp D χ i = ∃ (j : S), D i j ∧ χ j

theorem Semantics.Dynamic.Core.WeakestPrecondition.wp_test {S : Type u_1} (C χ : DynProp.Condition S) : wp [C] χ = fun (i : S) => C i ∧ χ i

WP of a test: wp [C] χ = C ∧ χ.

A test checks C and passes the state through unchanged.

theorem Semantics.Dynamic.Core.WeakestPrecondition.wp_seq {S : Type u_1} (D₁ D₂ : DynProp.DRS S) (χ : DynProp.Condition S) : wp (D₁ ⨟ D₂) χ = wp D₁ (wp D₂ χ)

WP of sequencing: wp (D₁ ⨟ D₂) χ = wp D₁ (wp D₂ χ).

Corresponds to WP_{;} (p. 173): the postcondition threads through.

theorem Semantics.Dynamic.Core.WeakestPrecondition.wp_randomAssign {S : Type u_1} {E : Type u_2} [DynamicTy2.AssignmentStructure S E] (u : S → E) (χ : DynProp.Condition S) : wp [u]ᵈʳᵉᶠ χ = fun (i : S) => ∃ (e : E), χ (DynamicTy2.AssignmentStructure.extend i u e)

WP of random assignment: wp [u] χ = ∃e, χ(extend i u e).

Introducing a discourse referent existentially quantifies over values. Corresponds to the ∃ clause in WP_{[]} (p. 173).

theorem Semantics.Dynamic.Core.WeakestPrecondition.wp_dexists {S : Type u_1} {E : Type u_2} [DynamicTy2.AssignmentStructure S E] (u : S → E) (D : DynProp.DRS S) (χ : DynProp.Condition S) : wp ∃'u(D) χ = fun (i : S) => ∃ (e : E), wp D χ (DynamicTy2.AssignmentStructure.extend i u e)

WP of existential DRS: wp (∃u. D) χ = ∃e, wp D χ (extend i u e).

theorem Semantics.Dynamic.Core.WeakestPrecondition.wp_true_eq_closure {S : Type u_1} (D : DynProp.DRS S) : (wp D fun (x : S) => True) = DynProp.closure D

Proposition 2 (@cite{muskens-1996}, p. 175):

wp(K, ⊤) is equivalent to ∃j K(i)(j) — the existential closure. In the semantic formulation, this is definitional.

def Semantics.Dynamic.Core.WeakestPrecondition.drtEntails {S : Type u_1} (premises : List (DynProp.DRS S)) (conclusion : DynProp.DRS S) : Prop

DRT entailment (@cite{muskens-1996}, p. 175):

K₁,...,Kₙ ⊨_DRT K iff for every state i, if all premises are true at i, then the conclusion is true at i.

Equations

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

theorem Semantics.Dynamic.Core.WeakestPrecondition.proposition_3 {S : Type u_1} (premises : List (DynProp.DRS S)) (conclusion : DynProp.DRS S) : drtEntails premises conclusion ↔ ∀ (i : S), (∀ (D : DynProp.DRS S), D ∈ premises → wp D (fun (x : S) => True) i) → wp conclusion (fun (x : S) => True) i

Proposition 3 (@cite{muskens-1996}, p. 175):

DRT entailment reduces to entailment of truth conditions. K₁,...,Kₙ ⊨_DRT K iff wp(K₁, ⊤),...,wp(Kₙ, ⊤) entail wp(K, ⊤).

def Semantics.Dynamic.Core.WeakestPrecondition.dplEntails {S : Type u_1} (D₁ D₂ : DynProp.DRS S) : Prop

DPL-style entailment: every output of D₁ can be extended by D₂.

Equations

• Semantics.Dynamic.Core.WeakestPrecondition.dplEntails D₁ D₂ = ∀ (i j : S), D₁ i j → ∃ (k : S), D₂ j k

theorem Semantics.Dynamic.Core.WeakestPrecondition.dpl_entailment_eq_dimpl_valid {S : Type u_1} (D₁ D₂ : DynProp.DRS S) : dplEntails D₁ D₂ ↔ ∀ (i : S), DynProp.dimpl D₁ D₂ i

Corollary (@cite{muskens-1996}, p. 175):

DPL entailment = validity of dynamic implication. K₁,...,Kₙ ⊨_DPL K iff ⊢ tr((K₁;...;Kₙ) ⇒ K).

theorem Semantics.Dynamic.Core.WeakestPrecondition.tr_neg_eq {S : Type u_1} (D : DynProp.DRS S) : (∼D) = fun (i : S) => ¬wp D (fun (x : S) => True) i

TR of negation: tr(not K) = ¬wp(K, ⊤).

The truth of ¬D at state i is the negation of D's satisfiability. Corresponds to TR_{not} (p. 173).

theorem Semantics.Dynamic.Core.WeakestPrecondition.tr_disj_eq {S : Type u_1} (D₁ D₂ : DynProp.DRS S) : DynProp.ddisj D₁ D₂ = fun (i : S) => wp D₁ (fun (x : S) => True) i ∨ wp D₂ (fun (x : S) => True) i

TR of disjunction: tr(K₁ or K₂) = wp(K₁, ⊤) ∨ wp(K₂, ⊤).

Corresponds to TR_{or} (p. 173). The existential distributes over disjunction.

theorem Semantics.Dynamic.Core.WeakestPrecondition.tr_impl_eq {S : Type u_1} (D₁ D₂ : DynProp.DRS S) : DynProp.dimpl D₁ D₂ = fun (i : S) => ¬wp D₁ (fun (j : S) => ¬wp D₂ (fun (x : S) => True) j) i

TR of implication: tr(K₁ ⇒ K₂) = ¬wp(K₁, ¬wp(K₂, ⊤)).

Dynamic implication = no way to satisfy antecedent without satisfying consequent. Corresponds to TR_{⇒} (p. 173).

def Semantics.Dynamic.Core.WeakestPrecondition.isProper {S : Type u_1} (D : DynProp.DRS S) : Prop

A DRS is semantically proper if its truth condition is uniform across input states: satisfiability doesn't depend on the input assignment.

This is the semantic counterpart of @cite{muskens-1996}'s syntactic notion of properness (§III.5, p. 171): a DRS with no free discourse referents. Proposition 1 (p. 174) connects the two: K is proper iff wp(K, ⊤) is a closed formula.

Equations

• Semantics.Dynamic.Core.WeakestPrecondition.isProper D = ∀ (i₁ i₂ : S), Semantics.Dynamic.Core.DynProp.closure D i₁ ↔ Semantics.Dynamic.Core.DynProp.closure D i₂

theorem Semantics.Dynamic.Core.WeakestPrecondition.proper_wp_uniform {S : Type u_1} (D : DynProp.DRS S) (h : isProper D) (i₁ i₂ : S) : wp D (fun (x : S) => True) i₁ ↔ wp D (fun (x : S) => True) i₂

Proper DRSes have state-independent weakest preconditions.