[Agda] New blog post: Hack your type theory with rewrite rules

[Jesper Cockx]

Hi Apostolis,

Excellent question! Unfortunately, the answer is not an unqualified 'yes'.
It is true that using such rewrite rules always preserves soundness of the
theory, since rewrite rules are in a sense a limited form of equality
reflection, and equality reflection is known to be consistent.

However, other more syntactic properties such as confluence, termination,
and subject reduction (aka type preservation) can still be broken. In our
2014 paper, I give one such example: the rewrite rules `(suc x) * y == (x *
y) + y` and `x * (suc y) == x + (x * y)` are not confluent unless you also
have associativity of + as a rewrite rule. It's not very straightforward,
but by tricking Agda's constraint solver to solve equations in a particular
order, you can exploit a non-confluence like this to break subject
reduction. This manifests as a type error complaining two things should be
equal even though they are according to the rules.

I have actually been working on implementing a confluence checker for
rewrite rules (which I'm planning to talk about in an upcoming post). If
you want, you can try it out by installing the current master branch of
Agda and enabling the --confluence-check flag.

Cheers,
Jesper

On Mon, Oct 21, 2019 at 4:21 PM Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> If you have proved the equality as in your 2nd example, is there any
> reason not to use REWRITE?
> My impression is that I should use REWRITE everywhere where I have proven
> a propositional equality so as to make it definitional.
>
> Nice blog post, and a good reference to a book on type theory. I was
> looking into a good introductory book that would help me understand agda a
> bit better.
>
> On Mon, Oct 21, 2019 at 4:22 PM Jesper Cockx <Jesper at sikanda.be> wrote:
>
>> Hi Agda folks,
>>
>> I have another blog post for you on extending Agda with rewrite rules,
>> with no less than six examples of how they can be used. You can read it at
>> https://jesper.sikanda.be/posts/hack-your-type-theory.html. Any comments
>> are welcome here on the mailing list as usual.
>>
>> Cheers,
>> Jesper
>> _______________________________________________
>> 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/20191021/71cdc8b6/attachment.html>