Bundled Query Runtimes

This file packages concrete query implementations as explicit runtime objects.

HasQuery spec m is the right capability interface for constructions that only need to issue queries. When we want to instrument, transport, or otherwise analyze that capability, we also need an explicit QueryImpl spec m to work with. QueryRuntime spec m is the thin bundle that stores that implementation without changing the capability layer.

The main use cases are:

• reifying an existing HasQuery capability as a QueryRuntime;
• adding cost, counting, or logging layers to a runtime;
• instantiating a generic HasQuery construction directly in an analysis monad.

structure QueryRuntime {ι : Type} (spec : OracleSpec ι) (m : Type → Type u_1) : Type u_1

Bundled implementation of the oracle family spec in the ambient monad m.

• impl : QueryImpl spec m

  Concrete implementation of each query in the family spec.

@[reducible, inline]

abbrev QueryRuntime.toHasQuery {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} (runtime : QueryRuntime spec m) : HasQuery spec m

View a bundled query runtime as the corresponding HasQuery capability.

@[simp]

theorem QueryRuntime.toHasQuery_query {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} (runtime : QueryRuntime spec m) (t : spec.Domain) : HasQuery.query t = runtime.impl t

def QueryRuntime.ofHasQuery {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [HasQuery spec m] : QueryRuntime spec m

Repackage an existing HasQuery capability as an explicit query runtime.

@[simp]

theorem QueryRuntime.ofHasQuery_impl {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [HasQuery spec m] (t : spec.Domain) : ofHasQuery.impl t = HasQuery.query t

@[reducible, inline]

abbrev QueryRuntime.oracleCompRuntime {ι : Type} (spec : OracleSpec ι) : QueryRuntime spec (OracleComp spec)

The canonical bundled runtime for the free oracle monad OracleComp spec.

@[simp]

theorem QueryRuntime.oracleCompRuntime_impl_eq_ofLift {ι : Type} {spec : OracleSpec ι} : (oracleCompRuntime spec).impl = QueryImpl.ofLift spec (OracleComp spec)

def QueryRuntime.withCost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] {ω : Type} [Monoid ω] (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) : QueryRuntime spec (WriterT ω m)

Instrument a query runtime with multiplicative/monoidal cost accumulation in a WriterT layer.

@[simp]

theorem QueryRuntime.withCost_impl {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] {ω : Type} [Monoid ω] (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) (t : spec.Domain) : (runtime.withCost costFn).impl t = do tell (costFn t) liftM (runtime.impl t)

def QueryRuntime.withAddCost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] {ω : Type} [AddMonoid ω] (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) : QueryRuntime spec (AddWriterT ω m)

Instrument a query runtime with additive cost accumulation in an AddWriterT layer.

@[simp]

theorem QueryRuntime.withAddCost_impl {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] {ω : Type} [AddMonoid ω] (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) (t : spec.Domain) : (runtime.withAddCost costFn).impl t = do AddWriterT.addTell (costFn t) liftM (runtime.impl t)

def QueryRuntime.withUnitCost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] (runtime : QueryRuntime spec m) : QueryRuntime spec (AddWriterT ℕ m)

Instrument a query runtime with unit additive cost for every query.

@[simp]

theorem QueryRuntime.withUnitCost_impl {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] (runtime : QueryRuntime spec m) (t : spec.Domain) : runtime.withUnitCost.impl t = do AddWriterT.addTell 1 liftM (runtime.impl t)

def AddWriterT.PathwiseCostAtMost {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] (oa : AddWriterT ω m α) (w : ω) : Prop

Pathwise upper bound for an AddWriterT computation: every reachable execution result carries additive cost at most w.

def AddWriterT.PathwiseCostAtLeast {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] (oa : AddWriterT ω m α) (w : ω) : Prop

Pathwise lower bound for an AddWriterT computation: every reachable execution result carries additive cost at least w.

def AddWriterT.PathwiseCostEqOnSupport {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] (oa : AddWriterT ω m α) (w : ω) : Prop

Pathwise exactness on support for an AddWriterT computation: every reachable execution result carries exactly the additive cost w.

This is the weak extensional notion of pathwise exactness. If oa.run has empty support, it holds vacuously for every w. Use [AddWriterT.PathwiseHasCost] when the intended meaning is that oa has an exact pathwise cost and admits at least one reachable execution.

@[simp]

theorem AddWriterT.pathwiseCostEqOnSupport_iff {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] (oa : AddWriterT ω m α) (w : ω) : oa.PathwiseCostEqOnSupport w ↔ oa.PathwiseCostAtMost w ∧ oa.PathwiseCostAtLeast w

def AddWriterT.PathwiseHasCost {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] (oa : AddWriterT ω m α) (w : ω) : Prop

Pathwise exact cost for an AddWriterT computation: oa has at least one reachable execution, and every reachable execution result carries exactly the additive cost w.

This is the strong semantic notion of exact cost over execution paths. Unlike [AddWriterT.HasCost], it does not require cost to be recoverable from the final output alone. Unlike [AddWriterT.PathwiseCostEqOnSupport], it is not vacuous on computations with empty support.

@[simp]

theorem AddWriterT.pathwiseHasCost_iff {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] (oa : AddWriterT ω m α) (w : ω) : oa.PathwiseHasCost w ↔ (support (WriterT.run oa)).Nonempty ∧ oa.PathwiseCostEqOnSupport w

