<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">Yes, very clear, thank you!<br>
Jacques<br>
PS: perhaps such pieces of advice should go on to the wiki?<br>
<br>
On 2016-02-03 11:23 , Ulf Norell wrote:<br>
</div>
<blockquote
cite="mid:CAJjNqYFLwW4Jmy1R5vzjQJzifMciMxjcNBZq=WEM9roN8cZanA@mail.gmail.com"
type="cite">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<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 moz-do-not-send="true"
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 moz-do-not-send="true"
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 moz-do-not-send="true"
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
moz-do-not-send="true"
href="mailto:liamoc@cse.unsw.edu.au"
target="_blank"><a class="moz-txt-link-abbreviated" href="mailto:liamoc@cse.unsw.edu.au">liamoc@cse.unsw.edu.au</a></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 moz-do-not-send="true"
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 moz-do-not-send="true"
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 moz-do-not-send="true"
href="mailto:Agda@lists.chalmers.se"
target="_blank">Agda@lists.chalmers.se</a><br>
<a moz-do-not-send="true"
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 moz-do-not-send="true" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a moz-do-not-send="true" 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>
</blockquote>
<br>
</body>
</html>