Does Query Model allow matrix mul in O(N^2) time ?

Stream: CSLib

[TongKe Xue]

Suppose we allow +, -, *, / on arbitrary precision numbers in one op:
Consider a vec of n elemes, each of log n bits. We can encode this as a big number of (n log n) bits in O(n) time.
We can take the dot product of two Vecs in O(1) time: amortize the encoding time, do regular integer mul on two (n log n) bit numbers, use mod to read off answer.
This would allow multiplying two NxN matrices, each with O(log n) bit number, in O(n^2 time):

1. encode all the rows of matrix A in O(n) time
2. encode all the rows of matrix B in O(n) time
3. for each cell of output, do dot product of corresponding row/col in O(1) time

How does Query Model prevent such a formalization?

[RAM model breaks this because we can only multiply , for some fixed constant c, (c log n) * (c log n) mul in O(1) time; a [n log n]-big number would be forced to take atleast [n/c] cells].

[Shreyas Srinivas]

What queries are you using?

[Shreyas Srinivas]

you keep speaking of "the query model". It's actually many models wrapped into one. If you provide a matrixMult query with input matrices, then you could even accomplish it in one query.

[Shreyas Srinivas]

When you want to reason about matrix multiplication, you would fix a parameter w for word size and allow input entries to range from 0 to 2^w - 1

[Shreyas Srinivas]

You are not going to get some big gotcha with encoding tricks since you'd have to choose the right kind of queries to get the result you seek

[TongKe Xue]

You are not going to get some big gotcha with encoding tricks since you'd have to choose the right kind of queries to get the result you seek

I disagree with this. With the CLRS-RAM model, you only have to get the model right once.

With the "many different queery model", it seems every time you define a new "query model", you have to make sure that model defines "ticks" correctly (limit on wordsize, for example).

[Shreyas Srinivas]

I hate to break it to you but that's how algorithms theory works. I admit that we don't teach these levels of abstraction in undergrad since we are not particularly concerned about these translations. The combinatorial stuff is much more central to the subject. You can get even more gotchas with the knapsack NP Hardness result. The knapsack problem is NP Hard but has a pseudopolynomial algorithm. This is fine. We know when we need to care about these representation issues and when we don't

[Shreyas Srinivas]

There are a gazillion models and variants out there

[Shreyas Srinivas]

Btw, there's something called the pointer machine model. Check out how much time integer multiplication takes there

[TongKe Xue]

Philosohically:

1. I want a tiny "trusted" base (ex: CLRS style RAM model).
2. I do NOT want to have a new "trusted" base for every class of algorithms where we manually assign costs to constructors and then make an informal argument that it is correct.
3. I believe the way to avoid (2) is to have everyone agree on a CLRS-style RAM model, and then for new "model creators" to provide lean4 verifiable formal proofs their model "compiles down" to CLRS-style RAM models for time/memory costs.

[Shreyas Srinivas]

3 is not happening. Sorry.

[Shreyas Srinivas]

Many of those models have useful purposes.

[Shreyas Srinivas]

The queries framework is the best way to capture all of them. One can always define translations between queries to do reductions for example.

[Shreyas Srinivas]

But the idea of “everyone agreeing to a strict definition of a ram model” and agreeing to write their algorithms fully formally in it is just not happening. Informally everybody agrees in some agnostic notion of a RAM model, but even there many other models exist for good reasons.

[TongKe Xue]

I agree with 99% of your idea. The only part I disagree on is this notion that for each Query Model, humans assign a cost to each constructor, and there is some informal, socially accepted "proof" that the cost of each constructor is correct.

I believe this "informal + socially accepted proof" should be replaced by a Lean4 verified "mini compiler" that targets some commonly accepted CLRS-style RAM model, and that we prove in lean4 that each of the constructor indeed only take X computation and Y memory.

I think this is an accurate stance on what we agree/disagree on (and it appears neither of us will convince the other of whether there should be a formal lean4 proof of the cost of each constructor of each query model.)

[Shreyas Srinivas]

You are misunderstanding the purpose of this subject. It is not to produce implementable algorithms. That’s a nice added bonus every theorist will like, but not enough to put in the necessary grunt work that offers no fundamentally new insights. The evidence lies in how many procedures of the last 20 years are actually simple enough to be implementable, let alone implemented. Even where implementation is possible, it can be done at a different level of abstraction so as to not obscure the key insights of an algorithm.

[Shreyas Srinivas]

What is of interest is “given a set of basic operations, what can I compute with so and so complexity”

[Shreyas Srinivas]

For example, given matrix multiplication, can I maintain such and such data structures dynamically ?

[Ching-Tsun Chou]

Would it be possible to formalize the Zeno machines as a query model? If yes, let’s do that and collapse all those pesky complexity classes to O(1) and bring the whole field of algorithm design to a successful conclusion. (Needless to say, the preceding paragraph is not meant to be taken seriously.)

[Shreyas Srinivas]

It’s also not a great argument.

