From: Ralf Jung Date: Wed, 15 May 2019 19:05:05 +0000 (+0200) Subject: typos X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/11eff2ea5dd6029346c369aaec53dbb68445c9f8 typos --- diff --git a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md index e59917b..2eda613 100644 --- a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md +++ b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md @@ -4,10 +4,10 @@ categories: research coq forum: https://coq.discourse.group/t/blog-post-exponential-blowup-when-using-unbundled-typeclasses-to-model-algebraic-hierarchies/289 --- -When formalizing a proof in an interactive theorem prover like [Coq](https://coq.inria.fr/), one reoccuring issue is the handling of algebraic hierarchies. +When formalizing a proof in an interactive theorem prover like [Coq](https://coq.inria.fr/), one reoccurring issue is the handling of algebraic hierarchies. Such hierarchies are everywhere: some operations are associative, while others commute; some types have an equivalence relation, while others also have a (pre-)order or maybe even a well-ordering; and so on. So the question arises: What is the best way to actually encode these hierarchies in Coq? -Coq offers two mechanism that are suited to solve this task: typeclasses and canonical structures. +Coq offers two mechanisms that are suited to solve this task: typeclasses and canonical structures. Both can be instrumented in different ways to obtain a (more or less) convenient-to-use algebraic hierarchy. A common approach using typeclasses is the ["unbundled" approach by Bas Spitters and Eelis van der Weegen](http://www.eelis.net/research/math-classes/mscs.pdf). However as we learned the hard way in the Coq formalization of the [original Iris paper](https://iris-project.org/pdfs/2015-popl-iris1-final.pdf), this approach quickly leads to terms that seem to be exponential in size.