FreeM: query/cost interpreters and lower-bound lemma

This file adds query-complexity interpreters to FreeM F α, where the type constructor F : Type u → Type v represents a query type mapping each query to its response type.

The key operations are:

• FreeM.eval oracle p: evaluate p by answering each query using oracle
• FreeM.countQueries oracle p: count queries along the oracle-determined path
• FreeM.cost oracle weight p: weighted query cost in any additive monoid

The program p must be fixed independently of oracle. Arbitrary pure computation embedded in p is uncharged, so countQueries and cost measure query complexity rather than total runtime. However, pure code cannot inspect oracle responses: those enter only through FreeM.lift.

This provides an alternative to the TimeM-based cost analysis in Cslib.Algorithms.Lean.MergeSort.MergeSort: here query counting is structural (derived from the FreeM tree) rather than annotation-based.

The combinatorial lower-bound lemma FreeM.exists_countQueries_ge_clog says: if n distinct oracles produce n distinct evaluation results from a program whose every response type has cardinality at most r, then some oracle makes at least ⌈log_r n⌉ queries. The proof uses the adversarial/partition argument: at each query node, the oracles split by their answer, and the largest fiber still produces distinct results in the corresponding subtree.

Setting up your own query type

1. Define an inductive Q : Type u → Type v whose constructors are the queries, indexed by their response types (see LEQuery, ArithQuery).
2. Wrap each constructor with FreeM.lift to obtain one-step programs (LEQuery.ask).
3. Write algorithms in do-notation as values of FreeM Q α.
4. Prove correctness by relating FreeM.eval to a reference implementation, and bounds by equational reasoning with the countQueries/cost simp lemmas; state them with Cslib.Query.UpperBound/Cslib.Query.LowerBound.

@[simp]

theorem Cslib.FreeM.timeMRet_liftM {F : Type u → Type v} {α : Type u} {T : Type t} [AddMonoid T] (interp : {ι : Type u} → F ι → Algorithms.Lean.TimeM T ι) (p : FreeM F α) : (FreeM.liftM (fun {ι : Type u} => interp) p).ret = (FreeM.liftM (fun {ι : Type u} (i : F ι) => pure (interp i).ret) p).run

TimeM.ret distributes across FreeM.liftM.

Interpreters

All three interpreters (eval, cost, countQueries) are defined as liftM interpretations into target monads, routing them through the universal property of the free monad rather than direct pattern-match on FreeM's constructors:

• eval interprets into Id.
• cost interprets into a TimeM accumulator monad (a value paired with a running cost in an arbitrary additive monoid).
• countQueries is cost with unit weight.

The pure and lift-then-bind simp lemmas (eval_pure, eval_liftBind, cost_pure, cost_liftBind, countQueries_pure, countQueries_liftBind) all reduce by rfl, giving the same proof ergonomics as direct pattern-match definitions while honouring the universal property as the primary abstraction.

def Cslib.FreeM.eval {F : Type u → Type v} {α : Type u} (oracle : {ι : Type u} → F ι → ι) (p : FreeM F α) : α

Evaluate a program by answering each query using oracle. Defined as liftM to Id, the canonical interpreter into pure values.

Equations

• Cslib.FreeM.eval oracle p = (Cslib.FreeM.liftM (fun {ι : Type ?u.2} (i : F ι) => pure (oracle i)) p).run

def Cslib.FreeM.cost {F : Type u → Type v} {α : Type u} {T : Type t} [AddMonoid T] (oracle : {ι : Type u} → F ι → ι) (weight : {ι : Type u} → F ι → T) (p : FreeM F α) : T

Weighted query cost in an additive monoid: each query has a cost given by weight, accumulated along the oracle-determined path. Defined as liftM into TimeM.

Equations

• Cslib.FreeM.cost oracle weight p = (Cslib.FreeM.liftM (fun {ι : Type ?u.3} (op : F ι) => { ret := oracle op, time := weight op }) p).time

def Cslib.FreeM.countQueries {F : Type u → Type v} {α : Type u} (oracle : {ι : Type u} → F ι → ι) (p : FreeM F α) : ℕ

Count the number of queries along the path determined by oracle.

This is deliberately a def with its own simp lemmas, rather than an abbreviation for cost oracle (fun _ => 1), so that goals display countQueries.

