update PNVI-ae-udi paper URL

[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 bc9a8c99f2534557e2c0e14192da183640a3bd9e..4c9f3cf20c58d2a74948560fb8a7d853fded7bca 100644 (file)
--- a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
+++ b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
@@ -16,7 +16,7 @@ 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), 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.
+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 in the two papers.
 
 ## Unbundled groups
 
@@ -172,12 +172,12 @@ That's 4 nested indices, and hence the terms have size `O(n^5)`.
 More generally speaking, the term size is *exponential* in the height of our hierarchy.
 That hurts.
 
-[^1]: Note that the *number* of indices does not matter, like the fact that `Monoid` has both an `Op` and a `Unit` index. That just affects the constant factor. It's the nesting of indices that gets us here.
+[^1]: Note that the *number* of indices does not matter, like the fact that `Monoid` has both an `Op` and a `Unit` index. That just affects the constant factor. It's the nesting of indices that gets us into trouble here.
 
 ## Conclusion
 
 We have seen that the number of nested indices of a typeclass has exponential impact on the size of proof terms that arise when deriving typeclass instances for compound types.
-This effect has grinded the original Iris coq development back in 2015 to a halt: compiling the correctness proof of the logic itself took around 3.5 hours and needed more than the 4GB of RAM than my laptop had back then.
+This effect has grinded the original Iris coq development back in 2015 to a halt: compiling the correctness proof of the logic itself took around 3.5 hours and needed more than the 4GB of RAM that my laptop had back then.
 
 In my view, this basically rules out the unbundled approach for any serious formalization effort.
 But what are the alternatives?