Lazy Random Oracle Equals Eager Full-Table Sampling

For an oracle specification D →ₒ R with a single constant range R, running an OracleComp (D →ₒ R) α under the lazy random oracle (OracleSpec.randomOracle, i.e. uniformSampleImpl.withCaching) has the same output distribution as the eager strategy: sample a full answer table f : D → R uniformly, then evaluate the computation deterministically against f via evalWithAnswerFn.

The lazy oracle samples a fresh uniform value on first query and caches it for consistency, so caching only ever affects repeated queries. Since every fresh table entry is uniform and independent, lazily sampling on demand is distributionally identical to pre-sampling the whole table. The marginalization lemma evalDist_uniformSample_bind_update is the workhorse: it absorbs each fresh on-demand uniform draw into the pre-sampled table.

Main results

• evalDist_simulateQ_randomOracle_run'_eq_tableExtending: the generalized, cache-parametrized form, the induction vehicle.
• evalDist_simulateQ_randomOracle_run'_empty_eq_uniformTable: the empty-cache corollary — the lazy-vs-eager equivalence proper.

@[reducible]

def OracleComp.tableExtending {D R : Type} (c : (OracleSpec.ofFn fun (x : D) => R).QueryCache) (g : D → R) : D → R

The total answer table obtained by overlaying a QueryCache on top of a full function table: cached entries take priority, uncached coordinates fall through to g.

theorem OracleComp.tableExtending_cacheQuery {D R : Type} [DecidableEq D] (c : (OracleSpec.ofFn fun (x : D) => R).QueryCache) (g : D → R) (t : D) (u : R) : tableExtending (c.cacheQuery t u) g = Function.update (tableExtending c g) t u

Overlaying c.cacheQuery t u on g is the t-update of overlaying c on g.

theorem OracleComp.tableExtending_update_of_none {D R : Type} [DecidableEq D] (c : (OracleSpec.ofFn fun (x : D) => R).QueryCache) (g : D → R) {t : D} (hc : c t = none) (u : R) : Function.update (tableExtending c g) t u = tableExtending c (Function.update g t u)

When t is uncached, updating the overlaid table at t equals overlaying the cache on the updated full table.

theorem OracleComp.evalDist_uniformSample_bind_update_map {D R : Type} [DecidableEq D] [Finite D] [Finite R] [Nonempty R] [SampleableType R] [SampleableType (D → R)] {α : Type} (t : D) (ψ : (D → R) → α) : 𝒟[do let u ← $ᵗ R let g ← $ᵗ (D → R) pure (ψ (Function.update g t u))] = 𝒟[do let g ← $ᵗ (D → R) pure (ψ g)]

Marginalization, post-composed. For any continuation ψ : (D → R) → α, drawing a fresh uniform u, then a full uniform table g, and evaluating ψ on Function.update g t u has the same distribution as evaluating ψ on a directly drawn uniform table.

theorem OracleComp.evalDist_simulateQ_randomOracle_run'_eq_tableExtending {D R : Type} [DecidableEq D] [Finite D] [Finite R] [Nonempty R] [SampleableType R] [SampleableType (D → R)] {α : Type} (oa : OracleComp (OracleSpec.ofFn fun (x : D) => R) α) (c : (OracleSpec.ofFn fun (x : D) => R).QueryCache) : 𝒟[(simulateQ OracleSpec.randomOracle oa).run' c] = 𝒟[do let g ← $ᵗ (D → R) pure (evalWithAnswerFn (QueryImpl.ofFn (tableExtending c g)) oa)]

Lazy random oracle equals eager full-table sampling — cache-parametrized form.

Running oa under the lazy random oracle starting from cache c yields the same output distribution as: sample a full table g : D → R uniformly, then evaluate oa deterministically against the table that overlays c on g.

This is the induction vehicle: the cache c is generalized so the query/bind step can recurse through cacheQuery.

theorem OracleComp.tableExtending_empty {D R : Type} (g : D → R) : tableExtending ∅ g = g

Overlaying the empty cache leaves a full table unchanged.

theorem OracleComp.evalDist_simulateQ_randomOracle_run'_empty_eq_uniformTable {D R : Type} [DecidableEq D] [Finite D] [Finite R] [Nonempty R] [SampleableType R] [SampleableType (D → R)] {α : Type} (oa : OracleComp (OracleSpec.ofFn fun (x : D) => R) α) : 𝒟[(simulateQ OracleSpec.randomOracle oa).run' ∅] = 𝒟[do let g ← $ᵗ (D → R) pure (evalWithAnswerFn (QueryImpl.ofFn g) oa)]

Lazy random oracle equals eager full-table sampling.

Running an OracleComp (D →ₒ R) α under the lazy random oracle from the empty cache yields the same output distribution as: sample a full answer table g : D → R uniformly, then evaluate the computation deterministically against g.

This is the empty-cache specialization of evalDist_simulateQ_randomOracle_run'_eq_tableExtending: the classic lazy-vs-eager-sampling equivalence. Lazy caching only affects repeated queries, and since each fresh table entry is uniform and independent, sampling on demand matches pre-sampling the whole table.