feat(Query): query complexity framework with sorting examples

[kim-em]

This PR adds a FreeM-based framework for proving upper and lower bounds on query complexity. It incorporates and preserves the history of the earlier work in #372, together with subsequent design and review contributions discussed in the CSLib Algorithm frameworks thread.

A program is represented directly as FreeM F α, where F : Type u → Type v maps each query to its response type. The program is constructed independently of an oracle; evaluation supplies oracle responses only through lifted queries, while allowing later queries to depend on earlier responses.

The framework provides three universe-polymorphic interpreters, defined through FreeM.liftM:

• FreeM.eval evaluates a query program against an oracle.
• FreeM.countQueries counts the queries made along the oracle-determined execution path.
• FreeM.cost assigns query-dependent weights in an arbitrary additive monoid.

Pure computation is uncharged: costs attach only to lifted queries, so the interpreters measure query complexity. Counting is structural, derived from the program tree, rather than relying on trusted annotations as in a TimeM-style analysis. The FreeM module docstring includes a short recipe for setting up a new query type.

A caveat is that only operations represented by FreeM.lift are counted. If the intended oracle can be reconstructed from structure otherwise available to the program—for example, if its answers are determined by laws and computable using ordinary Lean definitions—an implementation may reimplement the oracle internally and avoid counted calls. The model is therefore strongest when oracle operations remain abstract. Parametric problems are less vulnerable: for example, an algorithm uniform over an arbitrary ring, with ring operations exposed only through ArithQuery, cannot generally reproduce those operations without issuing the corresponding queries. Parametricity alone is not sufficient if the same operations are also available directly through typeclass instances or other definitions.

Bounds and general lower-bound theorem

UpperBound and LowerBound express query bounds quantified over oracles. UpperBound.of_pointwise derives an upper bound from a per-input count bound and monotonicity of the bound function, and LowerBound.le_upperBound shows that a lower bound for a program never exceeds an upper bound for it.

The central combinatorial result is FreeM.exists_countQueries_ge_clog: if

• every query response type is finite and has cardinality at most r, and
• n oracles produce distinct results from a fixed program,

then some oracle forces the program to make at least ⌈log_r n⌉ queries.

The proof works directly on FreeM, without a separate fixed-response QueryTree datatype.

Sorting

The PR defines comparison queries LEQuery, a correctness specification IsSort, and query implementations of insertion sort and merge sort mirroring List.insertionSort and List.mergeSort exactly: eval_insertionSort and eval_mergeSort identify each program, evaluated against any oracle, with the corresponding standard-library function, so correctness (permutation, sortedness, and, for merge sort, stability) transfers from the existing API rather than being reproved. IsSort.eval_eq shows the specification pins down the behaviour: under any oracle implementing an antisymmetric total transitive relation, all correct comparison sorts produce the same output.

Proved bounds:

• insertion sort makes at most n * (n - 1) / 2 queries, a bound attained by the all-false oracle, with n² as a corollary;
• merge sort makes at most n * ⌈log₂ n⌉ queries;
• every correct comparison sort on an infinite type has worst-case query complexity at least ⌈log₂(n!)⌉, by constructing n! hidden total orders with distinct sorted outputs and applying the general FreeM lower-bound theorem;
• comparing merge sort's two bounds via LowerBound.le_upperBound yields the arithmetic fact ⌈log₂(n!)⌉ ≤ n * ⌈log₂ n⌉ with no further work.

Weighted-cost example

The arithmetic example demonstrates query-dependent costs using naive complex multiplication and Gauss's trick:

• naive multiplication has exact cost 4 * c_mul + 2 * c_add;
• Gauss's trick has exact cost 3 * c_mul + 5 * c_add;
• Gauss's trick is no more expensive exactly when 3 * c_add ≤ c_mul.

Upstream mirrors

