Paper on CSLib

Stream: CSLib

[Ching-Tsun Chou]

https://arxiv.org/abs/2602.04846

[Justin Asher]

Awesome to see the white paper released!

[Shreyas Srinivas]

Slight quibble, I think the TimeM is not identical to Mathlib’s writer monad directly since the Mathlib writer monad assumes that the w type is a multiplicative monoid, a very mathlib specific distinction. The writer monad has been around in Haskell for longer and is conceptually similar to Writer monad with AddMonoid attached to the logging type w.

[Shreyas Srinivas]

Something like WriterT (Multiplicative Nat). (Cc: @Eric Wieser told me about the Multiplicative declaration recently)

[Shreyas Srinivas]

And it is worth mentioning that TimeM is currently limited to Nat costs which I address in cslib#275

Finally the query based approach is definitely not “heavyweight”. It is a systematisation and strict generalisation of what TimeM does and would definitely qualify as “lightweight”. It just allows explicit specification what is being counted upfront, allows defining reductions between models, custom cost models, and allows lower bound proofs, and also surprisingly to me circuit complexity upper bounds. Keeping it lightweight is why Tanner suggested to put my combinator proposal into a Free monad.

[Shreyas Srinivas]

CC : Corresponding authors (help tag them please) :folded_hands:

[Eric Wieser]

Shreyas Srinivas said:

I think the TimeM is not identical to Mathlib’s writer monad directly since the Mathlib writer monad

This is why the wording is "akin to" not "exactly"

[Shreyas Srinivas]

Okay fair. I still think the second third point is worth fixing.

[Shreyas Srinivas]

Also whom should I tag for this?

[Shreyas Srinivas]

At least the classification of query models into the heavy weight side needs fixing, even if the rest of it is not explained. The current draft is factually wrong on that point.

[Swarat Chaudhuri]

I was going to post the paper here but you beat me to it! :-) @Shreyas Srinivas thanks for your thoughts. I will discuss a rewording with the other authors.

[Shreyas Srinivas]

Another thing. We had a really long chat about the pros and cons of the TimeM model and the query model on this channel. I see some content from there in the paper . I am guessing that channel topic needs to be cited or referenced somehow, though I am not sure how that would work (maybe a footnote? authors: CSLib Zulip community?)

[Shreyas Srinivas]

https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Proposal.20on.20Time.20Complexity/with/560640757

[Shreyas Srinivas]

I actually have a list linear search example and an ordered insertion example completed in CSLib#275. It might serve to illustrate this query model if you need a reference example.