expand prior work

[web.git] / 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 4c4c0a0ba1bef46472f030520b31d8e8fb206f9a..47ce741a3d547a4ae984d26bfcdd700e5c2cde5d 100644 (file)
--- a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md
+++ b/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md
@@ -1,12 +1,13 @@
 ---
 title: "Exponential blowup when using unbundled typeclasses to model algebraic hierarchies"
 categories: research coq
 ---
 title: "Exponential blowup when using unbundled typeclasses to model algebraic hierarchies"
 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?
 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.
 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.


@@ -14,8 +15,8 @@ In this post, I will explain the cause of this exponential blowup.
 
 <!-- MORE -->
 
 
 <!-- MORE -->
 

-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
 
 
 ## Unbundled groups