Complexity theory

Stream: Is there code for X?

[Martin Dvořák]

Hello! Has anything from Complexity theory already been formalized in Lean? I have just found Computability (in the mathlib library).

I'd like to do a Ph.D. on formalizing Complexity theory in Lean — probably from scratch; however, if there was something already done, I might want to build on top of that instead.

[Anne Baanen]

I'm not aware of any complexity theory in Lean. You might be interested in the recent papers on complexity theory in Coq via the λ calculus: https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13915 https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13914

[Mario Carneiro]

The existing material on computability was written with an eye for complexity theory (and it is mentioned as future work and motivation in the paper), but not much in that direction has landed yet. I think @Pim Spelier has some unmerged complexity theory work on P and NP

[Mario Carneiro]

see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Computability.2C.20P.20.28and.20NP.29

[Martin Dvořák]

Very exciting! I'll have a look at it after I learn the basics.

[david]

Has there been some thought on proving time complexity bound for algorithms?
For example, say my task is sorting. And we have different algorithms, insertion sort, quick sort, ...
We care about 2 things:

1. the algorithm solves the task
2. the algorithm runs in O(T).

Is there a framework / examples to describe these ideas?

(extension) We may care about different computation model (e.g. turing machine, random access, ...) in the future.

[Eric Wieser]

docs#list.sorted_merge_sort is an example of "1."

[Eric Wieser]

Note that since docs#funext declares functions equal if their values are equal, you cannot make proofs about "complexity" of functions by any metric. Instead, you can define a copy of your sort function to return something like (sorted_list, num_accesses) (or write a metaprogram to generate a function that does that!) and translate statements about complexity to statements about num_accesses.

[david]

Thank you! That sounds like a great idea, I will think about it. I think these tools will be useful and necessary when lean expands into the theoretical computer science world!

[Aporías]

Did you start working on this? Is anyone working on formalizing complexity theory?

[Yuyang Zhao]

There are some related open PRs, you can search on GitHub. See also this topic.

[Andrew Carter]