[TongKe Xue]

I want:

1. assume X
2. we can show that algorithm i has running time t(i) and memory usage s(i)

You want:

1. for i = 0, ... ; assume model_i
2. then for algorithm A_j in query_model_i, it uses time t(j) and memory usage s(j)

In the above, X = CLRS style ram model.

You want lots of "islands" each with their own assumptions. I just want a single assumption.

I think that is the core of our difference, and neither of us will convince the other.

[Shreyas Srinivas]

those islands can be related by someone who wants them related

[Shreyas Srinivas]

Others can continue building their islands

[Shreyas Srinivas]

Typically you will find that there are many ways to link those islands.

[Shreyas Srinivas]

That' s for the interested person to solve

[Marcelo Fornet]

Both approaches seems compatible to me, we develop the query meta-model, and on top of it we develop the RAM model … and other models.

Then everyone can work on the part they care the most! In particular a lot of the algorithms will be developed for the RAM model due to its practical importance, but connections between models can be made anyway.

[Shreyas Srinivas]

Exactly. If anything this might introduce a tower of abstractions connected through layers of interpretation functions.

[Eric Wieser]

The query complexity design ought to permit something like "evaluate the queries using this RAM model"

[Shreyas Srinivas]

It doesn’t forbid it

[Eric Wieser]

I don't remember if FreeM already has a monadic run that lets you implement the queries in another monad; but it would be easy enough to add it if it is missing.

[Shreyas Srinivas]

You can always translate from one query model to another. The point is, both conceptually and for formalisation, I think it is the abstraction that works best.

[Shreyas Srinivas]

it cleanly separates algorithmic insights for a particular algorithm in a model from insights into how its primitives can be implemented. There are bound to be many ways for the latter. So you can also structure the library to allow multiple complexity theorems for each algorithm corresponding to different translations.

[Shreyas Srinivas]

This separation is incidentally only implicit in the manual tick model, but will be automatic in the query model (by the query type)

[Eric Wieser]

One thing that is hard with the query model is space complexity, since you can't prevent the implementation using storage in the Lean type theory

[Eric Wieser]

This is out of my area of expertise, but probably systems with more exotic things like linear types can protect against this.

[Yuval Filmus]

TongKe Xue said:

I want:

1. assume X
2. we can show that algorithm i has running time t(i) and memory usage s(i)

You want:

1. for i = 0, ... ; assume model_i
2. then for algorithm A_j in query_model_i, it uses time t(j) and memory usage s(j)

Shreyas' view reflects the literature, see for example https://arxiv.org/pdf/1402.1811
In American-style theoretical computer science there are many, many computation models floating around. Each sub-area has its own computational model. I don't know anybody bothered to chart all of them.

[TongKe Xue]

A single model dominates over half of https://en.wikipedia.org/wiki/Introduction_to_Algorithms . Let's just use that model. And if anyone wants to use some new model K, they can implement a compiler/VM for K on the CLRS model.

This, the "trusted kernel" is just the CLRS model, instead of every model out there.

[Yuval Filmus]

This will make CSLib useless for theoretical computer science.
Would you similarly suggest that Mathlib be built on some particular "Calculus 101" textbook and be useless for mathematicians?

[Yuval Filmus]

Since the infrastructure is only going to be developed once, you have to get it right the first time.

[TongKe Xue]

My point is this. There should be a tiny, fixed, trusted "kernel" for Time/Space called K.

Then, if Bob wants to use some new query model M_i, the burden is on Bob to write a compiler from M_i to K and prove properties. Bob does not get to say "M_i has properties P1, P2, P3, ... trust me bro."

[Yuval Filmus]

That’s just not how these models work.
The machine model isn’t supposed to reflect the complexity in some universal CPU.
If I consider real arithmetic to have unit cost (common in computational geometry), I am abstracting away irrelevant details, without claiming that I can actually implement these operations in constant time.

[Yuval Filmus]

Here’s another example. In optimization, the objective function (and sometimes the constraints) are given as oracles. When measuring the running time, we’re interested both in the cost of computation per se and in the number of oracle calls.

[TongKe Xue]

It sounds like your view is leaning towards: Before doing actual work, let's find a model that can formalize all of theoretical CS / optimization.

Whereas my view is: I just want something that I can formalize core CLRS + algorithms + NP completeness reductions + crypto reductions.

I.e. I'm not nearly as ambitious as you (and you raised many interesting theoretical results that are not within the realm of what I wish to formalize.)

[Shreyas Srinivas]

It’s actually the other way around. Producing implementable algorithms is both more tedious (and challenging) and less conceptually useful

[Shreyas Srinivas]

Also the whole point is to allow a family of models with one overarching (meta?) model (queries), not a single model as you suggest

[Shreyas Srinivas]

TongKe Xue said:

It sounds like your view is leaning towards: Before doing actual work, let's find a model that can formalize all of theoretical CS / optimization.

