[Agda] running out of memory in formalization of category theory

[Anton Setzer]

Could it be that the poor performance of agda is due to the fact that
it always normalises two terms in order to compare whether they are equal
even if they are identical.
(I don't know enough about the implementation of agda)

In most cases I think we are able to check the code by hand, which means
it must be feasible for a machine to check it as well.
My idea is that a good algorithm is as follows:
In order to check whether  two terms
r and s are equal:
- if they start with the same constructor check whether they arguments
are the same.
- if they start with a different constructor they are not equal.
- otherwise:
  . if they start with they same function symbol, check whether the
arguments are the same.
  . if that fails normalise
      (one could either normalise both sides, and check whether for two
reducts r' and s' of
      r and s we have that they start with the same
       function symbol and their arguments are the same; if one doesn't
get a hit
      before one reaches head normal forms, then one compares the head
normal forms
      by following the first two steps above
      This might be too expensive (quadratic in the number of reductions
to head normal form)
      Or one might in this case simply brutally normalise both sides to
head normal form,
     and compare the reducts as in the first two steps.

The first way would take into account that in order to compare two
terms, sometimes one needs
to reduce one a bit, the other a bit, and then they are essentially
syntactically equal.
There doesn't seem to be an optimal strategy however, but it seems to me
that
when we write code by hand, in most cases only few reductions on both
sides are
needed in order to reach identical terms, and full normalisation is a waste.

When looking at code I was by the way always looking at a way to avoid
that Agda
always normalises proofs with no computational content. We sometimes proved
those theorems, then postulated the proofs and referred to the postulated
proofs, just in order to avoid Agda normalising the proofs.


Anton


On 03/06/10 12:14, Nils Anders Danielsson wrote:
> On 2010-06-03 11:43, Conor McBride wrote:
>> Or is it that treatments of type theory tend to live in the
>> inductively defined fragment, which is less eta-expandable?
>
> Christian Sattler had problems when formalising category theory in Agda,
> so he tried replacing all records with single-constructor data types.
> Apparently he managed to finish another two definitions or so before
> performance was a problem again (using Agda 2.2.4 or 2.2.6, I believe).
> In other words, eta for records is not the sole culprit.
>
> -- 
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------