Feat : Query complexity model for algorithms

[Shreyas4991]

Generalizing @tannerduve 's query complexity model. This model of algorithmic complexity provides a lightweight approach to complexity verification of algorithms, similar to #165

However it offers several improvements over #165 :

1. No explicit ticks needed, so the chances of making mistakes like forgetting to count specific calls is removed.
2. The operations which are counted are made explicit as an inductive type and a model of this type.
3. The model of a query type accepts custom cost structures so long as you can define addition and a 0 operation on them (basically additive monoids suffice).
4. With a notion of reductions between models, this approach is more modular for the algorithm specifier, allowing high level specs of operations which can be translated into simpler query models later.

Update to the below drawback : The model requires users to choose a cost for each pure operation upfront by a typeclass instance for a given type of Cost. This is a departure from TimeMs model. But with custom Cost types with a specific field for pure, these costs can be separated from that of calls to queries.

One drawback : It is still possible to sneak in free operations inside pure. However this is unavoidable in any lightweight monadic approach. A deeply embedded DSL is the only foolproof way to avoid this. Nevertheless this approach removes annotation and review burden and ensures that any actual call to a query will be counted. Thus it is easy to notice when a monadic operation is not being called.

Zulip Discussion Thread: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Query.20model.20for.20Algorithms.20complexity.20.3A.20updates/near/569606456

[eric-wieser]

Deleting this seems counter-productive

[Shreyas4991]

That came from main. I don't use it in this PR. I am just not sure how to get rid of it.

[eric-wieser]

I think "came from main" means "I did a bad merge of main"

[eric-wieser]

Suggested change

	evalQuery q :=
	match q with
	| .write l i x => l.set i x
	| .find l elem => l.findIdx (· = elem)
	| .get l i => l[i]
	evalQuery
	| .write l i x => l.set i x
	| .find l elem => l.findIdx (· = elem)
	| .get l i => l[i]

etc

[eric-wieser]

This belongs in the file defining FreeM

[Shreyas4991]

Agreed. Do note that the current file has a lot of things that should move to separate files.

[eric-wieser]

Suggested change

	def eval [Add Cost] [Zero Cost]
	(P : Prog Q α) (M : Model Q Cost) : α :=
	match P with
	| .pure x => x
	| .liftBind op cont =>
	let qval := M.evalQuery op
	eval (cont qval) M
	def eval [Add Cost] [Zero Cost]
	(P : Prog Q α) (M : Model Q Cost) : α :=
	Id.run <| P.liftM fun x => pure (M.evalQuery i)

[eric-wieser]

Why not write these to look more like functions,

Suggested change

	| compare : (a : Vector α n) → (i : ℕ) → (val : α) → VecSearch α Bool
	| compare (a : Vector α n) (i : ℕ) (val : α) : VecSearch α Bool

[eric-wieser]

This is unsafe, as it lets the algorithm access the underlying data structure. At minimum you need

Suggested change

	inductive VecSortOps (α : Type) : Type → Type where
	| swap : (a : Vector α n) → (i j : Fin n) → VecSortOps α (Vector α n)
	| cmp : (a : Vector α n) → (i j : Fin n) → VecSortOps α Bool
	| write : (a : Vector α n) → (i : Fin n) → (x : α) → VecSortOps α (Vector α n)
	| read : (a : Vector α n) → (i : Fin n) → VecSortOps α α
	| push : (a : Vector α n) → (elem : α) → VecSortOps α (Vector α (n + 1))
	inductive VecSortOps (VecType : Nat → Type) (α : Type) : Type → Type where
	| swap : (a : VecType n) → (i j : Fin n) → VecSortOps VecType α (VecType n)
	| cmp : (a : VecType n) → (i j : Fin n) → VecSortOps VecType α Bool
	| write : (a : VecType n) → (i : Fin n) → (x : α) → VecSortOps VecType α (VecType n)
	| read : (a : VecType n) → (i : Fin n) → VecSortOps VecType α α
	| push : (a : VecType n) → (elem : α) → VecSortOps VecType α (VecType (n + 1))

[Shreyas4991]

Good point. I'll get back to this tomorrow noon. A Finvec would be the better option.

[eric-wieser]

On second thoughts, this still doesn't help; you can't let the algorithm have access to a at all, otherwise it can do classical if VecType = Vector then cheat else alg

[Shreyas4991]

Any monadic dsl will have this issue.

[eric-wieser]

I think the issue goes away if the dsl can only access the vector through opaque variable indices?

[Shreyas4991]

That was my data structure hiding idea. Make the vector opaque. That is, remove the vector from the query and add it to the model. The problem is removing it means we can't write monadic Progs that are recursive on specific subvectors.

[Shreyas4991]

Another issue with this idea is that currently the second parameter of the query type is the return type of the operation. If we can't have that, then we can't have the monad structure. Without flexibility on the return type of the query, we lose a lot of flexibility in our queries

[chenson2018]

Make sure with the move to the module system you now run lake exe mk_all --module

[chenson2018]

Can you clarify what you envision happening to this module? If what you are proposing subsumes this, I vote that we replace it outright with the new framework. I think we can make room for a lightweight monadic DSL and Boole's deep embedding, but I don't want to encourage any more fragmentation than that.

[Shreyas4991]

This PR largely subsumes TimeM. In principle, because TimeM allows arbitrary (occurrences of) operations to be checkmarked, it is more flexible, but as I argued in December, this flexibility is a footgun and a limitation in so many ways. As long as we are systematically counting operations, this model clearly subsumes TimeM.

There is one footgun any monadic DSL will have, namely, sneaking in of computations with pure. This is fundamental to a monad. However even here, I have just managed to improve the situation a bit, by adding a notion of PureCosts as a typeclass and adding custom pure fields in some cost models. As you can see in the #evals as lines 222 and 401, this model can capture how many pure operations are used as well. This breaks the equivalence with TimeM's model of assigning 0 cost to pure, but gives us room for a sanity check as reviewers of code.

Overall I agree with you that this model can entirely replace TimeM.

[eric-wieser]

Suggested change

	if id ∉ s₂
	then
	id :: s₂
	else
	s₂
	insert id s₂

[eric-wieser]

Suggested change

	| .const id _ =>
	if id ∉ countedIDs then id :: countedIDs else countedIDs
	| .const id _ => insert id countedIDs