theorem AddWriterT.PathwiseHasCost.nonempty {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] {oa : AddWriterT ω m α} {w : ω} (h : oa.PathwiseHasCost w) : (support (WriterT.run oa)).Nonempty

theorem AddWriterT.PathwiseCostEqOnSupport.atMost {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] {oa : AddWriterT ω m α} {w : ω} (h : oa.PathwiseCostEqOnSupport w) : oa.PathwiseCostAtMost w

theorem AddWriterT.PathwiseCostEqOnSupport.atLeast {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] {oa : AddWriterT ω m α} {w : ω} (h : oa.PathwiseCostEqOnSupport w) : oa.PathwiseCostAtLeast w

theorem AddWriterT.PathwiseHasCost.eqOnSupport {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] {oa : AddWriterT ω m α} {w : ω} (h : oa.PathwiseHasCost w) : oa.PathwiseCostEqOnSupport w

theorem AddWriterT.PathwiseHasCost.atMost {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] {oa : AddWriterT ω m α} {w : ω} (h : oa.PathwiseHasCost w) : oa.PathwiseCostAtMost w

theorem AddWriterT.PathwiseHasCost.atLeast {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] {oa : AddWriterT ω m α} {w : ω} (h : oa.PathwiseHasCost w) : oa.PathwiseCostAtLeast w

