[Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes

[Andreas Abel]

On 23.04.12 5:43 PM, James Deikun wrote:
> On Mon, 2012-04-23 at 16:14 +0200, Nils Anders Danielsson wrote:
>> On 2012-04-18 22:48, James Deikun wrote:
>>> Needless recursion when building or verifying equalities is prevented
>>> using the following function, which throws away its argument while
>>> requiring a suitable proof of said argument's existence:
>>>
>>>>   hideProof : {a : Level} {A : Set a} {x y : A} ->  x ≡ y ->  x ≡ y
>>>>   hideProof eq = trustMe
>>
>> Nice trick. I wonder if it's sound. If it is sound, then we should
>> perhaps try to find a less hacky way to do this.

This is a realization of proof-irrelevance for propositional equality. 
Basically, if you change subst (or J) that you do not check the proof 
for being refl before reduction, but you check the definitional equality 
of the compared things, then you do not need to store the equality proof.

In Agda, with pattern matching instead of J, this is of course more 
difficult to implement systematically...  I made an effort in MiniAgda 
by eta-expanding all equality proofs.

> Indeed.  I can't say for sure that it's sound, but at least the one
> major issue I thought of (that termination checking might see that the
> recursive calls are thrown away and admit proofs that wouldn't terminate
> with 'hideProof = id') doesn't seem to be a problem from my testing.
> (I'm not sure that it won't show up in sufficiently complex mutual
> recursions, though.)
>
> And this does seem to be more generally applicable than many of the
> other speedup techniques.
>
>>> The pairing heap (Heap.agda) and sieve (Sieve.agda) implementations use
>>> pattern-matching as a sequentialization measure to control duplication
>>> of unevaluated thunks, which can cause an exponential slowdown.
>>
>> We should really switch to a more efficient evaluation strategy.
>
> I had heard that something like this might come out of the last AIM; is
> there any work in progress?
>
> It does seem like a tough nut to crack, with reduce and reduceB
> currently in TCM; eliminating that effect to allow the reuse of
> Haskell's lazy evaluation would be a serious bit of rearchitecture in
> itself, and both graph- and let-based explicit call-by-need evaluators
> would need a major reworking of the term representation ...

Running reduce in a reader monad (to access the signature) should be 
possible, and maybe the restructuring is feasible  (as compared of 
switching to explicit sharing in Internal syntax, which would basically 
amount to a rewrite of the whole engine).

Do you think it would solve some performance issues?

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/