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

[Jon Sterling]

Hi Jesper,

I'm very pleased to hear that the confluence checker is coming along! Once it is in place, what kind of syntactic guarantees (relative to "pure Agda") can we expect to be available in the presence of custom rewrite rules? 

The main one I'm asking about is transitivity: if judgmental equality is transitive in plain Agda, then does one expect it to be transitive in Agda mod T, for T a set of rewrite rules that would accepted by the completed checker? If so, the rewriting facility sounds totally amazing and really useful.

Maybe in the future we can just use Agda to prototype most new extensions to type theory, rather than writing our own implementations right away. 


Best,
Jon



On Mon, Oct 21, 2019, at 12:14 PM, Jesper Cockx wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>