theorem AddWriterT.PathwiseHasCost.unique {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [PartialOrder ω] {oa : AddWriterT ω m α} {w₁ w₂ : ω} (h₁ : oa.PathwiseHasCost w₁) (h₂ : oa.PathwiseHasCost w₂) : w₁ = w₂

theorem AddWriterT.pathwiseCostAtMost_of_hasCost {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] {oa : AddWriterT ω m α} {w b : ω} (h : oa.HasCost w) (hwb : w ≤ b) : oa.PathwiseCostAtMost b

theorem AddWriterT.pathwiseCostAtLeast_of_hasCost {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] {oa : AddWriterT ω m α} {w b : ω} (h : oa.HasCost w) (hbw : b ≤ w) : oa.PathwiseCostAtLeast b

noncomputable def AddWriterT.expectedCost {m : Type → Type u_1} [Monad m] {α ω : Type} [HasEvalSPMF m] (oa : AddWriterT ω m α) (val : ω → ENNReal) : ENNReal

The expected additive cost of an AddWriterT computation, obtained by taking the expectation of its cost marginal.

This expectation is computed over the base monad's subdistribution semantics on oa.costs. In particular, if the underlying computation can fail, the missing mass contributes 0, exactly as for other wp-style expectations in VCV-io.

@[reducible, inline]

noncomputable abbrev AddWriterT.expectedCostNat {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSPMF m] (oa : AddWriterT ℕ m α) : ENNReal

Convenience specialization of [AddWriterT.expectedCost] to natural-valued additive costs.

theorem AddWriterT.expectedCostNat_eq_tsum_tail_probs {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSPMF m] (oa : AddWriterT ℕ m α) : oa.expectedCostNat = ∑' (i : ℕ), probEvent oa.costs fun (c : ℕ) => i < c

Tail-sum formula for the natural-valued expected cost of an AddWriterT computation:

E[cost] = ∑ i, Pr[i < cost].

This is the standard discrete expectation identity specialized to the writer-cost marginal.

theorem AddWriterT.expectedCostNat_le_tsum_of_tail_probs_le {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSPMF m] (oa : AddWriterT ℕ m α) {a : ℕ → ENNReal} (h : ∀ (i : ℕ), (probEvent oa.costs fun (c : ℕ) => i < c) ≤ a i) : oa.expectedCostNat ≤ ∑' (i : ℕ), a i

Tail domination bounds the expected natural-valued writer cost.

If the tail probability Pr[i < cost] is bounded by a i for every i, then E[cost] ≤ ∑ i, a i.

theorem AddWriterT.expectedCostNat_eq_sum_tail_probs_of_pathwiseCostAtMost {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSPMF m] [LawfulMonad m] {oa : AddWriterT ℕ m α} {n : ℕ} (h : oa.PathwiseCostAtMost n) : oa.expectedCostNat = ∑ i ∈ Finset.range n, probEvent oa.costs fun (c : ℕ) => i < c

Finite tail-sum formula for natural-valued writer cost under a pathwise upper bound.

If every execution path of oa incurs cost at most n, then the tail probabilities vanish above n, so the infinite tail sum truncates to Finset.range n.

theorem AddWriterT.expectedCost_le_of_support_bound {m : Type → Type u_1} [Monad m] {α ω : Type} [HasEvalSPMF m] (oa : AddWriterT ω m α) (val : ω → ENNReal) (c : ENNReal) (h : ∀ w ∈ support oa.costs, val w ≤ c) : oa.expectedCost val ≤ c

theorem AddWriterT.expectedCost_le_of_pathwiseCostAtMost {m : Type → Type u_1} [Monad m] {α ω : Type} [AddMonoid ω] [HasEvalSPMF m] [LawfulMonad m] [Preorder ω] {oa : AddWriterT ω m α} {w : ω} {val : ω → ENNReal} (h : oa.PathwiseCostAtMost w) (hval : Monotone val) : oa.expectedCost val ≤ val w

theorem AddWriterT.expectedCost_ge_of_pathwiseCostAtLeast {m : Type → Type u_1} [Monad m] {α ω : Type} [AddMonoid ω] [LawfulMonad m] [Preorder ω] [HasEvalPMF m] {oa : AddWriterT ω m α} {w : ω} {val : ω → ENNReal} (h : oa.PathwiseCostAtLeast w) (hval : Monotone val) : val w ≤ oa.expectedCost val

theorem AddWriterT.expectedCost_eq_tsum_outputs_of_costsAs {m : Type → Type u_1} [Monad m] {α ω : Type} [HasEvalSPMF m] [LawfulMonad m] {oa : AddWriterT ω m α} {f : α → ω} {val : ω → ENNReal} (h : oa.CostsAs f) : oa.expectedCost val = ∑' (a : α), Pr[= a | oa.outputs] * val (f a)

theorem AddWriterT.pathwiseCostAtMost_pure {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : α) : (pure x).PathwiseCostAtMost 0

theorem AddWriterT.pathwiseCostAtLeast_pure {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : α) : (pure x).PathwiseCostAtLeast 0

theorem AddWriterT.pathwiseCostEqOnSupport_pure {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : α) : (pure x).PathwiseCostEqOnSupport 0

theorem AddWriterT.pathwiseHasCost_pure {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : α) : (pure x).PathwiseHasCost 0

theorem AddWriterT.pathwiseCostAtMost_monadLift {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : m α) : (monadLift x).PathwiseCostAtMost 0

theorem AddWriterT.pathwiseCostAtLeast_monadLift {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : m α) : (monadLift x).PathwiseCostAtLeast 0

theorem AddWriterT.pathwiseCostEqOnSupport_monadLift {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : m α) : (monadLift x).PathwiseCostEqOnSupport 0

theorem AddWriterT.pathwiseHasCost_monadLift_of_supportNonempty {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : m α) (hx : (support x).Nonempty) : (monadLift x).PathwiseHasCost 0

theorem AddWriterT.pathwiseCostAtMost_liftM {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : m α) : (liftM x).PathwiseCostAtMost 0

theorem AddWriterT.pathwiseCostAtLeast_liftM {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : m α) : (liftM x).PathwiseCostAtLeast 0

theorem AddWriterT.pathwiseCostEqOnSupport_liftM {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : m α) : (liftM x).PathwiseCostEqOnSupport 0

theorem AddWriterT.pathwiseHasCost_liftM_of_supportNonempty {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (x : m α) (hx : (support x).Nonempty) : (liftM x).PathwiseHasCost 0

theorem AddWriterT.pathwiseCostAtMost_probCompLift {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [MonadLiftT ProbComp m] (x : ProbComp α) : (monadLift x).PathwiseCostAtMost 0

theorem AddWriterT.pathwiseCostAtLeast_probCompLift {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [MonadLiftT ProbComp m] (x : ProbComp α) : (monadLift x).PathwiseCostAtLeast 0

theorem AddWriterT.pathwiseCostEqOnSupport_probCompLift {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [MonadLiftT ProbComp m] (x : ProbComp α) : (monadLift x).PathwiseCostEqOnSupport 0

theorem AddWriterT.pathwiseHasCost_probCompLift_of_supportNonempty {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [MonadLiftT ProbComp m] (x : ProbComp α) (hx : (support (liftM x)).Nonempty) : (monadLift x).PathwiseHasCost 0

theorem AddWriterT.pathwiseCostAtMost_mono {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] {oa : AddWriterT ω m α} {w₁ w₂ : ω} (h : oa.PathwiseCostAtMost w₁) (hw : w₁ ≤ w₂) : oa.PathwiseCostAtMost w₂

theorem AddWriterT.pathwiseCostAtLeast_mono {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] {oa : AddWriterT ω m α} {w₁ w₂ : ω} (h : oa.PathwiseCostAtLeast w₂) (hw : w₁ ≤ w₂) : oa.PathwiseCostAtLeast w₁

theorem AddWriterT.pathwiseCostAtMost_addTell {m : Type → Type u_1} [Monad m] [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (w : ω) : (addTell w).PathwiseCostAtMost w

theorem AddWriterT.pathwiseCostAtLeast_addTell {m : Type → Type u_1} [Monad m] [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (w : ω) : (addTell w).PathwiseCostAtLeast w

theorem AddWriterT.pathwiseCostEqOnSupport_addTell {m : Type → Type u_1} [Monad m] [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (w : ω) : (addTell w).PathwiseCostEqOnSupport w

theorem AddWriterT.pathwiseHasCost_addTell {m : Type → Type u_1} [Monad m] [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] (w : ω) : (addTell w).PathwiseHasCost w

theorem AddWriterT.pathwiseCostAtMost_map {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] {oa : AddWriterT ω m α} {w : ω} (f : α → β) (h : oa.PathwiseCostAtMost w) : (f <$> oa).PathwiseCostAtMost w

theorem AddWriterT.pathwiseCostAtLeast_map {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] {oa : AddWriterT ω m α} {w : ω} (f : α → β) (h : oa.PathwiseCostAtLeast w) : (f <$> oa).PathwiseCostAtLeast w

theorem AddWriterT.pathwiseCostEqOnSupport_map {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] {oa : AddWriterT ω m α} {w : ω} (f : α → β) (h : oa.PathwiseCostEqOnSupport w) : (f <$> oa).PathwiseCostEqOnSupport w

theorem AddWriterT.pathwiseHasCost_map {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] {oa : AddWriterT ω m α} {w : ω} (f : α → β) (h : oa.PathwiseHasCost w) : (f <$> oa).PathwiseHasCost w

theorem AddWriterT.pathwiseCostAtMost_bind {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {oa : AddWriterT ω m α} {f : α → AddWriterT ω m β} {w₁ w₂ : ω} (h₁ : oa.PathwiseCostAtMost w₁) (h₂ : ∀ (a : α), (f a).PathwiseCostAtMost w₂) : (oa >>= f).PathwiseCostAtMost (w₁ + w₂)

theorem AddWriterT.pathwiseCostAtLeast_bind {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {oa : AddWriterT ω m α} {f : α → AddWriterT ω m β} {w₁ w₂ : ω} (h₁ : oa.PathwiseCostAtLeast w₁) (h₂ : ∀ (a : α), (f a).PathwiseCostAtLeast w₂) : (oa >>= f).PathwiseCostAtLeast (w₁ + w₂)

theorem AddWriterT.pathwiseCostEqOnSupport_bind {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {oa : AddWriterT ω m α} {f : α → AddWriterT ω m β} {w₁ w₂ : ω} (h₁ : oa.PathwiseCostEqOnSupport w₁) (h₂ : ∀ (a : α), (f a).PathwiseCostEqOnSupport w₂) : (oa >>= f).PathwiseCostEqOnSupport (w₁ + w₂)

theorem AddWriterT.pathwiseHasCost_bind {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {oa : AddWriterT ω m α} {f : α → AddWriterT ω m β} {w₁ w₂ : ω} (h₁ : oa.PathwiseHasCost w₁) (h₂ : ∀ (a : α), (f a).PathwiseHasCost w₂) : (oa >>= f).PathwiseHasCost (w₁ + w₂)

theorem AddWriterT.pathwiseHasCost_bind_zero_left {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {oa : AddWriterT ω m α} {f : α → AddWriterT ω m β} {w : ω} (h₁ : oa.PathwiseHasCost 0) (h₂ : ∀ (a : α), (f a).PathwiseHasCost w) : (oa >>= f).PathwiseHasCost w

theorem AddWriterT.pathwiseHasCost_bind_zero_right {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {oa : AddWriterT ω m α} {f : α → AddWriterT ω m β} {w : ω} (h₁ : oa.PathwiseHasCost w) (h₂ : ∀ (a : α), (f a).PathwiseHasCost 0) : (oa >>= f).PathwiseHasCost w

theorem AddWriterT.pathwiseCostEqOnSupport_bind_zero_left {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {oa : AddWriterT ω m α} {f : α → AddWriterT ω m β} {w : ω} (h₁ : oa.PathwiseCostEqOnSupport 0) (h₂ : ∀ (a : α), (f a).PathwiseCostEqOnSupport w) : (oa >>= f).PathwiseCostEqOnSupport w

theorem AddWriterT.pathwiseCostEqOnSupport_bind_zero_right {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {oa : AddWriterT ω m α} {f : α → AddWriterT ω m β} {w : ω} (h₁ : oa.PathwiseCostEqOnSupport w) (h₂ : ∀ (a : α), (f a).PathwiseCostEqOnSupport 0) : (oa >>= f).PathwiseCostEqOnSupport w

theorem AddWriterT.pathwiseCostAtMost_fin_mOfFn {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {n : ℕ} {k : ω} {f : Fin n → AddWriterT ω m α} (h : ∀ (i : Fin n), (f i).PathwiseCostAtMost k) : (Fin.mOfFn n f).PathwiseCostAtMost (n • k)

theorem AddWriterT.pathwiseCostAtLeast_fin_mOfFn {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {n : ℕ} {k : ω} {f : Fin n → AddWriterT ω m α} (h : ∀ (i : Fin n), (f i).PathwiseCostAtLeast k) : (Fin.mOfFn n f).PathwiseCostAtLeast (n • k)

theorem AddWriterT.pathwiseHasCost_fin_mOfFn {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [LawfulMonad m] [IsOrderedAddMonoid ω] {n : ℕ} {k : ω} {f : Fin n → AddWriterT ω m α} (h : ∀ (i : Fin n), (f i).PathwiseHasCost k) : (Fin.mOfFn n f).PathwiseHasCost (n • k)

def AddWriterT.QueryBoundedAboveBy {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] (oa : AddWriterT ℕ m α) (n : ℕ) : Prop

Pathwise upper bound for a unit-cost AddWriterT computation.

def AddWriterT.QueryBoundedBelowBy {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] (oa : AddWriterT ℕ m α) (n : ℕ) : Prop

Pathwise lower bound for a unit-cost AddWriterT computation.

theorem AddWriterT.queryBoundedAboveBy_pure {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] [LawfulMonad m] (x : α) : (pure x).QueryBoundedAboveBy 0

theorem AddWriterT.queryBoundedBelowBy_pure {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] [LawfulMonad m] (x : α) : (pure x).QueryBoundedBelowBy 0

theorem AddWriterT.queryBoundedAboveBy_monadLift {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] [LawfulMonad m] (x : m α) : (monadLift x).QueryBoundedAboveBy 0

theorem AddWriterT.queryBoundedBelowBy_monadLift {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] [LawfulMonad m] (x : m α) : (monadLift x).QueryBoundedBelowBy 0

theorem AddWriterT.queryBoundedAboveBy_mono {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {oa : AddWriterT ℕ m α} {n₁ n₂ : ℕ} (h : oa.QueryBoundedAboveBy n₁) (hn : n₁ ≤ n₂) : oa.QueryBoundedAboveBy n₂

theorem AddWriterT.queryBoundedBelowBy_mono {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {oa : AddWriterT ℕ m α} {n₁ n₂ : ℕ} (h : oa.QueryBoundedBelowBy n₂) (hn : n₁ ≤ n₂) : oa.QueryBoundedBelowBy n₁

theorem AddWriterT.queryBoundedAboveBy_addTell {m : Type → Type u_1} [Monad m] [HasEvalSet m] [LawfulMonad m] (w : ℕ) : (addTell w).QueryBoundedAboveBy w

theorem AddWriterT.queryBoundedBelowBy_addTell {m : Type → Type u_1} [Monad m] [HasEvalSet m] [LawfulMonad m] (w : ℕ) : (addTell w).QueryBoundedBelowBy w

theorem AddWriterT.queryBoundedAboveBy_map {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] [LawfulMonad m] {oa : AddWriterT ℕ m α} {n : ℕ} (f : α → β) (h : oa.QueryBoundedAboveBy n) : (f <$> oa).QueryBoundedAboveBy n

theorem AddWriterT.queryBoundedBelowBy_map {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] [LawfulMonad m] {oa : AddWriterT ℕ m α} {n : ℕ} (f : α → β) (h : oa.QueryBoundedBelowBy n) : (f <$> oa).QueryBoundedBelowBy n

theorem AddWriterT.queryBoundedAboveBy_bind {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] [LawfulMonad m] {oa : AddWriterT ℕ m α} {f : α → AddWriterT ℕ m β} {n₁ n₂ : ℕ} (h₁ : oa.QueryBoundedAboveBy n₁) (h₂ : ∀ (a : α), (f a).QueryBoundedAboveBy n₂) : (oa >>= f).QueryBoundedAboveBy (n₁ + n₂)

theorem AddWriterT.queryBoundedBelowBy_bind {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] [LawfulMonad m] {oa : AddWriterT ℕ m α} {f : α → AddWriterT ℕ m β} {n₁ n₂ : ℕ} (h₁ : oa.QueryBoundedBelowBy n₁) (h₂ : ∀ (a : α), (f a).QueryBoundedBelowBy n₂) : (oa >>= f).QueryBoundedBelowBy (n₁ + n₂)

theorem AddWriterT.queryBoundedAboveBy_fin_mOfFn {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] [LawfulMonad m] {n k : ℕ} {f : Fin n → AddWriterT ℕ m α} (h : ∀ (i : Fin n), (f i).QueryBoundedAboveBy k) : (Fin.mOfFn n f).QueryBoundedAboveBy (n * k)

theorem AddWriterT.queryBoundedBelowBy_fin_mOfFn {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] [LawfulMonad m] {n k : ℕ} {f : Fin n → AddWriterT ℕ m α} (h : ∀ (i : Fin n), (f i).QueryBoundedBelowBy k) : (Fin.mOfFn n f).QueryBoundedBelowBy (n * k)

def AddWriterT.QueryCostExactly {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] (oa : AddWriterT ℕ m α) (n : ℕ) : Prop

Pathwise exact cost for a unit-cost AddWriterT computation: every reachable execution carries exactly n unit queries.

theorem AddWriterT.QueryCostExactly.toAbove {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {oa : AddWriterT ℕ m α} {n : ℕ} (h : oa.QueryCostExactly n) : oa.QueryBoundedAboveBy n

theorem AddWriterT.QueryCostExactly.toBelow {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] {oa : AddWriterT ℕ m α} {n : ℕ} (h : oa.QueryCostExactly n) : oa.QueryBoundedBelowBy n

theorem AddWriterT.queryCostExactly_pure {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] [LawfulMonad m] (x : α) : (pure x).QueryCostExactly 0

theorem AddWriterT.queryCostExactly_monadLift {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] [LawfulMonad m] (x : m α) : (monadLift x).QueryCostExactly 0

theorem AddWriterT.queryCostExactly_addTell {m : Type → Type u_1} [Monad m] [HasEvalSet m] [LawfulMonad m] (w : ℕ) : (addTell w).QueryCostExactly w

theorem AddWriterT.queryCostExactly_map {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] [LawfulMonad m] {oa : AddWriterT ℕ m α} {n : ℕ} (f : α → β) (h : oa.QueryCostExactly n) : (f <$> oa).QueryCostExactly n

theorem AddWriterT.queryCostExactly_bind {m : Type → Type u_1} [Monad m] {α β : Type} [HasEvalSet m] [LawfulMonad m] {oa : AddWriterT ℕ m α} {f : α → AddWriterT ℕ m β} {n₁ n₂ : ℕ} (h₁ : oa.QueryCostExactly n₁) (h₂ : ∀ (a : α), (f a).QueryCostExactly n₂) : (oa >>= f).QueryCostExactly (n₁ + n₂)

theorem AddWriterT.queryCostExactly_fin_mOfFn {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSet m] [LawfulMonad m] {n k : ℕ} {f : Fin n → AddWriterT ℕ m α} (h : ∀ (i : Fin n), (f i).QueryCostExactly k) : (Fin.mOfFn n f).QueryCostExactly (n * k)

theorem AddWriterT.expectedCostNat_le_of_queryBoundedAboveBy {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalSPMF m] [LawfulMonad m] {oa : AddWriterT ℕ m α} {n : ℕ} (h : oa.QueryBoundedAboveBy n) : oa.expectedCostNat ≤ ↑n

theorem AddWriterT.expectedCostNat_ge_of_queryBoundedBelowBy {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalPMF m] [LawfulMonad m] {oa : AddWriterT ℕ m α} {n : ℕ} (h : oa.QueryBoundedBelowBy n) : ↑n ≤ oa.expectedCostNat

theorem AddWriterT.expectedCostNat_eq_of_queryCostExactly {m : Type → Type u_1} [Monad m] {α : Type} [HasEvalPMF m] [LawfulMonad m] {oa : AddWriterT ℕ m α} {n : ℕ} (h : oa.QueryCostExactly n) : oa.expectedCostNat = ↑n

def HasQuery.inRuntime {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} (oa : [HasQuery spec m] → m α) (runtime : QueryRuntime spec m) : m α

Instantiate a generic HasQuery computation in the concrete runtime runtime.

def HasQuery.withAddCost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] (oa : [HasQuery spec (AddWriterT ω m)] → AddWriterT ω m α) (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) : AddWriterT ω m α

Instantiate a generic HasQuery computation in the additive-cost instrumented runtime obtained from runtime.

def HasQuery.withUnitCost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] (oa : [HasQuery spec (AddWriterT ℕ m)] → AddWriterT ℕ m α) (runtime : QueryRuntime spec m) : AddWriterT ℕ m α

Instantiate a generic HasQuery computation in the unit-cost instrumented runtime obtained from runtime.

theorem HasQuery.hasCost_withAddCost_query {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] [LawfulMonad m] {ω : Type} [AddMonoid ω] (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) (t : spec.Domain) : (withAddCost (fun [HasQuery spec (AddWriterT ω m)] => query t) runtime costFn).HasCost (costFn t)

theorem HasQuery.queryBoundedAboveBy_withUnitCost_query {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] [LawfulMonad m] [HasEvalSet m] (runtime : QueryRuntime spec m) (t : spec.Domain) : (withUnitCost (fun [HasQuery spec (AddWriterT ℕ m)] => query t) runtime).QueryBoundedAboveBy 1

theorem HasQuery.queryBoundedBelowBy_withUnitCost_query {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] [LawfulMonad m] [HasEvalSet m] (runtime : QueryRuntime spec m) (t : spec.Domain) : (withUnitCost (fun [HasQuery spec (AddWriterT ℕ m)] => query t) runtime).QueryBoundedBelowBy 1

theorem HasQuery.queryCostExactly_withUnitCost_query {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] [LawfulMonad m] [HasEvalSet m] (runtime : QueryRuntime spec m) (t : spec.Domain) : (withUnitCost (fun [HasQuery spec (AddWriterT ℕ m)] => query t) runtime).QueryCostExactly 1

@[reducible, inline]

abbrev HasQuery.Computation {ι : Type} (spec : OracleSpec ι) (m : Type → Type u_2) (α : Type) : Type u_2

A computation generic over a HasQuery spec m capability.

def HasQuery.UsesCostAs {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) (f : α → ω) : Prop

Running oa in the additive-cost instrumentation of runtime yields an output-dependent cost described by f.

def HasQuery.UsesCostExactly {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) (w : ω) : Prop

Running oa in the additive-cost instrumentation of runtime incurs constant cost w.

def HasQuery.UsesCostAtMost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] [Preorder ω] [HasEvalSet m] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) (w : ω) : Prop

Running oa in the additive-cost instrumentation of runtime incurs cost at most w on every execution path. This is a semantic support bound, not merely an output-indexed cost description.

def HasQuery.UsesCostAtLeast {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] [Preorder ω] [HasEvalSet m] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) (w : ω) : Prop

Running oa in the additive-cost instrumentation of runtime incurs cost at least w on every execution path.

theorem HasQuery.usesCostAtMost_of_usesCostExactly {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] [HasEvalSet m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryRuntime spec m} {costFn : spec.Domain → ω} {w b : ω} (h : UsesCostExactly (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn w) (hwb : w ≤ b) : UsesCostAtMost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn b

theorem HasQuery.usesCostAtLeast_of_usesCostExactly {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] [HasEvalSet m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryRuntime spec m} {costFn : spec.Domain → ω} {w b : ω} (h : UsesCostExactly (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn w) (hbw : b ≤ w) : UsesCostAtLeast (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn b

theorem HasQuery.usesCostAtMost_query_of_le {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} [Monad m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] [HasEvalSet m] (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) (t : spec.Domain) {b : ω} (ht : costFn t ≤ b) : UsesCostAtMost (fun [HasQuery spec (AddWriterT ω m)] => query t) runtime costFn b

def HasQuery.UsesExactlyQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryRuntime spec m) (n : ℕ) : Prop

Unit-cost specialization: every query contributes cost 1.

def HasQuery.UsesAtMostQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSet m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryRuntime spec m) (n : ℕ) : Prop

Unit-cost specialization: every query contributes cost 1, with an upper bound.

def HasQuery.UsesAtLeastQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSet m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryRuntime spec m) (n : ℕ) : Prop

Unit-cost specialization: every query contributes cost 1, with a lower bound.

theorem HasQuery.usesAtMostQueries_of_usesExactlyQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] [HasEvalSet m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryRuntime spec m} {n b : ℕ} (h : UsesExactlyQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) (hnb : n ≤ b) : UsesAtMostQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime b

theorem HasQuery.usesAtLeastQueries_of_usesExactlyQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] [HasEvalSet m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryRuntime spec m} {n b : ℕ} (h : UsesExactlyQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) (hbn : b ≤ n) : UsesAtLeastQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime b

noncomputable def HasQuery.expectedQueryCost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] {ω : Type} [AddMonoid ω] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) (val : ω → ENNReal) : ENNReal

The expected weighted query cost of oa, instantiated in runtime and instrumented by costFn.

This is the primary expectation notion for generic HasQuery computations. It is computed from the additive cost marginal in the base monad's subdistribution semantics, valued by val.

The unit-cost query-counting notion [HasQuery.expectedQueries] is a specialization of this definition with costFn := fun _ ↦ 1 and val := fun n ↦ (n : ENNReal).

def HasQuery.queryCostDist {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] {ω : Type} [AddMonoid ω] (oa : Computation spec (AddWriterT ω m) α) (runtime : QueryRuntime spec m) (costFn : spec.Domain → ω) : m ω

The marginal distribution of weighted query costs induced by running oa in runtime with query-cost function costFn.

@[reducible, inline]

abbrev HasQuery.queryCountDist {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryRuntime spec m) : m ℕ

The marginal distribution of the unit-cost query count induced by running oa in runtime.

@[reducible, inline]

noncomputable abbrev HasQuery.expectedQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryRuntime spec m) : ENNReal

Expected number of oracle queries made by oa when run in runtime, counting each query with unit additive cost.

theorem HasQuery.expectedQueries_eq_tsum_tail_probs {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryRuntime spec m) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime = ∑' (i : ℕ), probEvent (queryCountDist (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime) fun (c : ℕ) => i < c

Tail-sum formula for the expected number of oracle queries made by oa in runtime:

E[number of queries] = ∑ i, Pr[i < number of queries].

This is the generic HasQuery version of [AddWriterT.expectedCostNat_eq_tsum_tail_probs].

theorem HasQuery.expectedQueries_le_tsum_of_tail_probs_le {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] (oa : Computation spec (AddWriterT ℕ m) α) (runtime : QueryRuntime spec m) {a : ℕ → ENNReal} (h : ∀ (i : ℕ), (probEvent (queryCountDist (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime) fun (c : ℕ) => i < c) ≤ a i) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime ≤ ∑' (i : ℕ), a i

Tail domination bounds expected query count.

If Pr[i < number of queries] ≤ a i for every i, then ExpectedQueries[ oa in runtime ] ≤ ∑ i, a i.

theorem HasQuery.expectedQueries_eq_sum_tail_probs_of_usesAtMostQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] [LawfulMonad m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryRuntime spec m} {n : ℕ} (h : UsesAtMostQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime = ∑ i ∈ Finset.range n, probEvent (queryCountDist (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime) fun (c : ℕ) => i < c

Finite tail-sum formula for expected query count under a pathwise upper bound.

If oa uses at most n oracle queries in every execution, then its expected query count is the finite sum of the probabilities that the query count exceeds i, for i < n.

theorem HasQuery.expectedQueryCost_le_of_usesCostAtMost {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryRuntime spec m} {costFn : spec.Domain → ω} {w : ω} {val : ω → ENNReal} (h : UsesCostAtMost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn w) (hval : Monotone val) : expectedQueryCost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn val ≤ val w

theorem HasQuery.expectedQueryCost_eq_tsum_outputs_of_usesCostAs {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] {ω : Type} [AddMonoid ω] [LawfulMonad m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryRuntime spec m} {costFn : spec.Domain → ω} {f : α → ω} {val : ω → ENNReal} (h : UsesCostAs (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn f) : expectedQueryCost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn val = ∑' (a : α), Pr[= a | (withAddCost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn).outputs] * val (f a)

theorem HasQuery.expectedQueries_le_of_usesAtMostQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalSPMF m] [LawfulMonad m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryRuntime spec m} {n : ℕ} (h : UsesAtMostQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime ≤ ↑n

theorem HasQuery.expectedQueryCost_ge_of_usesCostAtLeast {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalPMF m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryRuntime spec m} {costFn : spec.Domain → ω} {w : ω} {val : ω → ENNReal} (h : UsesCostAtLeast (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn w) (hval : Monotone val) : val w ≤ expectedQueryCost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn val

theorem HasQuery.expectedQueryCost_eq_of_usesCostExactly {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalPMF m] {ω : Type} [AddMonoid ω] [Preorder ω] [LawfulMonad m] {oa : Computation spec (AddWriterT ω m) α} {runtime : QueryRuntime spec m} {costFn : spec.Domain → ω} {w : ω} {val : ω → ENNReal} (h : UsesCostExactly (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn w) (hval : Monotone val) : expectedQueryCost (fun [HasQuery spec (AddWriterT ω m)] => oa) runtime costFn val = val w

theorem HasQuery.expectedQueries_ge_of_usesAtLeastQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalPMF m] [LawfulMonad m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryRuntime spec m} {n : ℕ} (h : UsesAtLeastQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) : ↑n ≤ expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime

theorem HasQuery.expectedQueries_eq_of_usesAtMostQueries_of_usesAtLeastQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalPMF m] [LawfulMonad m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryRuntime spec m} {n : ℕ} (hUpper : UsesAtMostQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) (hLower : UsesAtLeastQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime = ↑n

theorem HasQuery.expectedQueries_eq_of_usesExactlyQueries {ι : Type} {spec : OracleSpec ι} {m : Type → Type u_1} {α : Type} [Monad m] [HasEvalPMF m] [LawfulMonad m] {oa : Computation spec (AddWriterT ℕ m) α} {runtime : QueryRuntime spec m} {n : ℕ} (h : UsesExactlyQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime n) : expectedQueries (fun [HasQuery spec (AddWriterT ℕ m)] => oa) runtime = ↑n

def HasQuery.«termQueries[_In_]=_» : Lean.ParserDescr

Queries[ oa in runtime ] = n means that the generic HasQuery computation oa makes exactly n oracle queries when instantiated in runtime and instrumented with unit additive cost per query.

The computation oa is written in direct HasQuery style. The notation elaborates it against the unit-cost analysis monad induced by runtime, so statements can usually be written without explicit monad annotations such as m := AddWriterT ℕ m.

def HasQuery.«termQueries[_In_]≤_» : Lean.ParserDescr

Queries[ oa in runtime ] ≤ n means that every execution path of oa makes at most n oracle queries when run in the unit-cost instrumentation of runtime.

This packages the common cryptographic statement “the construction uses at most n queries” on top of [HasQuery.UsesAtMostQueries].

def HasQuery.«termQueries[_In_]≥_» : Lean.ParserDescr

Queries[ oa in runtime ] ≥ n means that every execution of oa in the unit-cost instrumentation of runtime incurs at least n query-cost units.

This is less common than the exact and upper-bound forms, but it is useful for statements saying that a construction must query the oracle at least a certain number of times.

def HasQuery.«termQueryCost[_In_]=_» : Lean.ParserDescr

QueryCost[ oa in runtime ] = n is the unit-cost specialization of weighted query cost: each oracle query contributes additive cost 1, so the total query cost is just the number of queries made by oa.

def HasQuery.«termQueryCost[_In_By_]=_» : Lean.ParserDescr

QueryCost[ oa in runtime by costFn ] = w means that oa, instantiated in runtime and instrumented so that each query t contributes cost costFn t, has constant total query cost w.

Use this when the cost model is not unit cost, for example when different query families or different query shapes carry different weights.

def HasQuery.«termQueryCost[_In_]≤_» : Lean.ParserDescr

QueryCost[ oa in runtime ] ≤ n is the unit-cost specialization of pathwise query-cost upper bounds. It says that every execution of oa makes at most n oracle queries.

def HasQuery.«termQueryCost[_In_By_]≤_» : Lean.ParserDescr

QueryCost[ oa in runtime by costFn ] ≤ w means that every execution path of oa has total query cost bounded above by w under the weighting function costFn.

This is the weighted analogue of [Queries[ oa in runtime ] ≤ n].

def HasQuery.«termQueryCost[_In_]≥_» : Lean.ParserDescr

QueryCost[ oa in runtime ] ≥ n is the unit-cost specialization of pathwise query-cost lower bounds. It says that every execution of oa makes at least n oracle queries.

def HasQuery.«termQueryCost[_In_By_]≥_» : Lean.ParserDescr

QueryCost[ oa in runtime by costFn ] ≥ w means that every execution path of oa has total query cost bounded below by w under the weighting function costFn.

This is the weighted analogue of [Queries[ oa in runtime ] ≥ n].

def HasQuery.«termExpectedQueryCost[_In_]» : Lean.ParserDescr

ExpectedQueryCost[ oa in runtime ] is the expected number of oracle queries made by oa when run in runtime, viewed as the unit-cost specialization of weighted expected query cost.

def HasQuery.«termExpectedQueryCost[_In_By_Via_]» : Lean.ParserDescr

ExpectedQueryCost[ oa in runtime by costFn via val ] is the expected weighted query cost of oa when instantiated in runtime.

Each query t contributes additive cost costFn t, and the total cost is then valued by val : ω → ENNReal before taking expectation. This is the primary expected-cost term for generic HasQuery constructions.

def HasQuery.«termExpectedQueries[_In_]» : Lean.ParserDescr

ExpectedQueries[ oa in runtime ] is the expected number of oracle queries made by oa when run in runtime, with each query carrying unit additive cost.

The result is an ℝ≥0∞ expectation, so it can be compared directly against natural-number bounds such as ExpectedQueries[ oa in runtime ] ≤ n.

This is the unit-cost specialization of [ExpectedQueryCost[ oa in runtime by costFn via val ]], with costFn := fun _ ↦ 1 and val := fun n ↦ (n : ENNReal).