X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/2a0598d090829c0f9db3a7763464d9800d6511dd..e1e887492ae24f7b0448913b92a401b16b117b87:/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md diff --git a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md b/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md index e59917b..47ce741 100644 --- a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md +++ b/ralf/_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. @@ -15,8 +15,8 @@ In this post, I will explain the cause of this exponential blowup. -I should note that this observation is not new, it already occurs in [François Garillot's PhD thesis](https://pastel.archives-ouvertes.fr/pastel-00649586). -The goal of this post is to provide a more self-contained presentation, not requiring all the context set up in that thesis. +I should note that this observation is not new, it already occurs in [François Garillot's PhD thesis](https://pastel.archives-ouvertes.fr/pastel-00649586) and even the authors of the "unbundled" paper already note having performance problems when scaling up. +The goal of this post is to provide a more self-contained presentation, not requiring all the context set up in that thesis and going into more details than the brief remark in the original paper. ## Unbundled groups