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

[Bas Spitters]

One development for such meta-theory is available for CoqMT.
https://hal.archives-ouvertes.fr/hal-01664457
I wonder about the relation with the rewriting technology in Jesper's blog
post.

Bas

On Mon, Oct 21, 2019 at 9:36 PM Jon Sterling <jon at jonmsterling.com> wrote:

> 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
> >
> _______________________________________________
> 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/217d3e92/attachment.html>