add CACM article to blog

[web.git] / personal / _posts / 2019-05-15-typeclasses-exponential-blowup.md

diff --git a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
index 4c4c0a0ba1bef46472f030520b31d8e8fb206f9a..bc9a8c99f2534557e2c0e14192da183640a3bd9e 100644 (file)
--- a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
+++ b/personal/_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
+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.
@@ -14,8 +15,8 @@ In this post, I will explain the cause of this exponential blowup.
 
 <!-- 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), a [paper by the same author](https://hal.inria.fr/inria-00368403v2/document) 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 remarks the two papers.
 
 ## Unbundled groups
 
@@ -191,7 +192,7 @@ Class Monoid (A: Type) `{Op A, Unit A} := {
 {% endhighlight %}
 
 This limits the "index depth" to 2, and thus limits term complexity to `O(n^3)`.
-Still not great, but at least it doesn't grow further as we add more sublcasses.
+Still not great, but at least it doesn't grow further as we add more subclasses.
 However, this scheme does not support diamonds in the hierarchy as instances will be duplicated.
 Also, the instance we implicitly added by writing `:>`, namely that `Monoid A -> Semigroup A`, means we'll check all `Monoid` instances any time we just want a `Semigroup`.
 This leads to exponential complexity when performing backtracking typeclass search: a `Semigroup (A*A)` can be obtained either by searching for a `Monoid (A*A)` or via `prod_semigroup`, so in case of backtracking Coq will go through a combinatorial explosion when trying all possible ways to derive `Semigroup (A*A*A*...)`.[^2]