[Agda] How does unification work?

[Ulf Norell]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190828/f7d1fb96/attachment.html>