[Agda] How does unification work?

[Guillaume Brunerie]

I still haven’t managed to get a minimal test case for this, but I did
an agda-bisect between 2.5.3 and 2.5.4.1 and it suggests that the
first bad commit is a02895d (The Agda Abstract Machine - Complete
rewrite of fast reduce to use a proper call-by-need abstract machine.
Runs in the ST monad with STRefs for heap pointers.)

Best,
Guillaume

Den ons 28 aug. 2019 kl 14:44 skrev Ulf Norell <ulf.norell at gmail.com>:
>
> A difference is that when normalizing you stay in the abstract machine until you reach a normal form, but when
> checking equality, each whnf step runs in a separate instance of the machine. This means that you lose sharing
> between steps, which could explain the behaviour you're seeing.
>
> / Ulf
>
> On Wed, Aug 28, 2019 at 2:30 PM Guillaume Brunerie <guillaume.brunerie at gmail.com> wrote:
>>
>> Hi all,
>>
>> I have a (rather big) example of two terms u and v which each take about 20 seconds and not much memory to fully normalize (the results is about 30 000 lines long), but checking whether reflexivity has type u == v exhaust all of the memory of my computer (25G). With Agda 2.5.3, the same example does not take much memory at all, but takes several minutes, much longer than simply computing both normal forms. The high memory usage is already present in Agda 2.5.4.1.
>>
>> I’m trying to shrink the example but I’m wondering if it’s expected that checking whether two terms are definitionally equal can take much longer and/or much more memory than normalizing them and comparing the normal forms.
>>
>> My naive understanding of the algorithm for checking definitional equality is as follows (at least for types without eta):
>> - check whether the two terms are syntactically equal (unless using the option --no-syntactic-equality), return True if they are
>> - reduce both terms to weak-head normal form, if the heads differ then return False, otherwise recursively check definitional equality of the arguments pairwise.
>>
>> Is this more or less correct? If we do not have eta, then it seems to me that in the worst case scenario, checking definitional equality is more or less as expensive as normalizing both sides, but it shouldn’t be considerably more expensive.
>>
>> Is eta the problem, then? Or am I missing something else?
>>
>> Best,
>> Guillaume
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda