Verifying Time Complexity of Functions

Stream: new members

[Nilesh]

As an exercise, I wanted to do this:

I want to write a function that takes n : Nat as input and returns a List of String of the given size
But with some additional requirements:

a) n between 100 and 200 must not be accepted.
b) If n > 5, then the second element of the list must be "foo".
c) The implemented function's time complexity must not be higher than O(n).

The challenge is to get Lean to provably satisfy all of these requirements.

Discussing back and forth with an LLM, I came up with this implementation using a Monad to keep counting ticks for computational cost.

Is this a good / idiomatic solution? How would the experts accomplish this?

[Matt Diamond]

You might find this (very long) thread relevant: #CSLib > Proposal on Time Complexity @ 💬

[Shreyas Srinivas]

My opinion is that this is not a good solution. Even the paper that introduced it calls it a lightweight approach

[Shreyas Srinivas]

You can see my points in the thread many times. Roughly :

1. It leaves the model implicit and makes it possible to mix up different models.
2. It is not compositional. You have to explicitly mark each occurrence of the code you care about with a tick explicitly. There is, by definition, no notion of "correct" marking.
3. It is very easy to sneak in zero cost calls using pure, just discard the cost computation.
4. It does not allow reasoning about complexity relations between different standard/custom models and oracles.
5. It is a reviewing nightmare as algorithms get complex.

[Shreyas Srinivas]

It can however serve as a building block for a better solution

[Shreyas Srinivas]

Which I am working on. I'll finish it near the new year when I have time.

Btw, the explicit annotation (cost monad) based approach is easily two decades old. There is one POPL 2008 paper, though I am guessing it was already internal knowledge by then. Every newcomer to lean interested in doing complexity seems to rediscover it. You can save a few steps by defining the Time Monad as a Writer monad.