Equations

• Cslib.FreeM.countQueries oracle p = Cslib.FreeM.cost (fun {ι : Type ?u.2} => oracle) (fun {ι : Type ?u.2} (x : F ι) => 1) p

Simp lemmas for eval

@[simp]

theorem Cslib.FreeM.eval_pure {F : Type u → Type v} {α : Type u} (oracle : {ι : Type u} → F ι → ι) (a : α) : eval (fun {ι : Type u} => oracle) (pure a) = a

@[simp]

theorem Cslib.FreeM.eval_liftBind {F : Type u → Type v} {α : Type u} (oracle : {ι : Type u} → F ι → ι) {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : eval (fun {ι : Type u} => oracle) (lift op >>= cont) = eval (fun {ι : Type u} => oracle) (cont (oracle op))

@[simp]

theorem Cslib.FreeM.eval_lift {F : Type u → Type v} (oracle : {ι : Type u} → F ι → ι) {ι : Type u} (op : F ι) : eval (fun {ι : Type u} => oracle) (lift op) = oracle op

@[simp]

theorem Cslib.FreeM.eval_bind {F : Type u → Type v} {α β : Type u} (oracle : {ι : Type u} → F ι → ι) (t : FreeM F α) (f : α → FreeM F β) : eval (fun {ι : Type u} => oracle) (t >>= f) = eval (fun {ι : Type u} => oracle) (f (eval (fun {ι : Type u} => oracle) t))

@[simp]

theorem Cslib.FreeM.eval_map {F : Type u → Type v} {α β : Type u} (oracle : {ι : Type u} → F ι → ι) (t : FreeM F α) (f : α → β) : eval (fun {ι : Type u} => oracle) (f <$> t) = f (eval (fun {ι : Type u} => oracle) t)

theorem Cslib.FreeM.isMonadHom_pure_eval {F : Type u → Type v} (oracle : {ι : Type u} → F ι → ι) : IsMonadHom (FreeM F) Id fun {α : Type u} (x : FreeM F α) => pure (eval (fun {ι : Type u} => oracle) x)

Simp lemmas for cost

@[simp]

theorem Cslib.FreeM.cost_pure {F : Type u → Type v} {α : Type u} {T : Type t} [AddMonoid T] (oracle : {ι : Type u} → F ι → ι) (weight : {ι : Type u} → F ι → T) (a : α) : cost (fun {ι : Type u} => oracle) (fun {ι : Type u} => weight) (pure a) = 0

@[simp]

theorem Cslib.FreeM.cost_liftBind {F : Type u → Type v} {α : Type u} {T : Type t} [AddMonoid T] (oracle : {ι : Type u} → F ι → ι) (weight : {ι : Type u} → F ι → T) {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : cost (fun {ι : Type u} => oracle) (fun {ι : Type u} => weight) (lift op >>= cont) = weight op + cost (fun {ι : Type u} => oracle) (fun {ι : Type u} => weight) (cont (oracle op))

@[simp]

theorem Cslib.FreeM.cost_lift {F : Type u → Type v} {T : Type t} [AddMonoid T] (oracle : {ι : Type u} → F ι → ι) (weight : {ι : Type u} → F ι → T) {ι : Type u} (op : F ι) : cost (fun {ι : Type u} => oracle) (fun {ι : Type u} => weight) (lift op) = weight op

@[simp]

theorem Cslib.FreeM.cost_bind {F : Type u → Type v} {α β : Type u} {T : Type t} [AddMonoid T] (oracle : {ι : Type u} → F ι → ι) (weight : {ι : Type u} → F ι → T) (t : FreeM F α) (f : α → FreeM F β) : cost (fun {ι : Type u} => oracle) (fun {ι : Type u} => weight) (t >>= f) = cost (fun {ι : Type u} => oracle) (fun {ι : Type u} => weight) t + cost (fun {ι : Type u} => oracle) (fun {ι : Type u} => weight) (f (eval (fun {ι : Type u} => oracle) t))

@[simp]

theorem Cslib.FreeM.cost_map {F : Type u → Type v} {α β : Type u} {T : Type t} [AddMonoid T] (oracle : {ι : Type u} → F ι → ι) (weight : {ι : Type u} → F ι → T) (t : FreeM F α) (f : α → β) : cost (fun {ι : Type u} => oracle) (fun {ι : Type u} => weight) (f <$> t) = cost (fun {ι : Type u} => oracle) (fun {ι : Type u} => weight) t

Simp lemmas for countQueries

@[simp]

theorem Cslib.FreeM.countQueries_pure {F : Type u → Type v} {α : Type u} (oracle : {ι : Type u} → F ι → ι) (a : α) : countQueries (fun {ι : Type u} => oracle) (pure a) = 0

@[simp]

theorem Cslib.FreeM.countQueries_liftBind {F : Type u → Type v} {α : Type u} (oracle : {ι : Type u} → F ι → ι) {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : countQueries (fun {ι : Type u} => oracle) (lift op >>= cont) = 1 + countQueries (fun {ι : Type u} => oracle) (cont (oracle op))

@[simp]

theorem Cslib.FreeM.countQueries_lift {F : Type u → Type v} (oracle : {ι : Type u} → F ι → ι) {ι : Type u} (op : F ι) : countQueries (fun {ι : Type u} => oracle) (lift op) = 1

@[simp]

theorem Cslib.FreeM.countQueries_bind {F : Type u → Type v} {α β : Type u} (oracle : {ι : Type u} → F ι → ι) (t : FreeM F α) (f : α → FreeM F β) : countQueries (fun {ι : Type u} => oracle) (t >>= f) = countQueries (fun {ι : Type u} => oracle) t + countQueries (fun {ι : Type u} => oracle) (f (eval (fun {ι : Type u} => oracle) t))

@[simp]

theorem Cslib.FreeM.countQueries_map {F : Type u → Type v} {α β : Type u} (oracle : {ι : Type u} → F ι → ι) (t : FreeM F α) (f : α → β) : countQueries (fun {ι : Type u} => oracle) (f <$> t) = countQueries (fun {ι : Type u} => oracle) t

theorem Cslib.FreeM.countQueries_eq_cost_one {F : Type u → Type v} {α : Type u} (oracle : {ι : Type u} → F ι → ι) (p : FreeM F α) : countQueries (fun {ι : Type u} => oracle) p = cost (fun {ι : Type u} => oracle) (fun {ι : Type u} (x : F ι) => 1) p

@[simp]

theorem Cslib.FreeM.countQueries_ite {F : Type u → Type v} {α : Type u} (oracle : {ι : Type u} → F ι → ι) (P : Prop) [Decidable P] (p q : FreeM F α) : countQueries (fun {ι : Type u} => oracle) (if P then p else q) = if P then countQueries (fun {ι : Type u} => oracle) p else countQueries (fun {ι : Type u} => oracle) q

@[simp]

theorem Cslib.FreeM.countQueries_dite {F : Type u → Type v} {α : Type u} (oracle : {ι : Type u} → F ι → ι) (P : Prop) [Decidable P] (p : P → FreeM F α) (q : ¬P → FreeM F α) : countQueries (fun {ι : Type u} => oracle) (if h : P then p h else q h) = if h : P then countQueries (fun {ι : Type u} => oracle) (p h) else countQueries (fun {ι : Type u} => oracle) (q h)

Combinatorial lower bound

theorem Cslib.FreeM.exists_countQueries_ge_clog {F : Type u → Type v} {α : Type u} (r : ℕ) (h_card : ∀ {ρ : Type u} (a : F ρ), Cardinal.mk ρ ≤ ↑r) (p : FreeM F α) {n : ℕ} (oracles : Fin n → {ρ : Type u} → F ρ → ρ) (hn : 0 < n) (h_inj : Function.Injective fun (i : Fin n) => eval (fun {ι : Type u} => oracles i) p) : ∃ (i : Fin n), countQueries (fun {ι : Type u} => oracles i) p ≥ Nat.clog r n

If n oracles produce n distinct evaluation results from a FreeM F α program whose every response type has cardinality at most r (and hence is finite), then some oracle makes at least ⌈log_r n⌉ queries.

This is the core combinatorial lemma for query complexity lower bounds. The proof uses the adversarial/partition argument: at each query node, the n oracles split by their answer; the largest group (size ≥ ⌈n/r⌉) still produces distinct results in the corresponding subtree, and the induction proceeds there.