The phrase "actual work" implies that finding a good model is not actual work. Finding good definitions that work for the field is the heart of formalisation. So this is definitely "actual work". Secondly we have figured out a model that works. I am actually implementing it (within severe time constraints).

Whereas my view is: I just want something that I can formalize core CLRS + algorithms + NP completeness reductions + crypto reductions.

And what would the point of this formalisation of CLRS be if it is useless for anything beyond textbook level?

I.e. I'm not nearly as ambitious as you (and you raised many interesting theoretical results that are not within the realm of what I wish to formalize.)

You are welcome to do so. CSLib must however pick good definitions from the beginning if it is to serve its purpose and not become a chaotic forest like AFP. This is also true in mathlib where the discussion on how to encode planar graphs has been happening for months now.

[Shreyas Srinivas]

In short, coming up with proper definitions that can soundly express theorems we care about is "actual work"

[Bolton Bailey]

I recently watched this short talk about #PrimeNumberTheorem+ > Update on tertiary estimate projects , and I found it inspiring and perhaps relevant to this discussion, in the sense that it suggests infrastructure can be built that helps us manage transitions between models and upgrade our understanding as more fine-grained details in the lower level theory are worked out.

[Shreyas Srinivas]

There is some intuitive parallel there yes

[TongKe Xue]

I think we can drop this debate. It is fairly clear that:

1. you and I have different objectives
2. neither of us is going to convince the other
3. this is a waste of both our time

Whether CSLib adopts a foundation closer to your views or closer to my views, I'm okay with both outcomes.

Cheers.

Shreyas Srinivas said:

TongKe Xue said:

It sounds like your view is leaning towards: Before doing actual work, let's find a model that can formalize all of theoretical CS / optimization.

The phrase "actual work" implies that finding a good model is not actual work. Finding good definitions that work for the field is the heart of formalisation. So this is definitely "actual work". Secondly we have figured out a model that works. I am actually implementing it (within severe time constraints).

Whereas my view is: I just want something that I can formalize core CLRS + algorithms + NP completeness reductions + crypto reductions.

And what would the point of this formalisation of CLRS be if it is useless for anything beyond textbook level?

I.e. I'm not nearly as ambitious as you (and you raised many interesting theoretical results that are not within the realm of what I wish to formalize.)

You are welcome to do so. CSLib must however pick good definitions from the beginning if it is to serve its purpose and not become a chaotic forest like AFP. This is also true in mathlib where the discussion on how to encode planar graphs has been happening for months now.

[Shreyas Srinivas]

Fwiw @TongKe Xue your question is also applicable to the TimeM model which is even less specific about what it counts, to a point where you can’t even state proper models and reduction theorems between them or even count different operations separately.

Basically in algorithms we don’t actually care about some specific RAM model directly (indirectly we all love pretending that our sequential algorithms work on RAM but don’t care too much about the details). Algorithms theory is fundamentally answering questions of the form:

Given operations X Y and Z as primitives, how many calls of each operation do we need to compute operation W.

[TongKe Xue]

Let's drop this.

Shreyas Srinivas said:

Fwiw TongKe Xue your question is also applicable to the TimeM model which is even less specific about what it counts, to a point where you can’t even state proper models and reduction theorems between them or even count different operations separately.

Basically in algorithms we don’t actually care about some specific RAM model directly (indirectly we all love pretending that our sequential algorithms work on RAM but don’t care too much about the details). Algorithms theory is fundamentally answering questions of the form:

Given operations X Y and Z as primitives, how many calls of each operation do we need to compute operation W.

[Alok Singh]

TongKe Xue said:

I want:

1. assume X
2. we can show that algorithm i has running time t(i) and memory usage s(i)

You want:

1. for i = 0, ... ; assume model_i
2. then for algorithm A_j in query_model_i, it uses time t(j) and memory usage s(j)

In the above, X = CLRS style ram model.

You want lots of "islands" each with their own assumptions. I just want a single assumption.

I think that is the core of our difference, and neither of us will convince the other.

But I want to assume Y. Why shouldn’t you write a converter from X to Y?

[TongKe Xue]

Because you are not Emperor. If you want to assume Y, you go write a converter from Y to X. It's not the rest of the world's job to serve you.

Alok Singh said:

TongKe Xue said:

I want:

1. assume X
2. we can show that algorithm i has running time t(i) and memory usage s(i)

You want:

1. for i = 0, ... ; assume model_i
2. then for algorithm A_j in query_model_i, it uses time t(j) and memory usage s(j)

In the above, X = CLRS style ram model.

You want lots of "islands" each with their own assumptions. I just want a single assumption.

I think that is the core of our difference, and neither of us will convince the other.

But I want to assume Y. Why shouldn’t you write a converter from X to Y?

[Chris Henson]

Please keep the conversation respectful.

[TongKe Xue]

I've gone ahead and muted the topic. I feel like I'm getting reply quoted by people who just want to argue/debate in an online forum. DM me if you know of cool projects making progress on the CLRS/RAM world view. Cheers.