feat: query complexity via free monads #201
Conversation
tannerduve
force-pushed
the
query-complexity-freeM
branch
from
7fafeed to
a32b00d
Compare
Co-authored-by: Sorrachai Yingchareonthawornhcai <sorrachai@users.noreply.github.com>
Co-authored-by: Sorrachai Yingchareonthawornhcai <sorrachai@users.noreply.github.com>
feat: Generalize Query Model
| def evalQuery : {ι : Type} → QueryF ι → ι | ||
| | _, .read _ => 0 | ||
| | _, .write _ _ => PUnit.unit | ||
| | _, .cmp x y => x ≤ y |
There was a problem hiding this comment.
Shouldn't this be more like
def evalQuery [LE α] [Inhabited α] : {ι : Type} → QueryF ι → StateT (Array α) ι
| _, .read i => return (← get)[i]!
| _, .write i x => do modify fun a => a.set! i x
| _, .cmp i j => do let a ← get; return a[i]! ≤ a[j]!You need a real model if you want to prove correctness
There was a problem hiding this comment.
The Inhabited here flags that this query API is not great, as it allows illegal queries. You might want to parametrize QueryF by the array length.
There was a problem hiding this comment.
thanks. That's a valid point. Fwiw, this entire example has several points where it is still possible to sneak in flawed code. Currently I am trying to get the typeclasses and composition theorems right, then I can redo this example.
There was a problem hiding this comment.
Do note that evalQuery is meant to execute the computations. The time complexity evaluation will be done by translation to the time monad with ticks
| /-- Write value `v` at index `i`. -/ | ||
| | write : Nat → Nat → QueryF PUnit |
There was a problem hiding this comment.
If you refer to names in the docstring they should exist in the code
/-- Write value `v` at index `i`. -/
| write (i : Nat) (v : Nat) : QueryF PUnitetc
| open Cslib.Algorithms | ||
|
|
||
|
|
||
| /-- The Model for comparison sorting natural-number registers.-/ |
There was a problem hiding this comment.
Why not generalize to arbitrary registers?
There was a problem hiding this comment.
This is still WIP. I will make this change once I have generalized the query type, and I am instantiating it.
There was a problem hiding this comment.
The PR started from a proof-of-concept in the zulip, posted by Tanner. It has some way to go.
| /-- Read the value stored at index `i`. -/ | ||
| | read : Nat → QueryF Nat | ||
| /-- Write value `v` at index `i`. -/ | ||
| | write : Nat → Nat → QueryF PUnit |
There was a problem hiding this comment.
The fact your sorting implementation doesn't use these at all suggests that they're not really useful as query operators. Even if you did force the API to manually read and write, I don't think you would be able to prevent an implementation that:
- reads every entry in sequence into a
List - does a mergesort
- writes the outputs back
which makes counting reads and writes pretty uninteresting.
There was a problem hiding this comment.
The correct model would have compare and swap operations.
| namespace Prog | ||
|
|
||
|
|
||
|
|
||
| /-- Conditional branching on a boolean program. -/ | ||
| def cond {QType} {α} (b : Prog QType Bool) (t e : Prog QType α) : Prog QType α := | ||
| b.bind (fun b' => if b' then t else e) | ||
|
|
||
| /-- A counting loop from `0` to `n - 1`, sequencing the body. -/ | ||
| def forLoop {QType} (n : Nat) (body : Nat → Prog QType PUnit) : Prog QType PUnit := | ||
| go n | ||
| where | ||
| /-- Auxiliary recursive worker for `forLoop`. -/ | ||
| go : Nat → Prog QType PUnit | ||
| | 0 => pure () | ||
| | i + 1 => | ||
| body i >>= fun _ => go i | ||
|
|
||
| end Prog |
There was a problem hiding this comment.
As discussed on zulip, this is do if and do for, no need for new defs
3 participants
This PR introduces a generic query-based computation model, and reuses the
TimeMmonad from #165 to give it a simple cost semantics