I put together some code following @Eric Wieser suggestion for multiplication (I ended up with a monad instead),
I was originally going to code through Karatsuba but stopped at traditional multiply instead (too much algebra - I probably need to get more experience with tactics - simp/ring/linarith don't seem to be cutting it),
https://github.com/calcu16/lean_complexity/tree/main/src.

I think my main concern is that ideally we'd just have to read the proposition of the correct value and cost of any function (in my case traditional_multiply_value and traditional_multiply_cost) to know that the function does what its supposed to do and that it has a certain complexity. But in this case you have to read the entire definition of traditional_multiply to make sure no funny business happens (this is in contrast to using turing machines or partrec definitions where I think we can be confident of the algorithm if we assume the machine definition is sound).

[Shreyas Srinivas]

Is there an encoding of asymptotic analysis in lean?

[Shreyas Srinivas]

I suspect that this would be

1. A prerequisite
2. Achievable

[Mario Carneiro]

docs#asymptotics.is_O

[Martin Dvořák]

I am not sure about the "prerequisite" part. I think we should first implement a model that counts steps exactly, to have a solid definition.

[Shreyas Srinivas]

I am writing as I think here, so please bear with me:
With my CS theory hat on, usually we don't seem to "count" per se. We have some algorithms with their respective complexities and then we compose them to get other algorithms of other complexities. But both this, and the counting you suggest have similar requirements. You have some operations, with certain input parameters and computational complexities in terms of those input parameters. There are certain ways of combining them (conditionals, loops, recursion etc). The complexity of the resultant operation is determined by the type of composition.

[Shreyas Srinivas]

Importantly the cost of various operations is specific to the model.

[Shreyas Srinivas]

There are a gazillion models out there

[Shreyas Srinivas]

And depending on what sort of complexity theory you do, the model matters to differing degrees.

[Shreyas Srinivas]

For example, fine-grained complexity people won't be happy with polynomial factors that, say, the NP-Completeness might not care about. Distributed algorithms people might care deeply about polylog factors.

[Shreyas Srinivas]

I wonder if building a DSL for pseudocode, tagged with input parameter sizes and complexity expressions is the way to go? It might be the most intuitive for the algorithms and complexity people, plus we might avoid having to actually execute the computations

[Martin Dvořák]

Shreyas Srinivas said:

(...) There are certain ways of combining them (conditionals, loops, recursion etc). The complexity of the resultant operation is determined by the type of composition.

It will be crucial to design a model of computation that allows "combining them". Usually, in computer science, we employ a lot of arguments like "and then we run algorithm A on the segment between # and $ and store the result on the ends of the tape" which are amazing for handwaving but extremely tedious to formalize.

[Martin Dvořák]

Shreyas Srinivas said:

Importantly the cost of various operations is specific to the model.

Yes. And it is important to have a concrete model.

[Martin Dvořák]

Shreyas Srinivas said:

There are a gazillion models out there

It will be really important to choose the right one. If we choose something that's cumbersome to work with, we will end up writing hundreds of thousands of lines extra.

[Martin Dvořák]

Shreyas Srinivas said:

For example, fine-grained complexity people won't be happy with polynomial factors that, say, the NP-Completeness might not care about. Distributed algorithms people might care deeply about polylog factors.

Yeah. That is another reason why we should start with exact counting of computation steps. Later we can decide what factors we ignore.

[Martin Dvořák]

Shreyas Srinivas said:

I wonder if building a DSL for pseudocode, tagged with input parameter sizes and complexity expressions is the way to go? It might be the most intuitive for the algorithms and complexity people, plus we might avoid having to actually execute the computations

Keep in mind that the most difficult thing is to reason about computation, not to implement stuff and execute programs. I cannot imagine pseudocode would help us.

[Martin Dvořák]

Martin Dvořák said:

I am not sure about the "prerequisite" part. I think we should first implement a model that counts steps exactly, to have a solid definition.

As a computer-science student, I truly appreciate complexity classes that are agnostic to the programming language / model of computation. However, we have to be really precise here. We should choose one model, define the time (and space) complexity exactly, and build a good API over it.

[Martin Dvořák]

Later we can introduce other models and show in which sense they are equivalent.

[Shreyas Srinivas]

Martin Dvořák said:

Shreyas Srinivas said:

(...) There are certain ways of combining them (conditionals, loops, recursion etc). The complexity of the resultant operation is determined by the type of composition.

It will be crucial to design a model of computation that allows "combining them". Usually, in computer science, we employ a lot of arguments like "and then we run algorithm A on the segment between # and $ and store the result on the ends of the tape" which are amazing for handwaving but extremely tedious to formalize.

I think a very basic DSL can do much of this. The basic operations are : creating new identifiers, assigning to identifiers, arithematic and logic, conditionals, and loops. Then for correctness we use the hoare triplets approach which can be implemented as refinement types (which is possible in lean).

[Shreyas Srinivas]

Then comes procedure calls . Then finally, (mu?)-recursion

[Shreyas Srinivas]

This should give us the RAM model at the very least. Proving equivalences can be non-trivial to impossible (think LOCAL model, which allows undecidable local computations at each node, with say, RAM).

[Mario Carneiro]

I think it is more important to get a model that works without the sugar... the DSL part is not the hard part but it is a large investment so either it needs to work on a wide spectrum of models or we need to make one model which has all the properties we want

[Shreyas Srinivas]

Mario Carneiro said:

I think it is more important to get a model that works without the sugar... the DSL part is not the hard part but it is a large investment so either it needs to work on a wide spectrum of models or we need to make one model which has all the properties we want

I think that is a non-starter. There are just too many models, completely incompatible in many cases. If there is one model that can be considered conceptually basic, it would be the RAM model.

[Mario Carneiro]

hence why I don't think the DSL should be the focus

[Shreyas Srinivas]

RAM model for the more algorithmy bits of complexity and Turing machine for the foundational results.

[Mario Carneiro]

Note that the turing_machine.lean file alone defines 3 different computational models, and there are a couple more in other files

[Mario Carneiro]

the ratio of programs to models is way too low for a DSL to be a worthwhile investment

[Mario Carneiro]

the only model which has enough written in it to be worth having more sugar in mathlib is primrec and/or partrec (even here, there is a split...)

[Shreyas Srinivas]

Mario Carneiro said:

hence why I don't think the DSL should be the focus

Beyond foundational computability + complexity (and some hierarchy) results, trying to do TCS in Turing machines is probably not meaningful.

[Mario Carneiro]

Have you actually looked at the file

[Mario Carneiro]

But it's true that TM-based models are not suitable for complexities tighter than P, because there is too much translation overhead

[Mario Carneiro]

Do you have a reference which defines a complexity model rigorously? They seem to be very hard to come by

[Shreyas Srinivas]

Well, there is the Barak-Arora textbook, freely available online. I tried looking up complexity zoo. It seems to be down.

[Mario Carneiro]

BTW, if we are going to write a DSL for writing programs, the most obvious choice of language is Lean itself

[Mario Carneiro]

Shreyas Srinivas said:

Well, there is the Barak-Arora textbook, freely available online. I tried looking up complexity zoo. It seems to be down.

https://users.cs.duke.edu/~reif/courses/complectures/books/AB/ABbook.pdf I guess?

[Shreyas Srinivas]

Mario Carneiro said:

BTW, if we are going to write a DSL for writing programs, the most obvious choice of language is Lean itself

This occurred to me at first. I see two challenges:

1. The typical theory paper is written in imperative style pseudo code. That's what most theorists understand.
2. I am trying to avoid performing the actual computation, and just build an expression tree with the relevant proofs and complexities.

[Mario Carneiro]

You can write imperative style code in lean too you know

[Shreyas Srinivas]

Mario Carneiro said:

You can write imperative style code in lean too you know

Yes, but then it is actually executed.

[Mario Carneiro]

??

[Shreyas Srinivas]

Most theory people don't care about the fine-grained aspects of getting an algorithm to run

[Mario Carneiro]

This is for modeling purposes, you don't have to call the function if you don't want to

[Mario Carneiro]

but the fact that the lean function functions as its own denotational semantics is immensely useful in this context

[Shreyas Srinivas]

What I mean is that, for example a theorist might be happy to leave several implementation details unspecified.

[Mario Carneiro]

I don't think that the fact that lean programs are also compiled is a downside here... it is at most a neutral thing

[Mario Carneiro]

you can put noncomputable if you really don't want the compiler to even contemplate compiling it, but... why?

[Mario Carneiro]

it helps to test the function in #eval in any case

[Martin Dvořák]

Shreyas Srinivas said:

What I mean is that, for example a theorist might be happy to leave several implementation details unspecified.

Are you serious? You want to formally prove properties of programs that are so informal that you could not even execute them?

[Shreyas Srinivas]

Mario Carneiro said:

you can put noncomputable if you really don't want the compiler to even contemplate compiling it, but... why?

Martin Dvořák said:

Shreyas Srinivas said:

What I mean is that, for example a theorist might be happy to leave several implementation details unspecified.

Are you serious? You want to formally prove properties of programs that are so informal that you could not even execute them?

Welcome to theoretical CS :sweat_smile: :sweat_smile:

[Mario Carneiro]

Shreyas Srinivas said:

What I mean is that, for example a theorist might be happy to leave several implementation details unspecified.

Also, this is a formal theorem prover we're talking about here. Specifying the unspecified implementation details is exactly what we do

[Mario Carneiro]

I fully expect a large part of the work to be figuring out all the gaps left by the informal mathematician

[Shreyas Srinivas]

Producing an implementable version of a theoretically proposed algorithm can be a challenge in and of itself: for example consider this:
https://link.springer.com/content/pdf/10.1007/BF01940648.pdf:
"We conclude that there is no published correct presentation of the embedding phase of the
Hopcroft and Tarjan algorithm. ". This refers to the paper here (https://dl.acm.org/doi/pdf/10.1145/321850.321852) and Hopcroft's book

[Martin Dvořák]

It seems to me that you @Shreyas Srinivas are aiming for some really inconvenient trade-offs.

[Martin Dvořák]

If you can't even implement the algorithm, forget about verifying it formally.

[Shreyas Srinivas]

I am trying to point out that algorithm engineering is different from algorithm design

[Martin Dvořák]

You can ship your informal pseudocode with an informal proof of its time complexity. You correctly observe that theorists do it all the time.

[Martin Dvořák]

However, for a formal proof of time complexity, having a formal implementation of the program is a basic need.

[Shreyas Srinivas]

Which is why counting minutiae might lead us astray. It is still possible to prove things at a sufficiently high level of abstraction. For example, an algorithm might say : explore the graph this way, construct such and such partition, and do something on the subgraphs. We might know the properties of the input/output of each of these steps.

[Shreyas Srinivas]

Then we might be able to prove meaningful things about the properties of the algorithm as a whole, without going too deep into specifics. This is also why a DSL might be helpful

[Shreyas Srinivas]

It might allow us to introduce adhoc routines of specific complexities and properties.

[Mario Carneiro]

I agree with Martin that it is not reasonable to consider high level reasoning about complexity without the ability to give overly precise step counting results first

[Mario Carneiro]

of course we'd like to be able to blur the results to something more asymptotic, but this is a research question all on its own because the standard techniques of is_O don't quite apply when it's not clear what is being held fixed and what is existentially quantified

[Shreyas Srinivas]

I agree with that in the sense that, fundamental complexity results do require a lot of intricate counting with turing machines. For example, if we prove the first four chapters of the Barak-Arora book, this would already be a significant step forward.

[Mario Carneiro]

I'm saying that even for the high level results where you just want a basic estimate, you can't even do that unless you have a precise definition of what you are estimating

[Patrick Johnson]

Mario Carneiro said:

https://users.cs.duke.edu/~reif/courses/complectures/books/AB/ABbook.pdf I guess?

It's just a book draft. The full book is longer and has many serious mistakes fixed. If anyone wants the full book in PDF, or any other paper or book regarding complexity theory, I'm happy to share.

[Shreyas Srinivas]

Hmm.. okay. that might be true, but then we would be in the world of an exploding number of models.

[Mario Carneiro]

and moreover, an issue that comes up fairly frequently IME is that if you try to bundle results in an existential too early, you have to go back and fix the proofs later when it turns out that you need to know that this constant C is not just fixed over x but also over n, or over some other parameter k you didn't think was going to vary

[Mario Carneiro]

the only way that I know to avoid that issue is to just say it's less than 2|x|^2 + 100 and be done with it

[Mario Carneiro]

(that doesn't have to be a precise bound either, but it's formally easy to see that 2 doesn't depend on n or k or anything else)

[Shreyas Srinivas]

Mario Carneiro said:

I'm saying that even for the high level results where you just want a basic estimate, you can't even do that unless you have a precise definition of what you are estimating

Question : How would this counting work: I imagine that I have procedure A which has time complexity f(n) and procedure B with complexity g(n). Then a sequential_compose A B might have complexity f(|x|) + g(|A(x)|). To me it seems like we don't need to run the algorithm and explicitly count the number of steps to achieve this. There are certain other kinds of compositions, but depending on the model, maybe not too many.

[Mario Carneiro]

I'm not sure what you are talking about by "explicitly running the algorithm"

[Mario Carneiro]

that's just a basic theorem about the cost model

[Shreyas Srinivas]

Exactly. so, I just need to carry this proof forward when I compose procedures together. Not perform them, carrying out each step and carrying their data around. So the "procedures" need not be executable

[Shreyas Srinivas]

In fact they could just be stubs.

[Mario Carneiro]

One thing that is important though is that A has time complexity bounded by an actual function f(n) (like 14 * (n+1)^2), not an existentially quantified function, in order to run that argument

[Mario Carneiro]

otherwise you have to add some existential unpacking steps in there and it can get tricky to automate that in such a way that the relevant parameters are generalized

[Mario Carneiro]

Shreyas Srinivas said:

Exactly. so, I just need to carry this proof forward when I compose procedures together. Not perform them, carrying out each step and carrying their data around. So the "procedures" need not be executable

The procedures do not need to be executable, but it's not like that's a negative thing that drags on the formalization

[Mario Carneiro]

But they do need to be precisely defined

[Mario Carneiro]

and they need to have a fixed denotation

[Mario Carneiro]

and it turns out that lean functions are one way to define the denotation of an algorithm

[Mario Carneiro]

so for example you might prove that eval (sequential_compose A B) = eval B ∘ eval A using lean's ∘ for sequential composition

[Shreyas Srinivas]

okay, maybe I misunderstood what you mean by counting each step: when I think of counting individual steps, I picture, say a merge sort implementation that, for each input, tells me how many swaps it did. Or some recursive procedure with the time complexity T(n), that explicitly computes the recursion until reaching the stopping condition.

[Mario Carneiro]

the procedure itself isn't doing the counting, we are doing the counting by analyzing what the procedure does

[Mario Carneiro]

although I have seen some formalizations that bake the counting into the procedure itself by embedding it in a "step-counting monad"

[Mario Carneiro]

this feels like a bit of a cheat to me though, since you don't have to call the tick function if you don't want to

[Mario Carneiro]

I think what we want is some type prog of programs in a given computational model, and the cost model and execution semantics defined by a predicate evals_in (p : prog) x n a which says that p evaluates x to a in n steps. Then there are a bunch of things you can build on top to make that easier to use and compose

[Martin Dvořák]

Mario Carneiro said:

this feels like a bit of a cheat to me though, since you don't have to call the tick function if you don't want to

I fully agree with this opinion. If we rely on the programmer to call tick with every operation, we can have a proof that "algorithm A has a time complexity f(n) assuming that the implementation is done well", but we can never prove that "problem X has a time complexity f(n)".

[Shreyas Srinivas]

Mario Carneiro said:

I think what we want is some type prog of programs in a given computational model, and the cost model and execution semantics defined by a predicate evals_in (p : prog) x n a which says that p evaluates x to a in n steps. Then there are a bunch of things you can build on top to make that easier to use and compose

With the important addition that there is usually more than one parameter.

[Mario Carneiro]

BTW I looked a bit at the A-B book but I'm not sure if there is something you think is particularly good in there. I'm seeing a lot about P and NP stuff and turing machines suffice for that (and given the tone of the first part of the book I don't expect it to be very helpful about choosing a good computational model)

[Mario Carneiro]

there are no parameters in that example, I'm not sure what you mean?

[Shreyas Srinivas]

A statement on graphs : depth-first-search runs on a graph G in O(|G.V| + |G.E|) steps

[Shreyas Srinivas]

usually |G.V| and |G.E| are treated as independent parameters (denoted n and m for example)

[Shreyas Srinivas]

Mario Carneiro said:

BTW I looked a bit at the A-B book but I'm not sure if there is something you think is particularly good in there. I'm seeing a lot about P and NP stuff and turing machines suffice for that (and given the tone of the first part of the book I don't expect it to be very helpful about choosing a good computational model)

Its first few chapters deal with the TM model, but it also introduces circuits towards the end of part 1. Later it introduces interactive proofs, decision trees, communication complexity, algebraic complexity etc.

[Mario Carneiro]

evals_in is a very low level primitive, you wouldn't use it for that statement. But after desugaring, a theorem like that would take the form:

\exists C,
\forall x,
x \in graph m n ->
evals_in depth-first-search x (c * (m + n + 1)) (DFS_result x)

[Mario Carneiro]

yeah, I saw the circuits. Circuits are "fun" since they are non-inductive

[Mario Carneiro]

None of them really sounds like a general purpose computational model though, such as you might use to execute pseudocode style programs you see in the textbooks

[Shreyas Srinivas]

That would be the RAM model. You would find it an algorithms book (Mehlhorn and Sanders for example). It is referenced in the chapter on NP completeness when they talk about graph problems and reductions if I remember correctly. The Barak-Arora book is basically the standard grad school textbook for complexity theory. But it tries its best to minimise contact with the algorithms side.

It is certainly not covering every model there is. There is the whole world of distributed models, Local computation, query complexity, dynamic complexity etc, that have not been covered.

[Shreyas Srinivas]

For some reason complexity zoo seems to be unavailable, but it is/was basically a wiki for everything to do with complexity theory (I mostly recall seeing complexity classes)

[Shreyas Srinivas]

There are variations like the"real RAM" model that you would only encounter in places like computational geometry.

Basically, finding a single source of comprehensive truth is hard in this subject

[Shreyas Srinivas]

But the Barak-Arora book has the benefit of containing enough foundational material that using it as a guide might be a good idea.

[Mario Carneiro]

The main thing we want to ensure here is that the model we actually use is suitably close (in the sense of having translations with low enough loss to not lose the distinctions of interest) to the ones that the textbooks use

[Mario Carneiro]

As I mentioned, as long as a factor of O(n) loss is okay, TMs are fine. But that's not good enough for your DFS example

[Mario Carneiro]

in fact, there is very commonly a O(log n) loss in a lot of RAM model style things in order to encode the pointer values

[Mario Carneiro]

I think that's what word RAM is about

[Shreyas Srinivas]

Mario Carneiro said:

The main thing we want to ensure here is that the model we actually use is suitably close (in the sense of having translations with low enough loss to not lose the distinctions of interest) to the ones that the textbooks use

Well then Barak-Arora is the way to go. It is one of the standard textbooks. Michael Sipser's textbook is also used a lot for intro courses.

[Shreyas Srinivas]

Mario Carneiro said:

in fact, there is very commonly a O(log n) loss in a lot of RAM model style things in order to encode the pointer values

Some log might come up like that in pseudopolynomial algorithms ( for example see knapsack algorithms or the ellipsoid algorithm).

[Mario Carneiro]

sure, but it's different if it's put there on purpose

[Shreyas Srinivas]

I mean, check this (recent, award winning) paper : https://arxiv.org/abs/2203.03456

[Shreyas Srinivas]

I don't think the log^8 n has anything to do with pointer packing.

[Mario Carneiro]

Right, but if we tried to formalize that and got log^10 because of pointer packing issues, that wouldn't look very good, would it?

[Shreyas Srinivas]

I don't think it matters that much.

[Mario Carneiro]

I'm not sure we can make the judgment that those factors are never relevant in any proof that will be using the framework

[Martin Dvořák]

It seems to me that we have some misunderstanding going on. Do you @Shreyas Srinivas actually want to formally verify complexity theory? Or do you want to build a library of complexity-theoretic results àla Formal Abstracts project?

[Shreyas Srinivas]

Mario Carneiro said:

I'm not sure we can make the judgment that those factors are never relevant in any proof that will be using the framework

In this case the authors are not bothered about those factors so they would probably the \tilde{O} notation (which ignores log factors in addition to constants)

[Martin Dvořák]

In the latter case, you maybe don't care about correctness, but rather about having an expressive formal language to allow a computer to work with this database?

[Mario Carneiro]

We proved that you can sort n numbers in O(n log^2 n) steps...

[Shreyas Srinivas]

Martin Dvořák said:

It seems to me that we have some misunderstanding going on. Do you Shreyas Srinivas actually want to formally verify complexity theory? Or do you want to build a library of complexity-theoretic results àla Formal Abstracts project?

I do care about correctness, but I am happy with correctness at the level of abstraction that the authors care about. Correctness is often tricky to prove as well.

[Shreyas Srinivas]

In the word RAM model where your numbers are guaranteed to fit into one word?
Mario Carneiro said:

We proved that you can sort n numbers in O(n log^2 n) steps...

[Martin Dvořák]

Shreyas Srinivas said:

I do care about correctness, but I am happy with correctness at the level of abstraction that the authors care about.

Do you want your computer to enforce the correctness?

[Mario Carneiro]

the sorting example is especially funny since those numbers are surely at least O(log n) long for the problem to be interesting, and hence at least O(log n) to compare, so most likely O(n log^2 n) is the correct bound

[Mario Carneiro]

Shreyas Srinivas said:

In the word RAM model where your numbers are guaranteed to fit into one word?
Mario Carneiro said:

We proved that you can sort n numbers in O(n log^2 n) steps...

This is my point. We're going to invest a bunch of time and effort into one model and then it turns out that for this result we've got to throw it away and get a better one

[Shreyas Srinivas]

Martin Dvořák said:

Shreyas Srinivas said:

I do care about correctness, but I am happy with correctness at the level of abstraction that the authors care about.

Do you want your computer to enforce the correctness?

I want to know if the papers I am checking have actually done their due diligence (which is a more non-trivial issue in theoretical CS than math, probably because of our conference culture).

[Shreyas Srinivas]

Mario Carneiro said:

the sorting example is especially funny since those numbers are surely at least O(log n) long for the problem to be interesting, and hence at least O(log n) to compare, so most likely O(n log^2 n) is the correct bound

If we find a way to avoid this issue, then we will be due some awards. Algorithms can quite often exploit very specific model properties to do things. So a result that you develop for one model might not work for another model by translation.

[Mario Carneiro]

well then it sure would be nice if papers were more precise about the definitions of their models

[Shreyas Srinivas]

Oh they are... it is just that everybody likes to write their own model from scratch

[Mario Carneiro]

if we can find some small set of equivalence classes of models into which we can bucket all the results that would be ideal...

[Martin Dvořák]

Shreyas Srinivas said:

I want to know if the papers I am checking have actually done their due diligence (which is a more non-trivial issue in theoretical CS than math, probably because of our conference culture).

I don't understand your sentence (which might be my mistake — my English isn't that good). To avoid further confusion, please, clarify:

Do you want the correctness of the results to be enforced by computer?

[Shreyas Srinivas]

Which brings us back to the word RAM model. It is ideal for several reasons:

1. Most CS students instinctively know it. Most code for algorithms (not all) is written on something close to word RAM.
2. Some of the work has already been done for us in the algorithms engineering world: https://www3.cs.stonybrook.edu/~algorith/implement/LEDA/implement.shtml
   They have nailed down the implementation of many algorithms in highly precise details.

[Mario Carneiro]

the word RAM model is a bit weird in that it explicitly depends on w which is related to n, though... it's not entirely clear to me how to avoid the issues with nonuniform algorithms

[Shreyas Srinivas]

Martin Dvořák said:

Shreyas Srinivas said:

I want to know if the papers I am checking have actually done their due diligence (which is a more non-trivial issue in theoretical CS than math, probably because of our conference culture).

I don't understand your sentence (which might be my mistake — my English isn't that good). To avoid further confusion, please, clarify:

Do you want the correctness of the results to be enforced by computer?

Yes their proofs must be correct and this correctness must be machine checkable. I am willing to tolerate reasonable assumptions about existing algorithms. For example I am not really going to insist that the authors write a proof of correctness for Depth First Search. If they make known assumptions about it or use a library invocation then I am happy with that.

[Shreyas Srinivas]

Mario Carneiro said:

the word RAM model is a bit weird in that it explicitly depends on w which is related to n, though... it's not entirely clear to me how to avoid the issues with nonuniform algorithms

nonuniform algorithms?

[Shreyas Srinivas]

like non-uniform circuits? (one algorithm per input size)

[Martin Dvořák]

Shreyas Srinivas said:

Yes their proofs must be correct and this correctness must be machine checkable. I am willing to tolerate reasonable assumptions about existing algorithms. For example I am not really going to insist that the authors write a proof of correctness for Depth First Search. If they make known assumptions about it or use a library invocation then I am happy with that.

I am completely happy with "library invocation" but not so much with "known assumptions". We are at a point when a library of complexity-theoretic results in Lean does not exist. We cannot invoke it.

We need to prove first things directly from the definition. And here comes the question: What definition do we exactly want to work with?

[Shreyas Srinivas]

Martin Dvořák said:

Shreyas Srinivas said:

Yes their proofs must be correct and this correctness must be machine checkable. I am willing to tolerate reasonable assumptions about existing algorithms. For example I am not really going to insist that the authors write a proof of correctness for Depth First Search. If they make known assumptions about it or use a library invocation then I am happy with that.

I am completely happy with "library invocation" but not so much with "known assumptions". We are at a point when a library of complexity-theoretic results in Lean does not exist. We cannot invoke it.

We need to prove first things directly from the definition. And here comes the question: What definition do we exactly want to work with?

There are formidable problems with asking for this. Take Depth First Search(hereon : DFS). There are at least 4-5 graph representations I can think of, off the top of my head. Then there is the question of whether you explicitly create a stack or use recursions. Already that gives you 10 potentially different implementations (and possibly many more), with different representation specific complexities. Now let's say you are writing a paper where all you care about is that DFS runs in O(|V| + |E|) time. Should you spend time on sorting through these implementations or building your own?

[Shreyas Srinivas]

Shreyas Srinivas said:

Martin Dvořák said:

Shreyas Srinivas said:

Yes their proofs must be correct and this correctness must be machine checkable. I am willing to tolerate reasonable assumptions about existing algorithms. For example I am not really going to insist that the authors write a proof of correctness for Depth First Search. If they make known assumptions about it or use a library invocation then I am happy with that.

I am completely happy with "library invocation" but not so much with "known assumptions". We are at a point when a library of complexity-theoretic results in Lean does not exist. We cannot invoke it.

We need to prove first things directly from the definition. And here comes the question: What definition do we exactly want to work with?

There are formidable problems with asking for this. Take Depth First Search(hereon : DFS). There are at least 4-5 graph representations I can think of, off the top of my head. Then there is the question of whether you explicitly create a stack or use recursions. Already that gives you 10 potentially different implementations (and possibly many more), with different representation specific complexities. Now let's say you are writing a paper where all you care about is that DFS runs in O(|V| + |E|) time. Should you spend time on sorting through these implementations or building your own?

It gets even worse. Suppose I have additional information that the graph has bounded degree. Now, do I rebuild a new version of these implementations from scratch?

[Martin Dvořák]

I don't think you can formally verify stuff without being precise about it in the first place.

[Shreyas Srinivas]

But you could verify that starting from known and simple assumptions, you can build a more complex algorithm

[Mario Carneiro]

These issues are exactly why the graph theory in lean took a while to get off the ground. What fixed it? Picking a definition and formalizing stuff about it

[Mario Carneiro]

We know there are many definitions. So we need to pick a good one

[Mario Carneiro]

And if you use too many different definitions then the results can't be used together and we end up not working well as a library of reusable results and more like an archive

[Mario Carneiro]

Shreyas Srinivas said:

Mario Carneiro said:

the word RAM model is a bit weird in that it explicitly depends on w which is related to n, though... it's not entirely clear to me how to avoid the issues with nonuniform algorithms

nonuniform algorithms?

like non-uniform circuits? (one algorithm per input size)

Yeah, the name escapes me at the moment. If you aren't careful here you can decide the undecidable

[Shreyas Srinivas]

The issue we will encounter here is that we will need all these definitions and show the relevant equivalences. Unfortunately, algorithmic upper and lower bounds don't always neatly translate between models. While I can recommend TMs and wordRAM as starting points, even within this there will be 10 different DFS versions. It is unavoidable. We can definitely start somewhere and see how it goes.

[Shreyas Srinivas]

CS theory is messy in that way.

[Mario Carneiro]

Do you have a recommendable source for word RAM done the way you think it should be done?

[Shreyas Srinivas]

Mario Carneiro said:

Shreyas Srinivas said:

Mario Carneiro said:

the word RAM model is a bit weird in that it explicitly depends on w which is related to n, though... it's not entirely clear to me how to avoid the issues with nonuniform algorithms

nonuniform algorithms?

like non-uniform circuits? (one algorithm per input size)

Yeah, the name escapes me at the moment. If you aren't careful here you can decide the undecidable

So the result is that non uniform circuit families can accept undecidable languages. Take a simple binary alphabet {0,1}. Then for any subset S of \N, you can build a family of circuits which accepts {1^x | x \in S}

[Mario Carneiro]

right, I don't want word RAM accepting undecidable languages

[Shreyas Srinivas]

Mario Carneiro said:

right, I don't want word RAM accepting undecidable languages

Word RAM does not have this issue.

[Mario Carneiro]

because?

[Mario Carneiro]

is w not observable to the program or something?

[Shreyas Srinivas]

More specifically you can write non-terminating programs in word RAM (any computer program). But is is equivalent to TMs upto polynomial time complexity factors. So it can do exactly what TMs can do

[Mario Carneiro]

A word RAM doesn't have infinite memory, does it?

[Mario Carneiro]

I don't see how they could be turing complete

[Shreyas Srinivas]

Mario Carneiro said:

because?

If you know n you know w

[Martin Dvořák]

Shreyas Srinivas said:

CS theory is messy in that way.

That's why we should choose a suitable part of it and make it tidy.

[Mario Carneiro]

If you have a sequence of programs running on larger machines then isn't this the non-uniform circuit issue all over again?

[Shreyas Srinivas]

I think I found the kind of definition you were looking for @Mario Carneiro : http://people.seas.harvard.edu/~cs125/fall14/lec6.pdf

[Mario Carneiro]

whoa, that model has a "malloc" that is literally "buy another byte from the hardware store"

[Mario Carneiro]

and maybe increase the word size so you can address it too

[Shreyas Srinivas]

I think they work around the limitation you speak of w

[Shreyas Srinivas]

by taking w = \Omega(\log n)

[Mario Carneiro]

it still looks like an incredibly painful model to work with

[Shreyas Srinivas]

Almost all computational models are

[Mario Carneiro]

it's like a turing machine, only worse because there are so many operations and you can't assume w = 1

[Shreyas Srinivas]

Most people think of it as : Most arithmetic and boolean operations in constant time (not real numbers, that is real RAM)).

[Mario Carneiro]

no I mean it's really obvious that it is C inspired

[Mario Carneiro]

and I'm sure it's fine to program in

[Mario Carneiro]

but not to reason about

[Mario Carneiro]

composition looks very bad in this model

[Shreyas Srinivas]

This is another reason you want to go through the DSL route. You can parameterize the choice of unit operations.

[Shreyas Srinivas]

And then build up from there.

[Shreyas Srinivas]

Mario Carneiro said:

it's like a turing machine, only worse because there are so many operations and you can't assume w = 1

TMs are different from the w=1 case. There is no addressing requirement. OTOH, the state register can store some bits of info.

[Yaël Dillies]

Shreyas Srinivas said:

I want to know if the papers I am checking have actually done their due diligence (which is a more non-trivial issue in theoretical CS than math, probably because of our conference culture).

Let me just say that formalising a result in Lean is orders of magnitude harder than checking it informally, so I wouldn't take that as my main motivation if I were you.

[Martin Dvořák]

Shreyas Srinivas said:

Almost all computational models are

People say "choose your poison". I add "but don't choose too many poisons at the same time — it would become too hard to build immunity to them".

[Mario Carneiro]

Shreyas Srinivas said:

This is another reason you want to go through the DSL route. You can parameterize the choice of unit operations.

I agree with this, although it doesn't have much to do with DSLs. A simple family of computational models which comes acceptably close to popular ones in the literature is also great

[Mario Carneiro]

certainly it's obvious how to insert a parameter to the word RAM to make the set of register operations configurable

[Mario Carneiro]

although IIRC the multiplication operation in particular is rather disproportionately more powerful than the others here

[Shreyas Srinivas]

Yaël Dillies said:

Shreyas Srinivas said:

I want to know if the papers I am checking have actually done their due diligence (which is a more non-trivial issue in theoretical CS than math, probably because of our conference culture).

Let me just say that formalising a result in Lean is orders of magnitude harder than checking it informally, so I wouldn't take as my main motivation if I were you.

Realistically I expect this to remain infeasible for at least the next decade for most of CS theory. At least until there is a reasonably large library.

[Mario Carneiro]

well that's what this phase is about, assessing the goals and picking what to go for and what to avoid

[Mario Carneiro]

what do you think would be in the "reasonably large library" that would make the second phase feasible?

[Shreyas Srinivas]

Mario Carneiro said:

well that's what this phase is about, assessing the goals and picking what to go for and what to avoid

word RAM is not Turing complete. RAM is. Apologies.

[Mario Carneiro]

we want to go for the things that empower later work, not just endpoint theorems

[Shreyas Srinivas]

Mario Carneiro said:

well that's what this phase is about, assessing the goals and picking what to go for and what to avoid

I think phase would be:

1. Formalise basic complexity theory.
2. Formalise linear programming. weak duality strong duality etc. Linear programming is fundamental to many areas inside CS.
3. Formalise structural results from graph theory that are useful in CS, relating various invariants (for example :graph minors a la Robertson and Seymour)
4. Formalise combinatorial results like : https://en.wikipedia.org/wiki/Isolation_lemma

[Shreyas Srinivas]

We can also probably go for a RAM model for algorithms.

[Shreyas Srinivas]

To make sure you can't claim arbitrary operations have arbitrary complexities, you need to restrict the ways in which valid algorithms are constructed (i.e. unit operations, function calls, loops, conditionals)

[Mario Carneiro]

why not allow arbitrary operations to have arbitrary complexities?

[Mario Carneiro]

In a reduction I would imagine it is convenient to allow weird cost functions on either the source or target to make things match up

[Shreyas Srinivas]

Mario Carneiro said:

why not allow arbitrary operations to have arbitrary complexities?

If I have a theorem which gives me a complexity result in a model, I can trust the result only if it does not use silly assumptions inside like polynomial time minimum vertex cover algorithms.

[Mario Carneiro]

sure, but it's not like that's a problem of the framework

[Shreyas Srinivas]

Mario Carneiro said:

why not allow arbitrary operations to have arbitrary complexities?

No, in reductions, you actually want to avoid this. Because you need to prove that the reduction has a certain time complexity for it to be valid. The reduction needs to be a valid algorithm with a valid time complexity.

[Kevin Buzzard]

Mario Carneiro said:

we want to go for the things that empower later work, not just endpoint theorems

This is the approach which worked so well with mathematics -- for a long time at the beginning the mantra was just "build as much as possible of a standard undergraduate maths degree in one place", and the showcase theorems grew from this solid core.

[Mario Carneiro]

Shreyas Srinivas said:

Mario Carneiro said:

why not allow arbitrary operations to have arbitrary complexities?

No, in reductions, you actually want to avoid this. Because you need to prove that the reduction has a certain time complexity for it to be valid. The reduction needs to be a valid algorithm with a valid time complexity.

I think we are miscommunicating. The reduction is just a theorem about the relation between different models, with some assumptions on the source and/or target and some relation between the cost models on each side. There isn't any point at which there is a cutoff and it stops being a "valid reduction" or a "valid time complexity", that's something you can impute on the theorem after the fact. For example, I should be able to prove that sorting is O(n!) if I want, it's not a useful theorem perhaps but I shouldn't define big-O so that the theorem is false.

[Shreyas Srinivas]

Oh, when I think of reductions, I think of reductions between problems in a single model.

[Shreyas Srinivas]

For example 3 CNF to Vertex Cover.

[Mario Carneiro]

In this case I mean reduction from one computational model to another, a translation

[Shreyas Srinivas]

So such a translation usually means that you are simulating one model in the other. Like writing a program to simulate a universal Turing machine in C or vice versa. Then, a complexity of this translation is defined in the model in which you are doing the simulation. It makes sense that the simulation algorithm cannot do arbitrary operations in a single step, since it is in fact an algorithm.

[Shreyas Srinivas]

It would be absolutely false to claim that I can simulate RAM model in Turing machines with O(1) overhead.

[Mario Carneiro]

Having a wide space of parameters is useful since you can have "algebraic" operations between them, like maps and comaps and stuff like that. It is a really powerful technique for making things reusable and for shorter proofs too.

[Shreyas Srinivas]

Mario Carneiro said:

Having a wide space of parameters is useful since you can have "algebraic" operations between them, like maps and comaps and stuff like that. It is a really powerful technique for making things reusable and for shorter proofs too.

I agree with this. I am just saying that the parametrisation must be in the choice of unit operations.

[Mario Carneiro]

Shreyas Srinivas said:

It would be absolutely false to claim that I can simulate RAM model in Turing machines with O(1) overhead.

I think it is fine to have an algebra that includes 0 cost for everything, for the same reason that ⊥ should be a filter

[Shreyas Srinivas]

Mario Carneiro said:

Shreyas Srinivas said:

It would be absolutely false to claim that I can simulate RAM model in Turing machines with O(1) overhead.

I think it is fine to have an algebra that includes 0 cost for everything, for the same reason that ⊥ should be a filter

Yes, that would be fine. It would just be a different model then. Not a translation between say RAM and TM

[Shreyas Srinivas]

This is incidentally what Erik Demaine does for describing a notion of energy complexity. All "reversible" operations have 0 energy cost. https://erikdemaine.org/papers/Energy_ITCS2016/paper.pdf

[Shreyas Srinivas]

Once you fix the model in which you are writing an algorithm (including reductions), the cost function is predetermined for that algorithm.

[Mario Carneiro]

well, you can also consider a translation from TM with the usual cost function to RAM with a weird cost function, or the other way around

[Mario Carneiro]

that is convenient because it is easy to prove how the same model with a different cost function relates

[Shreyas Srinivas]

Okay I think I see what you mean. You are saying that there could be multiple reductions each with its own cost

[Shreyas Srinivas]

and what I am saying is that given a particular reduction, the cost is fixed by the model

[Shreyas Srinivas]

I think we are in agreement if I read this correctly.

[Shreyas Srinivas]

The key thing is you don't want to allow a proof that says that the cost of solving some 3SAT instance along the way is O(1). A DSL is a good way to restrict the kind of programs you can build and the way the cost adds up.

[Shreyas Srinivas]

Nothing in lean itself might prevent someone from defining a function like that and tagging it with O(1) complexity.

[Mario Carneiro]

Shreyas Srinivas said:

The key thing is you don't want to allow a proof that says that the cost of solving some 3SAT instance along the way is O(1). A DSL is a good way to restrict the kind of programs you can build and the way the cost adds up.

This will either be a theorem or not depending on the precise statement and the values of the unstated parameters like the underlying computational model and cost model. If it's not a theorem, then there is no way you can sneak it through in the proof regardless of any DSL

[Mario Carneiro]

you can't just tag functions with a complexity, the cost of all the primitives is part of the definition of the cost model which is a parameter to everything

[Mario Carneiro]

or it's a fixed quantity which is defined somewhere, presumably with reasonable values so that useful results can be formalized

[Shreyas Srinivas]

Mario Carneiro said:

you can't just tag functions with a complexity, the cost of all the primitives is part of the definition of the cost model which is a parameter to everything

"the cost of all the primitives is part of the definition of the cost model which is a parameter to everything" => I am in complete agreement here

[Mario Carneiro]

but it's totally possible, even useful, to have a model which assigns O(1) cost to SAT problems. That's basically an oracle model

[Shreyas Srinivas]

Yeah that's also useful

[Shreyas Srinivas]

In the LOCAL and CONGEST model, we have 0 cost for local computations (even NP complete problems).

[Shreyas Srinivas]

But how would we define a cost model for every possible expression in lean?

[Mario Carneiro]

we don't need to?

[Mario Carneiro]

the cost model applies to operations definable in prog

[Shreyas Srinivas]

so prog is a DSL (I am thinking like a haskell person here).

[Mario Carneiro]

it's an inductive type of programs

[Mario Carneiro]

it's the stuff you reason about - in the word RAM example this was a sequence of primitive operations on registers and gotos

[Shreyas Srinivas]

Ah I think we are using different terms for the same thing

[Mario Carneiro]

a DSL would be a syntax for constructing elements of prog conveniently (and maybe proving properties about it along the way)

[Shreyas Srinivas]

Mario Carneiro said:

a DSL would be a syntax for constructing elements of prog conveniently (and maybe proving properties about it along the way)

I was thinking of an inductive type plus use of notation, which might yield a nice syntax

[Mario Carneiro]

and Lean-as-DSL is the idea that tactics can just look at declarations in the environment and translate them to an element of prog plus a proof of correctness

[Mario Carneiro]

if you try to use something too weird in the input lean program then the tactic will fail

[Shreyas Srinivas]

Shreyas Srinivas said:

Ah I think we are using different terms for the same thing

Now I am certain this is the case.

[Mario Carneiro]

lean 4 also lets you write some syntax which directly macro expands to elements of prog, that's more explicitly a DSL

[Mario Carneiro]

but prog itself is more of a deep embedding than a DSL

[Mario Carneiro]

it's not necessarily a language at all, it might be a circuit or some other thing

[Shreyas Srinivas]

With a bit of convenient notation and some macros, we should be able to make it much easier to write programs in a form familiar to theorists.
Shreyas Srinivas said:

Mario Carneiro said:

well that's what this phase is about, assessing the goals and picking what to go for and what to avoid

I think phase (EDIT: one) would be:

1. Formalise basic complexity theory.
2. Formalise linear programming. weak duality strong duality etc. Linear programming is fundamental to many areas inside CS.
3. Formalise structural results from graph theory that are useful in CS, relating various invariants (for example :graph minors a la Robertson and Seymour)
4. Formalise combinatorial results used in CS(example : https://en.wikipedia.org/wiki/Isolation_lemma)

[Shreyas Srinivas]

Any thoughts on the above? I think these four points, along with prog would go a long way to make theory results easy to prove on theorem provers.

[Shreyas Srinivas]

The trouble is most of the results are scattered across the literature, so starting with undergrad textbooks (or early graduate books) on graphs, complexity etc sounds like a good strategy.

[Mario Carneiro]

I think it's a bit too long term to be immediately actionable

[Mario Carneiro]

we're still talking about the setup to point 1 after all

[Mario Carneiro]

so something more precise than "basic complexity theory" would be useful

[Shreyas Srinivas]

Chapters 1 and 2 (https://theory.cs.princeton.edu/complexity/book.pdf) should be a good starting point : Chapter 1 is 60% about computability,

[Martin Dvořák]

Is this paper worth reading?
https://www.cs.ru.nl/~freek/pubs/sketches2.pdf

[Shreyas Srinivas]

[Quoting…]

I gave it a quick skim. The problem the paper claims to solve is how proofs in ITPs are presented. I don't know if they idea of a proof sketch is the way to do, theorem prover experts have to chime in.

But insofar as the authors claim that ITP proofs are practically unreadable, I think this is definitely true for lean. TPIL acknowledges this when it introduces tactic style proofs. I think the point was, the more the automation, the less readable the proof gets. #print on a theorem almost always produces a large messy term, produced by the tactics.

I also agree that this is an important issue
We discussed this issue in PM a few days ago. I pointed out that at least in theoretical CS, it is not only important that we know a claim is true, it is important to know the structure of the proof, what ideas come into play, and how they work together. So for example a proof that just calls "simp" would be unsatisfactory. #print of that proof might be an unreadable blob of code.

My suspicion is that there is some solution to this issue that involves producing a clean and readable text from a proof term.

[Shreyas Srinivas]

In complexity theory, we greatly care about the innards of our proofs to varying degrees. So making the proof output readable is very important to us.

[Shreyas Srinivas]

For example the crux of a new result could be a new reduction gadget. In that case, being able to see how the gadget is used in the reduction matters

[Kevin Buzzard]

I'll just chime in with my usual message that in maths the things we're proving in mathlib are either completely mathematically trivial or are very well-documented in standard textbooks so readability is not really something I'm too bothered about. I find lean proofs very easy to read if I step through them in VS Code -- although ring or linarith might produce huge proof terms, size or complexity of proof terms is an extremely poor measure of proof complexity to a human mathematician. I know that ring is just expanding out the brackets and tidying up, the fact that it turns out that it takes 100 applications of the axioms of a ring to justify this is of absolutely no interest to me. I've noticed that this is a big difference in attitude between mathematicians and computer scientists, and because computer scientists have traditionally dominated this area I think readability has somehow been made a bigger deal than perhaps I would expect.

[Martin Dvořák]

I care a lot about readability of definitions and theorems. I care a bit about readability of lemmata. I don't care about readability of proofs.

I like it when proofs are maintainable (for a developer who has invested some time to understanding the codebase) but I couldn't care less about how readable my proofs are without IDE.

[Shreyas Srinivas]

Kevin Buzzard said:

I'll just chime in with my usual message that in maths the things we're proving in mathlib are either completely mathematically trivial or are very well-documented in standard textbooks so readability is not really something I'm too bothered about. I find lean proofs very easy to read if I step through them in VS Code -- although ring or linarith might produce huge proof terms, size or complexity of proof terms is an extremely poor measure of proof complexity to a human mathematician. I know that ring is just expanding out the brackets and tidying up, the fact that it turns out that it takes 100 applications of the axioms of a ring to justify this is of absolutely no interest to me. I've noticed that this is a big difference in attitude between mathematicians and computer scientists, and because computer scientists have traditionally dominated this area I think readability has somehow been made a bigger deal than perhaps I would expect.

There are at least three different reasons I can think of, which makes readable presentations of proofs important:

1. Debugging: this is the reason people across CS, outside theory, care about it

2. Explanatory value: Often these days, the crux of theory papers are not results but algorithmic or proof techniques. It is debatable how much this can be rigorously formalized (or how readable even the statements of such theorems will be). Such techniques might then give you upper/lower bounds on a number of problems, when adapted to each specific problem. The technique would then be the key contribution of the paper, and seeing it action would be important. Typically what one can formalize might be specific uses of that technique.

3. Pedagogy: Good proofs are often very revealing. They teach students how to think about a problem, and often also yield algorithms or ways to generate counter examples. After all students need to learn to prove claims, not just learn statements. With some tactic based proofs it is clear what we are doing at each. For example proofs that use linarith or rw with specific theorems, or simp only. Other tactics might just look magical

[Martin Dvořák]

Shreyas Srinivas said:

1. Debugging: this is the reason people across CS, outside theory, care about it

Our stance on debugging will be very different from what software engineers think. When you write usual programs, you never know when another bug will be reported, forcing you to work with your code again. In theorem proving, we do our "debugging" only once. When our proof is done, we are guaranteed that there will never be a bug. If my code is incomprehensible for the future me, it isn't such a problem.

[Martin Dvořák]

Shreyas Srinivas said:

2. Explanatory value: (...) The technique would then be the key contribution of the paper, and seeing it action would be important. (...)

Reusability of our technique should be served in form of reusable lemmas. In formal proofs, we write much more of them than in usual theory papers. I'd focus on how the lemma is stated (and if the lemma cannot be reused, it will hopefully be at least possible to write an analogical lemma for the different settings). I don't want to dig into the proof of the lemma in order to extract some technique from within the proof to use it elsewhere. Another amazing thing is when you create a reusable tactic. With tactics, however, it is much harder to achieve high-level applicability.

[Mario Carneiro]

Martin Dvořák said:

Shreyas Srinivas said:

1. Debugging: this is the reason people across CS, outside theory, care about it

Our stance on debugging will be very different from what software engineers think. When you write usual programs, you never know when another bug will be reported, forcing you to work with your code again. In theorem proving, we do our "debugging" only once. When our proof is done, we are guaranteed that there will never be a bug. If my code is incomprehensible for the future me, it isn't such a problem.

I disagree with this, maintaining a formal mathematics library has more similarities than differences to maintaining a software library. It's not true that proofs are written once and never returned to. Mathlib is refactored all the time, to add new typeclasses, reorder developments, etc. Proofs need to change when their dependencies change, or the tactics that they use change.

It is also not true that a proof that compiles does not have a bug, it's just that the bugs are of a different nature than correctness. For example you can have an instance that loops, or simp lemma that causes non-confluence. The theorem itself is perfectly true, but it probably shouldn't have been annotated the way it was. Also it could be proving the wrong thing, either because the author didn't notice that the theorem was trivial or because a subsequent change to elaboration or something causes the statement / proof to be interpreted wrongly. These often lead to errors in the proof but not always - you can end up with a true proof of a garbage theorem.

[Shreyas Srinivas]

I recall reading something like "formal verification is only as good as the specification and tools allow"

[Kevin Buzzard]

When I came to lean in 2017 I told Mario that I could not possibly use his silly library with my students it couldn't even prove that 2 + 2 = 4 in the real numbers. He responded by writing norm_num. Chris Hughes then told him that proving that every positive integer was the sum of four squares was a nightmare and Mario wrote ring, following work of Assia and her group. Patrick complained about how he couldn't teach analysis because he couldn't do inequalities and Rob responded by writing norm_num. All of these tactics are writing completely unreadable code but which mathematician would want to read it? In all cases these tactics are doing things which humans find completely trivial. Type class inference is another example. I neither know nor care how it works. Coercions another, this one solved with rorm_num. I have absolutely no interest in what is going on under the hood here -- I am a mathematician!

[Yaël Dillies]

*linarith for the third, norm_cast for the fourth

[Shreyas Srinivas]

Kevin Buzzard said:

When I came to lean in 2017 I told Mario that I could not possibly use his silly library with my students it couldn't even prove that 2 + 2 = 4 in the real numbers. He responded by writing norm_num. Chris Hughes then told him that proving that every positive integer was the sum of four squares was a nightmare and Mario wrote ring, following work of Assia and her group. Patrick complained about how he couldn't teach analysis because he couldn't do inequalities and Rob responded by writing norm_num. All of these tactics are writing completely unreadable code but which mathematician would want to read it? In all cases these tactics are doing things which humans find completely trivial. Type class inference is another example. I neither know nor care how it works. Coercions another, this one solved with rorm_num. I have absolutely no interest in what is going on under the hood here -- I am a mathematician!

I wonder if the proof culture in different fields is different. I have encountered differences even within CS. Programming Languages and formal methods people are rigorous to a fault. They dot their i's and cross their t's. Cryptographic protocols people love machine checked proofs (see: tamarin prover, F*). Consensus folks have their way of writing proofs. Algorithms and Complexity theory people have this unrolling and verbose style of writing proofs (due to constraints of the conference system) which focuses on highlighting the key ideas and their application, at many levels of abstraction. An algorithm's proof of correctness might be key to understanding why it works. Based on my conversations with physicists, they too seem to care about the insights offered by a good proof.

[Shreyas Srinivas]

What I am worried about are situations when one needs to illustrate, for example, a reduction by proving it with some new gadget or technique. Suppose I write a tactic based proof that doesn't make it clear how the technique was combined with other theorems (let's say a bunch of simps and library searches). If the output of the proof is not readable, then how do I know anything about the technique and its usage? Was it even used? How do I get the insights and ideas for new problems/algorithms that well structured and written proofs might provide me?

[Henrik Böving]

If you actually have an abstract idea in your proof I don't see why your abstract idea couldn't be expressed via a tactic or a lemma on its own. If I see a simp I know "okay you chained a bunch of well known equalities + optional ones you defined in the parameter set" if I see a ring I know "okay this was solved by using ring axioms" if I see linarith I know "this was solved by some decision procedure for linear arithmetic". If you have an abstract idea for a proof in complexy theory write a tactic for it and write that tactic in a way that is nice to understand. It doesn't even have to be a special meta program it can also just be some arrangement of tactics with a macro. If your proof idea has such interesting insight that it is useful in general you can also just put it as a sepqrate lemma for everyone to read like say the pumping lemma for regular languages.

The closest i've seen to "readable" proofs would be Isabelle where they can mostly make leaps in logic because their automation with things like sledgehammer, blast, auto etc. are so good. So when they write their proofs in this Isar style they can just make a leap from one statement to another, put a sledgehammer under in and the system will do the rest (of course this doesn't work out always, but quite often).

[Reid Barton]

If you are ever actually in the kind of situation you're worried about, I think you should be very happy!

[Reid Barton]

Because I expect you will in practice have the opposite problem (need to spell out a huge amount of stuff explicitly).

[Shreyas Srinivas]

"If you have an abstract idea for a proof in complexity theory write a tactic for it and write that tactic in a way that is nice to understand" => I expect that this will be key for the complexity theory part of mathlib. I can imagine that reductions will be done with tactics that take some gadgets and lemmas. Similarly, for deducing the existence of greedy algorithms for problem, tactics related to matroids might be handy

[Shreyas Srinivas]

Reid Barton said:

Because I expect you will in practice have the opposite problem (need to spell out a huge amount of stuff explicitly).

I expect this to happen as well. Some tactics based proofs (especially ones that use limited tactics like cases, linarith, rw, simp only or induction) seem more readable compared to pen and paper versions of these proofs.

[Shreyas Srinivas]

If there is a hypothetical tactic line that were to read karp_reduction by [<some_reduction_theorems>, <reduction_maps>] that is already quite readable. Even more readable and informative is a proof that specifies the reduction step, then produces the goals about equivalence and complexity, which are in turn proved by some one line tactics.

[Mario Carneiro]

While that might be an eventual goal, I think it is important to not jump ahead and try to implement those tactics before the underlying machinery is proven out. Essentially, you have to do it the "hard way" at least a few times before you are in a good enough position to know what can / should be automated away, by looking at similarities and differences in the arguments

[Mario Carneiro]

("machinery" here meaning primarily lemmas!)

[Mario Carneiro]

tactics automate proofs, and proofs are made of lemmas, so until the lemmas are available and work well together the tactic can't be written

[Yaël Dillies]

I think you will understand our position on tactics once you try proving some contentful result.

[Yaël Dillies]

Let me also mention that tactics tend to make proofs more readable, not less. Because there are less tactic calls, the crucial ones are not lost in a sea of trivial rewrites. My own style changed quite a lot in the past months and I finally am following @Bhavik Mehta's long told advice to use simp rather three lines rw calls.

[Martin Dvořák]

For readability inside IDE, I prefer long rw calls.

[Shreyas Srinivas]

Yaël Dillies said:

Let me also mention that tactics tend to make proofs more readable, not less. Because there are less tactic calls, the crucial ones are not lost in a sea of trivial rewrites. My own style changed quite a lot in the past months and I finally am following Bhavik Mehta's long told advice to use simp rather three lines rw calls.

Part of my challenge is to also convince people around me that this is useful for our field (and it does). Some of them got their hands burnt trying to formalise things with Isabelle. Their complaints were that the prover had to be taught the basics and that they couldn't understand the arcane language of the prover. A bunch of rw's go a long way towards this than a simp in such cases.

[Shreyas Srinivas]

Yaël Dillies said:

Let me also mention that tactics tend to make proofs more readable, not less. Because there are less tactic calls, the crucial ones are not lost in a sea of trivial rewrites. My own style changed quite a lot in the past months and I finally am following Bhavik Mehta's long told advice to use simp rather three lines rw calls.

Part of my challenge is to also convince people around me that this is usable for our field (and it is). Some of them got their hands burnt trying to formalise things with Isabelle. Their complaints were that the prover had to be taught the basics and that they couldn't understand the arcane language of the prover. A bunch of rw's go a long way towards this than a simp in such cases.

[Shreyas Srinivas]

Sorry, on my phone. Zulip's interface is terrible

[Henrik Böving]

Shreyas Srinivas said:

Yaël Dillies said:

Let me also mention that tactics tend to make proofs more readable, not less. Because there are less tactic calls, the crucial ones are not lost in a sea of trivial rewrites. My own style changed quite a lot in the past months and I finally am following Bhavik Mehta's long told advice to use simp rather three lines rw calls.

Part of my challenge is to also convince people around me that this is useful for our field (and it does). Some of them got their hands burnt trying to formalise things with Isabelle. Their complaints were that the prover had to be taught the basics and that they couldn't understand the arcane language of the prover. A bunch of rw's go a long way towards this than a simp in such cases.

"They couldnt understand the arcane language of the prover" vs "doing everything by hand to the prover because I only have this one way to talk to it" Seems precisely like you are just teaching the basics to the prover. If you were to tell these people that they are supposed to prove some complex looking polynomial is equivalent to another complex looking polynomial would you really want to use a rewrite chain instead of saying "by ring" ? That just sounds like you are making your life unnecessarily hard.

[Shreyas Srinivas]

Fair. I guess I am trying to find a trade off between readability and automation in tactics, and the trade off is at a point where I can read the proof and see all the key ideas falling into place.

[Reid Barton]

Again in practice I think it will be very difficult to get anywhere near the amount of automation you would like.

[Martin Dvořák]

Yeah. The tactics are far less powerful than what we wish we had. It happened to me only twice in my life that a tactic closed a goal that I didn't see in my head why it holds.

[Andrew Carter]

Wow this got kind of busy, so I was exploring a bit (instead of watching this thread) and learning a lot of lean and I have some more thoughts.
One way to approach complexity is something inherent in the function, so the conceptual lean function of nat.add has some complexity regardless of how how its actually defined (since definitions are effectively omega equivalent this is unavoidable).

One way to define complexity is by encoding the problem in a well-known space, in my code I've used untyped lambda calculus (because lean is lambda calculus based - but also partly I underestimated how much of a pain confluence would be to prove). And then counting steps in the new space, in this case beta-reductions in lambda calculus (it can also be replaced with a cost function - from a quick literature search the time complexity of lambda calculus is a contentious topic - and beta-reductions should have different costs, for example I have adding 2 church numerals as a constant 6 reductions - which at first glance seems wrong, on the other hand unary numerals are basically linked lists and appending two linked lists together can be done in constant time so maybe its not as crazy as it seems). I haven't quite gotten there, but ideally we don't actually need lambda calculus and can do all of the theorem proving about lean functions, just using lambda calculus as the underlying shim.

It culminates with https://github.com/calcu16/lean_complexity/blob/main/src/lambda_calculus/utlc/complexity.lean, which has the example

example : complexity_le nat.add (λ n m, (6:ℕ)) :=
begin
  use encoding.nat.add,
  intros x y,
  apply utlc.encoding.nat.add_distance_le
end

while I did need to reference lambda calculus in the proof, I didn't in the definition. And hopefully there can be enough theorems that its not needed.

[Andrew Carter]

The downside of this approach is that it would be difficult (perhaps impossible) to prove differences in complexity between different algorithms that solve the same problem.

[Andrew Carter]

Ok, got a proof working for nat.sub that doesn't require knowing about the underlying shim but just the complexities of nat.iterate and nat.pred.
https://github.com/calcu16/lean_complexity/blob/main/src/lambda_calculus/complexity/nat.lean

theorem sub_complexity: complexity_le nat.sub
  (cast (by simp) (λ n m, (2 * n + 13) * m + 4)) :=
begin
  have hsub : nat.sub = (λ n m, nat.pred^[m] n),
  { ext1 n, ext1 m,
    induction m generalizing n,
    { simp [nat.sub] },
    simp [nat.sub],
    rw [m_ih, f_iterate nat.pred],
    simp },
  rw [hsub],
  apply iteration_complexity_le pred_complexity,
  intros n m,
  induction m,
  { simp },
  simp at *,
  rw [show (nat.pred^[m_n] n) = (λ a b, nat.pred^[b] a) n m_n, by simp,
      ← hsub,
      show n.sub m_n = n - m_n, by simp[has_sub.sub],
      nat.succ_eq_add_one],
  apply le_trans,
  { repeat { apply add_le_add },
    apply mul_le_mul,
    any_goals { apply nat.sub_le },
    any_goals { apply m_ih },
    any_goals { apply nat.zero_le },
    any_goals { apply le_refl } },
  ring_nf,
end

most of the proof is just math (unfortunately I couldn't convince linarith/nlinarith to do my dirty work), the main work is done by

apply iteration_complexity_le pred_complexity,

which in turn synthesizes the underyling untyped-lambda calculus, but from the nat.sub prover's perspective we just get back a recursive cost function that we need to prove is always less than or equal to our supplied function. Ideally we'd be able to prove directly from nat.sub's definition instead of that nat.iterate shim, but I'm not 100% sure how to manipulate the implicit structural recursion of lean into a a lean theorem (I tried to use nat.rec/nat.rec_on instead of nat.iterate but couldn't get it to work). Theorems for currying and working with pairs seem pretty straightforward, additionally we could probably add O notation on top of this pretty easily (and have an easier iterate lemma).

Responding to @Shreyas Srinivas

Now let's say you are writing a paper where all you care about is that DFS runs in O(|V| + |E|) time. Should you spend time on sorting through these implementations or building your own?
Another thought is that even in this model you could always have proofs of the form

complexity_le dfs O(|V| +|E|) -> complexity_le my_alg O(f)

You do technically run the risk of proving the latter time complexity by proving bottom, but (a) proving lower bounds for an implementation of a mathematical functions is really hard (see P vs. NP) and (b) if it doesn't hold, that kind of invalidates the theorem anyway.

Also if someone comes along later and fills in the proof of dfs, you would get a pure proof of my_alg for free.

[Shreyas Srinivas]

Andrew Carter said:

Ok, got a proof working for nat.sub that doesn't require knowing about the underlying shim but just the complexities of nat.iterate and nat.pred.
https://github.com/calcu16/lean_complexity/blob/main/src/lambda_calculus/complexity/nat.lean

theorem sub_complexity: complexity_le nat.sub
  (cast (by simp) (λ n m, (2 * n + 13) * m + 4)) :=
begin
  have hsub : nat.sub = (λ n m, nat.pred^[m] n),
  { ext1 n, ext1 m,
    induction m generalizing n,
    { simp [nat.sub] },
    simp [nat.sub],
    rw [m_ih, f_iterate nat.pred],
    simp },
  rw [hsub],
  apply iteration_complexity_le pred_complexity,
  intros n m,
  induction m,
  { simp },
  simp at *,
  rw [show (nat.pred^[m_n] n) = (λ a b, nat.pred^[b] a) n m_n, by simp,
      ← hsub,
      show n.sub m_n = n - m_n, by simp[has_sub.sub],
      nat.succ_eq_add_one],
  apply le_trans,
  { repeat { apply add_le_add },
    apply mul_le_mul,
    any_goals { apply nat.sub_le },
    any_goals { apply m_ih },
    any_goals { apply nat.zero_le },
    any_goals { apply le_refl } },
  ring_nf,
end

This is impressive. In general algorithms and complexity people might not see the value in complexity theory expressed in terms of lambda calculus, primarily because they are not accustomed to the model, but also because of the complexity blow up in beta reductions and complexity issues arising from space usage or persistent structures. It might prove to be just the thing that algorithm designers for functional languages want (the line of work starting at Chris Okasaki's thesis), especially considering how hard it is to understand the complexity of algorithms in languages with, say, lazy evaluation, compared to imperative RAM model style descriptions. Haskell people might really like any tool that makes it easy for them to reason about the complexity measures for their code.

[Andrew Carter]

Shreyas Srinivas said:

This is impressive. In general algorithms and complexity people might not see the value in complexity theory expressed in terms of lambda calculus, primarily because they are not accustomed to the model, but also because of the complexity blow up in beta reductions and complexity issues arising from space usage or persistent structures. It might prove to be just the thing that algorithm designers for functional languages want (the line of work starting at Chris Okasaki's thesis), especially considering how hard it is to understand the complexity of algorithms in languages with, say, lazy evaluation, compared to imperative RAM model style descriptions. Haskell people might really like any tool that makes it easy for them to reason about the complexity measures for their code.

It seems to me that the blow up (or lack thereof) in beta reductions is still open, but I'm not an expert here, but I did run into two papers while I was searching: https://arxiv.org/abs/1405.3311 which based on the abstract seems to indicate the number of steps in a "normal" reduction is cost invariant, while https://arxiv.org/abs/cs/0511045 proposes a cost function for call-by-value. I don't actually enforce an evaluation strategy (many of the proofs use normal reduction, but then substitute previous internally which is essentially call-by-value). As I mentioned earlier, at least in the examples I've done so far, I think I could simulate all of the complexities in an imperative language (e.g. the constant time of nat.add doesn't bother me since I could use a linked list).

However, any cost model could be plugged instead of counting the number of beta reductions and all of the rest of the machinery should still hold. One thought I had since yesterday is that complexity_le could be defined with a class of the underlying model, then people could prove complexities about any model instead of just utlc, for example in any model where dfs has a O(|V|+|E|) runtime (and some basic rules about composition) then my_alg has a runtime of O(f(n)).

That being said, the reason I ended up going down the lambda calculus rabbit hole was because it seemed intuitively easier to prove composition properties of lambda calculus vs a RAM model or TM (and the nat input restriction on partrec seemed too restrictive). In a RAM machine you have to prove that pure functions that take pointers somehow only touch the memory they are supposed to touch and that pointers don't overlap, or if they do overlap its intentional etc. whereas with a functional model we get that for free.

[Shreyas Srinivas]

I can't see this pointer issue causing us any trouble. Do you have any examples?

[Shreyas Srinivas]

I am not entirely clear on how the papers circumvent the explosion in term size with beta reduction (because I only skimmed them. Time crunch). But the polynomial overhead alone is not something we can really accept. There are too many placeswhere polynomial factors are relevant.

[Andrew Carter]

I guess I'm having trouble envisioning general proofs of things like (a → b) → (a, c) → (b, c), because what if the (a → b) transformation messes with c. Similarly a function like memmove (3) has to choose the iteration order in order to avoid smashing existing data. Maybe its not difficult at all, but I'm not seeing the strategy/invariants. On the other hand for lambda calculus, just making sure everything is closed gets you pretty far, and making sure the "data" is in normal form gets you the rest of the way. That being said most of the machinery is replaceable, so if you replace the "g·(@encode α e a)" and "g ≡β (@encode _ e f)" with a different model (or change the cost of ≡β) everything above it should still work.

So I just skimmed the paper as well, but I think its conceptually similar to my argument about a constant time unary add. You can represent n copies of something in log(n) time/space (or equivalently 2^m copies of something in m time/space) and it only becomes a problem if you actually try and use them, but if you do use them then it takes n/2^m beta reductions anyway. Using the nat example, while adding a number in unary is O(1) comparing two numbers is O(n), while in a binary nat adding two numbers is O(log n) and comparing two numbers is also O(log n). I think both of these are achievable both in lambda calculus and practically.

I think the polynomial term is probably overblown in practice, the biggest thing is that you would have to use trees instead of arrays which gives a log n factor, (although there are structures such as finger trees where even that is avoidable). Additionally if you access/mutate the memory in a structured manner (such as with map or fold) then it remains constant time. I would actually argue that constant time random access is a practical fiction anyway and given that we live in a 3D world with a speed-of-light upper bound, the best you can actually get is O(n^(1/3)) random access which is considerably worse than O(log n). Is there a particular (useful) algorithm (or class of algorithms) that you are thinking of that an imperative model and the lambda calculus equivalent would have more than a logarithmic difference?

[Shreyas Srinivas]

The approach we hashed out here was a step counter with a prog type. A cost function, specific to the model, determines how operations are counted as they are built up from other operations. So for a data structure of type \a, the respective insert/update operations are expressed in terms of the operations in prog.

About your question: Ignoring polynomial factors is out of the question for fine grained complexity, most query-based models, complexity of dynamic algorithms, PCPs, parallel complexity classes, circuit complexity etc.

[Shreyas Srinivas]

That's just the tip of the iceberg

[Shreyas Srinivas]

In general, to be useful as a library for theorists, model specific complexities will be required, so just doing everything in utlc is not going to be either useful or easy to translate results into

[Shreyas Srinivas]

In general, there are so many insights/results that are gained from one model and adapted to another through more clever results, that we will not be able to escape defining a gazillion models. Starting with the RAM model makes sense because it probably has the least "moving parts" and is core to undergraduate material, while also serving as the basis for many other models.

[Shreyas Srinivas]

utlc won't easily transfer to other models. So we will be spending so much time writing non-tri ial translations, provided they exist in the first place

[Andrew Carter]

Yeah, the step here is a β-reduction, and at the moment every reduction has a cost of 1.

| In general, to be useful as a library for theorists, model specific complexities will be required, so just doing everything in utlc is not going to be either useful or easy to translate results into
What I would like to prove is things about mathematical functions, as in the proof of sub there probably isn't actually a need for a prover to use utlc beyond a few primitives (or micro-optimizations).

I don't think query-based models or dynamic algorithms have anymore than a polylog difference (happy to take a reference otherwise). For the most part I think the polynomial factor comes from a reduction from a TM and the strong church-turing thesis. PCPs have a problem of generating random numbers in any model (you could attach an RNG as a list of bits lambda calculus argument though and then make arguments about it over the space of all lists). Parallel complexity and circuit complexity are difficult with either approach, especially if the problem isn't trivially parallelizable (that being said there is a notion of a parallel β step for those that are).

Given that lean is lambda calculus based, I would argue that a lambda-calculus based model has the least moving parts. Ideally most of the work can be done similar to sub where the utlc model isn't even touched, and so if there are other models with similar properties then the proofs transfer over directly. Even more so since the algorithms can be written in lean. The model is just a shim to prove things about mathematical functions.

[Andrew Carter]

Somewhat more concretely, I'm pretty sure I could prove (at some point, still need more machinery) that if the CS 125 RAM model has a cost function of w (or log S) for each step (except for division and multiplication, I'm not sure why division is one of the primitives) then a lambda calculus model could simulate it within a constant factor. That being said the reverse direction I'll grant is less obviously true.

[Shreyas Srinivas]

Another reason to pursue RAM is, in addition to its direct applicability: We might attract more theorists, like mathlib attracted mathematicians, if we work in models that most theorists already understand

[Shreyas Srinivas]

At least conceptually, RAM and TM are fundamental to algorithms and complexity. A lot of research would have to go towards addressing the issues with time and space complexity issues related to beta reduction, going by the papers you suggested.

[Andrew Carter]

Shreyas Srinivas said:

At least conceptually, RAM and TM are fundamental to algorithms and complexity. A lot of research would have to go towards addressing the issues with time and space complexity issues related to beta reduction, going by the papers you suggested.

My experience in class was that a lot of algorithms were described in a recursive manner conceptually similar to lambda calculus, for example the Master Theorem is formulated in terms of a recurrence relation. Also while I don't think there is a polynomial difference between RAM and LC, there is very much a polynomial difference between RAM and TM.

That being said, as I mentioned earlier with classes there is lots of room for multiple models (and if I can prove a linear relationship from RAM back to LC, then I'd get any RAM theorem's "for free"). Personally, I can vaguely see the path from where I am now to showing something like the Master theorem in UTLC, because of reasons like composability I don't see a similar path for RAM. But that doesn't mean you shouldn't try.

[Shreyas Srinivas]

As far as I know a single beta reduction can have a quadratic overhead ( size of the lambda abstraction x size of the substituted term) and reduction to a normal form can have exponential overhead when translated to RAM. We probably need to adopt highly specific kinds of reduction rules to avoid the exponential time and space complexity blow up. This makes it a highly unnatural way to work with for theorists.

[Shreyas Srinivas]

And these overheads completely ignore other complexity measures like space complexity (or sample complexity for learning algorithms)

[Shreyas Srinivas]

The formulation needs to remain intuitive to people in the field. Recursive algorithms are an important subset of algorithms, but even there, you would run into issues where destructive updates and non destructive updates are simultaneously used, each having different complexities. All in just one model. Now if you ask theorists to learn PL methods to encode such ideas in LC, that is a sure shot way to lose their interest. The typical STOC/FOCS/SODA author does not care about functional programming language algorithms for a very good reason.

[Shreyas Srinivas]

They are a very small niche in the field.

[Shreyas Srinivas]

Expecting CS theorists to encode their work in utlc style would be akin to asking mathematicians to stick to constructive proofs

[Shreyas Srinivas]

Perhaps there will come a time when substantial numbers of theorists take an interest in solving algorithmic problems efficiently in functional programming (something like an entire session in the top conferences for a few years in a row), but even then the vast majority of existing results will assume RAM or some such model.

[Shreyas Srinivas]

OTOH, perhaps this UTLC model could be included among others in mathlib, as a way to encourage exploration

[Andrew Carter]

I would argue it might be somewhat akin to asking mathematicians to encode their theorems in dependent type theory. I think there could be a suitable stable of theorems such that anyone wouldn't even be aware or have to interact with the underlying model, in the same way that you could get reasonably far without understanding dependent type theory (certainly I'm confused about the casting I have to do).

That being said, I understand a path forward for UTLC, I don't understand a path forward for RAM. If you know or can point to the equivalent transformations (f.x. f → Λ Λ ↓0·f·↓1 for iterate) for RAM I'm always happy to learn. But I don't really know lean (I ran through the tutorials in November) and I'm a software engineer by trade (I suppose ironically my C++ is orders of magnitude better than my Haskell, so if I could figure out a path forward for the RAM model I'd be more than happy to switch), so in terms of tangible results its either UTLC or nothing. But I'm also happy to collaborate on a multi-model environment if you understand the path forward for the RAM model.

[Andrew Carter]

I'm reminded of a comment one of my CS professors made about my infatuation with provable programming languages, "the problem is that you have to actually prove to the computer you know what you are doing".

[Shreyas Srinivas]

Andrew Carter said:

I would argue it might be somewhat akin to asking mathematicians to encode their theorems in dependent type theory. I think there could be a suitable stable of theorems such that anyone wouldn't even be aware or have to interact with the underlying model, in the same way that you could get reasonably far without understanding dependent type theory (certainly I'm confused about the casting I have to do).

That being said, I understand a path forward for UTLC, I don't understand a path forward for RAM. If you know or can point to the equivalent transformations (f.x. f → Λ Λ ↓0·f·↓1 for iterate) for RAM I'm always happy to learn. But I don't really know lean (I ran through the tutorials in November) and I'm a software engineer by trade (I suppose ironically my C++ is orders of magnitude better than my Haskell, so if I could figure out a path forward for the RAM model I'd be more than happy to switch), so in terms of tangible results its either UTLC or nothing. But I'm also happy to collaborate on a multi-model environment if you understand the path forward for the RAM model.

The path is as I described previously. Since we are talking about RAM, the projection operations would happen one after another and their complexities would be added up

[Shreyas Srinivas]

Proving the correctness of imperative descriptions of algorithms is reasonably well understood. This is different from proving their implementation in an actual language. As a haskeller you might have used Algebraic Data Types to encode grammars for small languages. We can do something similar in lean. A toy imperative language that allows us to introduce variables, modify them, conditional statements, loop constructs, procedure definitions, and procedure calls. Then for RAM, we identify types and operations with unit cost, and compose the complexity of operations for the rest of the language

[Shreyas Srinivas]

We can probably make it more intuitive with clever uses of notations and macros

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

One way to circumvent the need to construct data values explicitly in the toy language, is to define a cost function for data types and value constructors instead.

[Andrew Carter]

Shreyas Srinivas said:

The path is as I described previously. Since we are talking about RAM, the projection operations would happen one after another and their complexities would be added up

I think what is needed here is a function of type (RAM prog) → (RAM prog) → (RAM prog), "running them one after another" is actually already handwavy, since running the first program is going to pollute the memory of the next program (and the next program might smash the results of the first one). Even more so if you want to consider space complexity (what can be saved etc.).

[Shreyas Srinivas]

Theorists, with the honourable exception of data structure designers can be hand wavy about that. But a safe way to account for space complexity in this case is to add explicit modify and destroy functions to data types, with the corresponding cost functions tagged. So you need explicit constructors and destructors and cost functions which compute current as well as maximum overall resource usage, as they traverse the program

[Shreyas Srinivas]

Space complexity conscious theorists often need to specify where memory gets reused in any case. Adding destructors makes it explicit

[Shreyas Srinivas]

I totally do expect sequential composition of that form, with one caveat. For a space complexity conscious definition of RAM, additional state in the form of variables names in memory with their storage cost annotation will have to be carried around.

[Shreyas Srinivas]

For most theoretical algorithms however, we don't have to deal with such updates. These are implementation details. Typically, any given data structure has certain methods to access and update it (with the respective costs). Theorists are happy to operate on data at this level of abstraction

[Shreyas Srinivas]

For the data structure folks who are trying to save every last bit of storage (succinct data structures for instance), we will need to use a modified version of prog which is annotated with some information about it's memory usage at each statement and checks for permitted memory accesses.

[Shreyas Srinivas]

Starting with ram model time complexity and TM related theorems is already a non-trivial task.

[Andrew Carter]

Shreyas Srinivas said:

Starting with ram model time complexity and TM related theorems is already a non-trivial task.

Which is why I started with utlc (which is itself non-trivial, but slightly more trivial in my opinion at least). But yeah, computers don't really do hand wavy.

[Praneeth Kolichala]

There is a paper (discussed before on this Zulip) that demonstrates mechanization in Coq using lambda calculus, but it seems the semantics (in terms of TM's) is nontrivial.

Note that ultimately, we want to prove interesting things about our computational model, so while we can make the model more and more complex, this will make showing the existence of a complete problem more and more difficult. Thus, it seems inevitable that at some point, you will need to get to some "lower level" (Such as TM's, circuits) even if you start at a high level language such as lambda calculus.

By the way, I would like to mention that I also have a repo that has made some nontrivial progress towards defining polynomial time here. I have a new version that is making progress towards Cook-Levin (the key idea is to use circuits as the low level language, so that we get CIRCUIT-SAT as our NP-hard problem). I will say more about this soon-ish hopefully as soon as I clean up some of the code.

[Mario Carneiro]

@Praneeth Kolichala , it would be nice if you could attend Martin's meeting as well, I would like to make sure your plans are represented there

[Mario Carneiro]

oops, I see now you already responded

[Martin Dvořák]

Praneeth Kolichala said:

Note that ultimately, we want to prove interesting things about our computational model, so while we can make the model more and more complex, this will make showing the existence of a complete problem more and more difficult.

To me, it seems to be a clear reason to not make the model more and more complex. Instead, we should make the API more and more rich.

[Martin Dvořák]

Andrew Carter said:

I think what is needed here is a function of type (RAM prog) → (RAM prog) → (RAM prog), "running them one after another" is actually already handwavy (...)

Hitting the nail on the head!

[Shreyas Srinivas]

We also need to make sure we are not doing something so niche that theorists in these fields don't care about it. An LC-based model is a highly esoteric choice in this sense, with highly non-trivial, to unacceptable translation overheads to other models.

[Martin Dvořák]

FYI, @Mario Carneiro in his paper "Formalizing computability theory via partial recursive functions" writes:
image.png

[Martin Dvořák]

image.png

[Shreyas Srinivas]

We don't have to reduce everything to TMs either

[Shreyas Srinivas]

But for basic complexity theory TMs are unavoidable

[Shreyas Srinivas]

They key would be start with TMs, prove equivalence to RAM and translations for complexity classes etc. And define classes for RAM from this. Beyond that point, stay in RAM

[Shreyas Srinivas]

The one model rules all approach will never work in algorithms and complexity

[Andrew Carter]

Shreyas Srinivas said:

The one model rules all approach will never work in algorithms and complexity

I agree, and a couple of more thoughts,
(1) I think if you can prove that a model supports the arrow laws within a certain amount of time/space, probably the same overall machinery can be reused for each model. I think I'm getting close to to the point where I can intuit the cost function either from a monad or maybe from pure lean directly. For example the proof for nat.mul is super mechanical except for (a) the choice of function decomposition (apply *_complexity_le) (b) proof the function is the same as nat.mul (lines 122-129) and (c) proofs that the recursive bounds are actually correct (lines 106 -11)
https://github.com/calcu16/lean_complexity/blob/e3992afdfca1dcdec2b7a37528d50660765c5470/src/lambda_calculus/utlc/complexity/nat.lean
(2) This means that machinery can be built out with any model in parallel with alternative models

Martin Dvořák said:

To me, it seems to be a clear reason to not make the model more and more complex. Instead, we should make the API more and more rich.

(3) I'm wondering if its the opposite at least in regards to the RAM model, RAM is essential assembly and assembly doesn't have an explicit notion of things like data structures (you can encode them of course), perhaps if we had a jvm model (or rust model - which tracks sharing better) it would be both more usable and easier to make composability arguments about.

[Tomaz Gomes]

Hey, I didn't read the full discussion, but I had a PR opened in mathlib3 about this some time ago: https://github.com/leanprover-community/mathlib/pull/14494

I am only having time to port it now to lean4 and I am in the middle of the process. I am wondering whether this still has some value to mathlib

[Martin Dvořák]

I don't think your code represents complexity theory.
You don't define any predicates that would guarantee any bound on time or space complexity.

Consider one of your results:

theorem insertion_sort_complexity :
  ∀ l : list α, (insertion_sort r l).snd ≤ l.length * l.length :=

This theorem says:
If we believe that insertion_sort correctly counts its steps and the number of steps is stored in the .snd part of its output, then we know it performs at most l.length * l.length steps.

Your code doesn't enable us to express propositions such as:
"Sorting can be solved in quadratic time."

I think it is really nice that you formally verified the correctness and complexity of some concrete algorithms.
Unfortunately, it cannot be incorporated into a library of reusable results and I don't see any way how to build complexity theory on top of it.
Therefore, I suggest not to include your code into Mathlib.

[Shreyas Srinivas]

Martin Dvořák said:

If we believe that insertion_sort correctly counts its steps and the number of steps is stored in the .snd part of its output, then we know it performs at most l.length * l.length steps.

Your code doesn't enable us to express propositions such as:
"Sorting can be solved in quadratic time."

I think it is really nice that you formally verified the correctness and complexity of some concrete algorithms.
Unfortunately, it cannot be incorporated into a library of reusable results and I don't see any way how to build complexity theory on top of it.
Therefore, I suggest not to include your code into Mathlib.

Disagree. You need algorithms and verification of their complexity to even begin to fathom a reasonable description of complexity theory.

[Shreyas Srinivas]

Without that you have no reductions to begin with.

[Shreyas Srinivas]

We benefit from a port of "verified functional algorithms". So this is a good start.

[Shreyas Srinivas]

If we want to make the results usable, then we must work to build such a usable framework. For example, we could define a structure that is parametrized by a function, its input-output invariant, and its time complexity, and components for the respective proofs. Then an instance of this structure would we used as a parameter of another function corresponding to an algorithm, rinse and repeat.

[Johan Commelin]

I think Martin raises a fair point. I'm not a complexity theorist, but afaik if you honestly want to prove complexity bounds then you need to prove stuff about Turing machines (which exist in mathlib) and implement your algorithm on something like that. Otherwise we indeed need to trust that the .snd component correctly counts the time complexity. And even if everybody tries their best and acts in good faith, we are going to mess up anyways, because we can't prove and verify the correctness of our claims.

There are of course two mostly orthogonal components here: verifying that some algorithm behaves according to spec (which can be done without all the TM business) and verifying complexity bounds (which I think really needs a beafy foundation of TM stuff or something similar). It would be very interesting to see if in Lean 4 we can have some sort of TM-dsl or TM-compiler or anything like it that will make it easier to perform such complexity analysis.

[Shreyas Srinivas]

We could implement some version of the textbook toy imperative language IMP which tracks both invariants and steps. In an earlier discussion, we observed that if space complexity is not an immediate concern, then this is viable. Space complexity makes life harder (memory model and everything).

On the other hand, CS is full of horizontal abstractions. These are "horizontal" in that different abstractions include different concepts, but neither subsumes the other. Computational models are themselves examples of this. It helps to have a recursive description of a function to prove its properties. Later, an equivalence theorem for an IMP program implementing the same function could be shown, and the complexity result derived from it.

[Shreyas Srinivas]

It going to be difficult if we want a single DSL from which we can analyze all complexity parameters and correctness

[Scott Morrison]

@Shreyas Srinivas, sounds like you should write some code. :-)

[Shreyas Srinivas]

I should. I really should.

[Hunter Monroe]

To make some incremental progress, I created PR #8790 building on TM2ComputableInPolyTime to define polynomial time computable functions, indicator functions for languages decidable in polynomial time, and a verifier that could be used to define NP. There are important issues discussed over several years and work done on PRs/repositories regarding models, encoding, counting steps/space etc but can we take some baby steps?

[Martin Dvořák]

Why did you @Hunter Monroe close your PR?

[Hunter Monroe]

Please see the reopened the pull request defining polynomial time computation only for binary strings (List Bool). This avoids for now distinguishing acceptable encodings (a TM2ComputableInPolyTime can factor integers in polynomial time with a unary input alphabet).