Feat : Query complexity model for algorithms#275
Feat : Query complexity model for algorithms#275Shreyas4991 wants to merge 78 commits intoleanprover:mainfrom
Conversation
Co-authored-by: Sorrachai Yingchareonthawornhcai <sorrachai@users.noreply.github.com>
Co-authored-by: Sorrachai Yingchareonthawornhcai <sorrachai@users.noreply.github.com>
…ity-freeM-shreyas
…ity-freeM-shreyas
…ity-freeM-shreyas
Shreyas4991
changed the title
| /-- Equivalence between `TimeM α` and `WriterT Nat Id α` as plain types. -/ | ||
| def equivWriter (α : Type) : TimeM α ≃ WriterNat α where | ||
| toFun m := (m.ret, m.time) | ||
| invFun w := ⟨w.1, w.2⟩ | ||
| left_inv m := by cases m; rfl | ||
| right_inv w := by cases w; rfl |
There was a problem hiding this comment.
This is misleading; sure, the types have the same cardinality, but this isomorphism is not canonical; it does not preserve bind or tick.
There was a problem hiding this comment.
This comes from upstream. I am not touching TimeM. I am of the opinion that we can delete the whole file. This model already subsumes everything TimeM does. And TimeM is too thin a wrapper to serve any purpose.
There was a problem hiding this comment.
To clarify, does "upstream" mean #201? I don't believe this is an existing definition in the main branch.
There was a problem hiding this comment.
Possible. I don't recall touching TimeM at all. Tbh if we wanted to put this equivalence into CSLib at all, I would just change TimeM to an abbrev.
There was a problem hiding this comment.
Can you merge master and delete this file? master already defines TimeM in a different file, let's not repeat it.
There was a problem hiding this comment.
Will do. I think this is a relic of #201
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
I plan to remove the circuits stuff and add it to a separate PR. |
| (TimeM.bind m f).ret = (f m.ret).ret := rfl | ||
|
|
||
| -- this allow us to simplify the chain of compositions | ||
| attribute [simp] Bind.bind Pure.pure TimeM.pure |
There was a problem hiding this comment.
Note that this is cursed; I've removed it in #321
Shreyas4991
force-pushed
the
query-complexity-freeM-shreyas
branch
from
c965ec7 to
0a8316d
Compare
…ity-freeM-shreyas
…ests some useful API lemmas
…ests some useful API lemmas
|
Please merge master. |
Just did that a few hours ago |
There was a problem hiding this comment.
This file already exists with a different name, please fix the merge conflict by removing one of the duplicates.
4 participants
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 :
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 fromTimeMs model. But with custom Cost types with a specific field forpure, 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