[Agda] New blog post: Hack your type theory with rewrite rules
Frédéric Blanqui
frederic.blanqui at inria.fr
Tue Oct 22 09:30:17 CEST 2019
Dear all,
CoqMT is not really Coq modulo rewriting but rather Coq modulo decision
procedures like linear arithmetic, etc. Unfortunately, it is not
developed anymore at the moment I think.
For a proof assistant with builtin rewriting, I invite you to have a
look at Dedukti, or rather its new interactive version, Lambdapi (future
Dedukti v3), https://github.com/Deducteam/lambdapi. See its
documentation on
https://github.com/Deducteam/lambdapi/blob/master/doc/DOCUMENTATION.md .
Lambdapi is still under development and misses a basic library but this
will be fixed in the next months. So stay tuned! You can however have a
look at some of the test files to see how it looks like. For instance,
https://github.com/Deducteam/lambdapi/blob/master/tests/OK/rewrite.lp ,
https://github.com/Deducteam/lambdapi/blob/master/tests/OK/natproofs.lp
or https://github.com/Deducteam/lambdapi/blob/master/tests/OK/245.lp .
Some new VSCode interface has been developed and should be released in
the next months (there are also simple interfaces with vim and emacs).
Its current set of tactics is very basic but should be improved in the
next months. Two important tactics are much more advanced though: a
rewriting tactic following the SSReflect syntax and semantics, and a
tactic for calling external automated theorem/SAT/SMT provers through
the Why3 library (available in the next days).
Dedukti implements the lambda-Pi-calculus modulo user-defined rewriting.
See below for some references. In particular, adding rewriting to
dependent types allows to easily encode many other systems: HOL, Matita,
Coq, Isabelle or Agda (work in progress).
Dedukti includes a builtin subject-reduction checker (a new more
powerful algorithm based on Knuth-Bendix completion will be released in
the next months). For confluence, you can call external confluence
checkers like CSI^ho or other confluence provers participating to the
competition on confluence (http://project-coco.uibk.ac.at/). Idem for
termination using an extension to dependent types of the format for
termination problems of the termination competition
(http://termination-portal.org/wiki/Termination_Competition). See
https://github.com/Deducteam/lambdapi/blob/master/doc/sections/options.md
for more details. In particular, Guillaume Genestier developed a
termination checker prototype for Dedukti that could be extended to Agda.
Some references (we could add more):
- Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo
Theory, A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C.
Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard,
http://www.lsv.fr/~dowek/Publi/expressing.pdf , submitted.
- Dependency Pairs Termination in Dependent Type Theory Modulo
Rewriting, http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.9 , 2019.
- Definitions by rewriting in the Calculus of Constructions,
https://doi.org/10.1017/S0960129504004426 , 2005.
- Dependent type theory with first-order parameterized data types and
well-founded recursion, D. Wahlstedt,
http://www.cse.chalmers.se/alumni/davidw/wdt_phd_printed_version.pdf , 2007.
- Type checking in the Lambda-Pi-calculus modulo: theory and practice,
PhD thesis, R. Saillard,
https://pastel.archives-ouvertes.fr/tel-01299180 , 2015.
- Type theory and rewriting, PhD thesis,
http://hal.inria.fr/inria-00105525 , 2001.
- Modularity of strong normalization in the algebraic-lambda-cube, F.
Barbanera and M. Fernandez and H. Geuvers,
http://journals.cambridge.org/article_S095679689700289X , 1997.
Le 21/10/2019 à 22:04, Bas Spitters a écrit :
> 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
> <mailto: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
> <mailto: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 <mailto: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 <mailto:Agda at lists.chalmers.se>
> > >> https://lists.chalmers.se/mailman/listinfo/agda
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto: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/20191022/ba04b5b3/attachment.html>
More information about the Agda
mailing list