<div dir="ltr">Abstracting from the details of this particular example, the problem is the following: You want to construct a proof of some proposition P using some sort of search procedure that may or may not deliver an actual proof. So you define<div><br></div><div> search : Maybe P</div><div><br></div><div> proof : P</div><div> proof = unMaybe search</div><div><br></div><div>where</div><div> <br></div><div> unMaybe : (m : Maybe A) {_ : IsJust m} -> A</div><div> unMaybe nothing {}</div><div> unMaybe (just x) _ = x</div><div><br></div><div>When type checking 'proof' the type checker has to run 'search' to see that it is indeed 'just' something so that the implicit IsJust proof can be filled in. The important thing to note here is that 'search' only needs to be evaluated far enough to discover that it is a 'just' and no further. This means that we should make getting to the 'just' constructor as cheap as possible.</div><div><br></div><div>Consider what happens if you implement search in the most straightforward way, simply running the search in the Maybe monad. In this case you need to traverse the search space and build up the proof object (which may be very large), at every step checking that all the substeps came back 'just'. You don't get the final 'just' until you have created the entire proof object.</div><div><br></div><div>The alternative that I'm advocating is that you split the search procedure into a test and a soundness proof for the test:</div><div><br></div><div> test : Bool</div><div> sound : T test -> P</div><div><br></div><div>Here the soundness proof is responsible for constructing the proof object, assuming that the test came back 'true'. We can then implement the search as follows:</div><div><br></div><div> search : Maybe P</div><div> search with T? test</div><div> ... | yes p = just (sound p)</div><div> ... | no _ = nothing</div><div><br></div><div>Now, in order to get to the 'just' constructor we only have to run 'test' and we don't have to worry at all about constructing the proof object.</div><div><br></div><div>Concretely what I did in the me-em example was replace the 'ag' and 'af' functions by two new functions 'ag-now' and 'af-now' implemented as 'search' above (with tests 'ag-test' and 'af-test', and soundness proofs 'ag-proof' and 'af-proof').</div><div><br></div><div>I hope this clarifies things.</div><div><br></div><div>/ Ulf</div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Feb 3, 2016 at 3:34 PM, Jacques Carette <span dir="ltr"><<a href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000">
<div>Where can one read more about
"no-eta-equality" ? I believe that some of my work could benefit
from this as well.<br>
<br>
Similarly, I sought to learn from the changes you did<br>
<a href="https://github.com/UlfNorell/me-em/commit/5930ad6b155244a1ba85abc36a0e79c1333ca7f4" target="_blank">https://github.com/UlfNorell/me-em/commit/5930ad6b155244a1ba85abc36a0e79c1333ca7f4</a><br>
but while I can "read the code", I can't quite understand how this
matches your high-level description. Could you comment a bit
about this? I believe that this would be well worth it, and may
indeed help achieve a reduction in Agda-blame, as outlined in the
first paragraph.<span class="HOEnZb"><font color="#888888"><br>
<br>
Jacques</font></span><div><div class="h5"><br>
<br>
On 2016-02-03 04:31 , Ulf Norell wrote:<br>
</div></div></div><div><div class="h5">
<blockquote type="cite">
<div dir="ltr">I think it's unfortunate, if perhaps not completely
undeserved, that Agda gets blamed every time a program is slow
or uses a lot of memory. When people are writing slow Haskell
programs their first thoughts are "maybe I should try to
optimise my program", not "maybe someone should optimise GHC"
and I wish we could have a little more of that for Agda
programs. There are certainly performance problems in Agda's
compile time evaluator (call-by-name, interpretation overhead,
etc) but that doesn't mean that you can't write programs that
perform reasonably well.
<div><br>
</div>
<div>I had a look at your code and the main performance problem
seems to be that you are too strict in the proof objects
produced by the model checker. In your example the correctness
proof of Peterson's algorithm consists of four (I think)
complete state graphs (with ~14k states) decorated with proofs
that you build up eagerly before deciding that you have a
valid proof. If you instead separate the decision procedure
from the construction of the proof object you only need to run
the former to be sure that you have a proof, and can evaluate
the latter lazily as you need it. I forked [1] your repo and
tried this out. The Examples module checks in 26s and uses
900M memory on my machine. Another thing I tried is to use a
pair type without eta equality for the models (in my
experience eta equality and call-by-name is a major source of
inefficiency). This saves you another 30% time and space.</div>
<div><br>
</div>
<div>/ Ulf</div>
<div><br>
</div>
<div>[1] <a href="https://github.com/UlfNorell/me-em" target="_blank">https://github.com/UlfNorell/me-em</a><br>
</div>
<div><br>
</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Mon, Feb 1, 2016 at 9:46 AM, Liam
O'Connor <span dir="ltr"><<a href="mailto:liamoc@cse.unsw.edu.au" target="_blank">liamoc@cse.unsw.edu.au</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi all,<br>
<br>
I’m currently using the development version of Agda, and
I’ve been working on using the evaluation in type checking
to embed proof search procedures inside Agda.<br>
<br>
<a href="https://github.com/liamoc/me-em" rel="noreferrer" target="_blank">https://github.com/liamoc/me-em</a><br>
<br>
Now, one of the applications of this technique is a model
checker for a fragment of CTL on the guarded command
language (*).<br>
<br>
Here is an example, where I use the model checker to verify
peterson’s synchronisation algorithm.<br>
<br>
<a href="https://github.com/liamoc/me-em/blob/master/GCL/Examples.agda#L91" rel="noreferrer" target="_blank">https://github.com/liamoc/me-em/blob/master/GCL/Examples.agda#L91</a><br>
<br>
Before I cleaned this code up and put it on GitHub, it was
all in one file. I can affirm that I was able to type check
the code then. Today, after splitting it into multiple
files, and cleaning it up a little bit, I found that Agda
would just get OOM killed before finishing, and it would
take at least 10 minutes before getting OOM-killed, using
all 8GB of my RAM and 4GB of my swap.<br>
<br>
Going back to the original, single-file version, it now also
fails to finish checking and gets OOM-killed, so perhaps the
multiple-files thing isn’t causing the issue.<br>
<br>
(Perhaps I just used a bit of disk space and now it’s
running out of swap).<br>
<br>
Anyway, I’ll try this on a machine with more memory (RAM and
swap) later, but is there any plan to improve performance
(both in time and space) of the type-checker evaluator? I
appreciate that what I’m trying to do is not something which
it was designed to handle, but it _was working_ at some
point.<br>
<br>
BTW, it seems to make no difference whether I use sharing or
not, but when I got it to successfully check yesterday it
was using sharing.<br>
<br>
(*) If you’ve seen the paper I wrote on this, note that the
model checker is substantially different now.<br>
<br>
(*) Also note that originally the definition for
petersons-search read:<br>
<br>
petersons-search<br>
= search $<br>
and′ mutex? (and′ sf? termination?)<br>
(model petersons initialState)<br>
<br>
but I gave it a fixed depth of 25 just to stop it doing any
unnecessary searching.<br>
<br>
Liam<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
<br>
</div>
<br>
<fieldset></fieldset>
<br>
<pre>_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</div></div></div>
</blockquote></div><br></div>