Three general-purpose declarations are proposed upstream and kept private here until they land: List.mergeSort_append (leanprover/lean4#14995), Function.Injective.extend_sum_inl_inr (leanprover-community/mathlib4#43325), and the Std.Total (InvImage r f) instance (leanprover-community/mathlib4#43326).

Files

File	Contents
Query/FreeM.lean	Evaluation, query counting, weighted costs, the general lower-bound theorem, and the query-type recipe
Query/Bounds.lean	UpperBound, LowerBound, of_pointwise, le_upperBound
Query/Arith/{Defs,Lemmas}.lean	Parametric arithmetic costs and complex-multiplication example
Query/Sort/LEQuery.lean	Boolean comparison queries and their response-cardinality facts
Query/Sort/IsSort.lean	Correctness specification for comparison sorts and output uniqueness
Query/Sort/Insertion/{Defs,Lemmas}.lean	Insertion sort, agreement with List.insertionSort, triangular bound
Query/Sort/Merge/{Defs,Lemmas}.lean	Merge sort, agreement with List.mergeSort, n * ⌈log₂ n⌉ bound
Query/Sort/Merge/Bounds.lean	Combined merge sort bounds and the ⌈log₂(n!)⌉ ≤ n * ⌈log₂ n⌉ corollary
Query/Sort/LowerBound.lean	⌈log₂(n!)⌉ comparison-sorting lower bound
CslibTests/Query.lean	Executable checks and API examples

[Shreyas4991]

Another mistake in the descr :

This makes the framework suitable for query complexity, rather than general runtime analysis through explicit TimeM instrumentation.

The query combinator approach
allows as much structured general runtime analysis as TimeM. Unstructured (improperly ticked) use of TimeM is dangerous anyway. For algorithms and complexity there is no meaningful algorithm one could write in TimeM that one couldn't in Prog.

[Shreyas4991]

Parametricity alone is not sufficient if the same operations are also available directly through typeclass instances or other definitions

Not quite true. You can state correctness uniformly over a family of correct models. This is possible if this family of models is not a singleton and if different models may produce different outputs, as happens with sorting. It fails when the correct model is uniquely defined (as in determinants).

That being said, proving uniform correctness over a family of models is a bit overkill.

[eric-wieser]

I'm reasonably happy with this now, though let's wait for discussion to stop in the CSLib reviewer channel before finally merging.

I'd like to review the updates

[Shreyas4991]

I'm reasonably happy with this now, though let's wait for discussion to stop in the CSLib reviewer channel before finally merging.

@eric-wieser I was told there would be a discussion comparing #685 and #401 involving me. Why is it that this PR is being merged directly. It is still suboptimal in design. I have waited two three months for said discussion.

This was discussed in the cslib meetings.
Cc: @arademaker and @fmontesi

For the record I maintain that #685 should be merged. This PR (401) has done a good job of performing what amounts to a shallow copy of my work. However #372 (and #685) makes better design choices and has been battle tested. It has a better downstream track record.

It is also extremely dishonest to claim that subsequent reviews have improved it over #372. At best it is an inadequate approximation, with some minor changes that can be PRed back to #685 (successor of #372 which contains this PR's history, and was made at the maintainers' request).

[Shreyas4991]

Additionally I wish to note that in any sensible open source project that respects its contributors, a PR with this much overlap with a prior PR would be closed as a duplicate PR. The contributor would be asked to build on top of existing work. Senior members in particular wouldn’t scoop the work of junior members (with/without AI)

Even Google's AI knows this. I am sure a Claude user can figure this out :

https://share.google/aimode/h7o10KNuBhufnoDM0

[Shreyas4991]

What monad are you planning to use other than free monads?

[Shreyas4991]

This change you are applying you could be used to rewrite all monadic functions in all of lean and mathlib, including tactic monads and tactics in a monad polymorphic way. That doesn't mean one should. This is the design used by so-called mtl style transformers. It doesn't add anything meaningful here.

[Shreyas4991]

Another point : This doesn't scale for large and composite query models. It results in redundancy in parameters Explained here on zulip

[eric-wieser]

What monad are you planning to use other than free monads?

Id and PFunctor.FreeM are two natural choices; but you could equally do something silly like IO for a game where you ask the human to do the comparison, or perhaps some kind of LogM monad that records the comparisons as they happen.

Of course you can get here by starting with something in FreeM and using liftM, but my guess is that Lean's compiler cannot optimize this to anywhere near the same extent.

The actual motivation for this is to:

• present a pattern that allow algorithms to be written without CSLib, but then have their complexity proved downstream in CSLib
• allow monad-generic implementations to be proved lawful, in the sense that they are preserved under IsMonadHom (feat: add a predicate for monad morphisms #856).

[eric-wieser]

This change you are applying you could be used to rewrite all monadic functions in all of lean and mathlib,

See List.find/List.findM, List.any/List.anyM, etc; there is lots of precedent for already doing this.

including tactic monads and tactics in a monad polymorphic way

To some extend the functions written with [MonadEnv m] instead of CoreM are also opting into this pattern.

[eric-wieser]

Transitioning to PFunctor.FreeM is much simpler since PFunctor.FreeM generalizes FreeM.

I'd encourage you to start a Zulip thread comparing these. As I understand it, there are queries in FreeM that have no representation in PFunctor.FreeM and vice versa. I think this is not well-explained by the current docstring of PFunctor.FreeM, and it would be great to construct contrived or even plausible examples of each.

[Shreyas4991]

It's not true though.

1. FreeM and this MTL style approach are actually complementary. They are both separately used to compose multiple effects to achieve effectful programming.
2. Secondly to construct the interface, you would compose an existing queue type, an existing stack type, and an existing fibonacci heap type using direct sums, and use the composition lemmas for these. Writing a bespoke structure means we can't directly use those lemmas.

[Shreyas4991]

Transitioning to PFunctor.FreeM is much simpler since PFunctor.FreeM generalizes FreeM.

I'd encourage you to start a Zulip thread comparing these. As I understand it, there are queries in FreeM that have no representation in PFunctor.FreeM and vice versa. I think this is not well-explained by the current docstring of PFunctor.FreeM, and it would be great to construct contrived or even plausible examples of each.

Michael Sammler already explained how PFunctor.FreeM can express everything FreeM can but not vice versa. Quang Dao corrected it:

https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Free.20monad.20over.20a.20polynomial.20functor/near/584202846

[kim-em]

@eric-wieser, f6d8269

[Shreyas4991]

I wish to note that Eric and I discussed on Zulip that this change is orthogonal to the query combinator model and has been refactored to #861. Further we discussed that this change is of no use to algorithmic theory.

Given the amount of misunderstanding expressed by several people about this framework, this content only serves to obfuscate the above points to maintainers.