def pGCL.AST {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (C : pGCL Γ) : Prop

A program is Almost Surely Terminating iff it's weakest pre-expectation without ticks of one is one is.

Equations

• C.AST = (wp[Optimization.Demonic]⟦@C.st⟧ 1 = 1)

noncomputable def pGCL.cwp {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (O : Optimization) (C : pGCL Γ) : (State Γ → ENNReal) →o State Γ → ENNReal

Equations

• cwp[O]⟦@C⟧ = { toFun := fun (x : pGCL.State Γ → ENNReal) => wp[O]⟦@C⟧ x / ⇑(wlp'[O]⟦@C⟧ 1), monotone' := ⋯ }

def pGCL.«termCwp[_]⟦_⟧» : Lean.ParserDescr

Equations

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

def pGCL.cwpUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.ertEnc {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : pGCL Γ → pGCL Γ

Encodes a program for analyzing expected runtimes by removing all existing tick statements, and adding tick(1) to every existing non-tick statement.

Equations

• pgcl {skip}.ertEnc = pgcl {tick(1) ; skip}
• pgcl {@x_1 := @A}.ertEnc = pgcl {tick(1) ; @x_1 := @A}
• pgcl {@C₁ ; @C₂}.ertEnc = pgcl {@C₁.ertEnc ; @C₂.ertEnc}
• pgcl {{ @C₁ } [@p] { @C₂ }}.ertEnc = pgcl {tick(1) ; { @C₁.ertEnc } [@p] { @C₂.ertEnc }}
• pgcl {{ @C₁ } [] { @C₂ }}.ertEnc = pgcl {tick(1) ; { @C₁.ertEnc } [] { @C₂.ertEnc }}
• pgcl {while @b { @C' }}.ertEnc = pgcl {tick(1) ; while @b { @C'.ertEnc }}
• pgcl {tick(@a)}.ertEnc = pgcl {skip}
• pgcl {observe(@b)}.ertEnc = pgcl {tick(1) ; observe(@b)}

noncomputable def pGCL.ert {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (O : Optimization) (C : pGCL Γ) : (State Γ → ENNReal) →o State Γ → ENNReal

Equations

• ert[O]⟦@C⟧ = wp[O]⟦@C.ertEnc⟧

def pGCL.«termErt[_]⟦_⟧» : Lean.ParserDescr

Equations

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

def pGCL.ertUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.ParkInvariant {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (g : (State Γ → ENNReal) →o State Γ → ENNReal) (b : BExpr Γ) (φ I : State Γ → ENNReal) : Prop

A Park invariant.

Equations

• pGCL.ParkInvariant g b φ I = (((Ψ[g] b) φ) I ≤ I)

theorem pGCL.ParkInduction {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {b : BExpr Γ} {C : pGCL Γ} {φ I : State Γ → ENNReal} (h : ParkInvariant wp[O]⟦@C⟧ b φ I) : wp[O]⟦while @b { @C }⟧ φ ≤ I

Park induction.

def pGCL.ParkCoinvariant {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (g : ProbExp Γ →o ProbExp Γ) (b : BExpr Γ) (φ I : ProbExp Γ) : Prop

A Park coinvariant.

Equations

• pGCL.ParkCoinvariant g b φ I = (I ≤ ((pΨ[g] b) φ) I)

theorem pGCL.ParkCoinduction {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {b : BExpr Γ} {C : pGCL Γ} {φ I : ProbExp Γ} (h : ParkCoinvariant wlp'[O]⟦@C⟧ b φ I) : I ≤ wlp'[O]⟦while @b { @C }⟧ φ

Park coinduction.

def pGCL.ParkKInvariant {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (g : (State Γ → ENNReal) →o State Γ → ENNReal) (b : BExpr Γ) (φ : State Γ → ENNReal) (k : ℕ) (I : State Γ → ENNReal) : Prop

A Park k-invariant.

Equations

• pGCL.ParkKInvariant g b φ k I = (((Ψ[g] b) φ) ((fun (x : pGCL.State Γ → ENNReal) => ((Ψ[g] b) φ) x ⊓ I)^[k] I) ≤ I)

theorem pGCL.ParkKInduction {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {b : BExpr Γ} {C : pGCL Γ} {φ I : State Γ → ENNReal} (k : ℕ) (h : ParkKInvariant wp[O]⟦@C⟧ b φ k I) : wp[O]⟦while @b { @C }⟧ φ ≤ I

Park k-induction.

def pGCL.ParkKCoinvariant {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (g : ProbExp Γ →o ProbExp Γ) (b : BExpr Γ) (φ : ProbExp Γ) (k : ℕ) (I : ProbExp Γ) : Prop

A Park k-coinvariant.

Equations

• pGCL.ParkKCoinvariant g b φ k I = (I ≤ ((pΨ[g] b) φ) ((fun (x : pGCL.ProbExp Γ) => ((pΨ[g] b) φ) x ⊔ I)^[k] I))

theorem pGCL.ParkKCoinduction {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {b : BExpr Γ} {C : pGCL Γ} {φ I : ProbExp Γ} (k : ℕ) (h : ParkKCoinvariant wlp'[O]⟦@C⟧ b φ k I) : I ≤ wlp'[O]⟦while @b { @C }⟧ φ

Park k-coinduction.