From c4ce390dbcdaa44f921727b90901562e06111394 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 14 May 2019 17:17:16 +0200 Subject: [PATCH] editing --- personal/_drafts/typeclasses-exponential-blowup.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/personal/_drafts/typeclasses-exponential-blowup.md b/personal/_drafts/typeclasses-exponential-blowup.md index 0343bb5..f081e79 100644 --- a/personal/_drafts/typeclasses-exponential-blowup.md +++ b/personal/_drafts/typeclasses-exponential-blowup.md @@ -105,7 +105,7 @@ End prod. Seems reasonable? Unfortunately, we have set ourselves up for some unexpectedly large terms: -the instance of something like `Group (Z*Z*Z*Z*Z*Z)` grows with the fifth power as the number of `Z` increase! +the size of an instance of something like `Group (Z*Z*Z*Z*Z*Z)` grows with the fifth power as the number of `Z` increase! {% highlight coq %} Definition test: Group (Z*Z*Z*Z*Z*Z) := _. @@ -164,7 +164,8 @@ This includes `Zn_op n`, which is quadratic -- so `Zn_semigroup` is cubic! `Zn_semigroup` has an `Op (Zn n)` as index, and again the full nested term describing the operator of both semigroups that we take the product of is getting repeated each time we add just one more `Z`. So, while `Op (Zn n)` has an index that makes it grow quadratically, `Semigroup (Zn n)` *has an index that has an index*, and grows cubically. -To compute the complexity of our terms, we have to figure out *how nested* our indices are: with no indices (such as `Zn n` itself), the term is linear; for each extra nested index the power increases by 1.[^1] + +In general, to compute the complexity of our terms, we have to figure out *how nested* our indices are: with no indices (such as `Zn n` itself), the term is linear; for each extra nested index the power increases by 1.[^1] If we look at `Group`, we see that it has a `Monoid` index which has a `Semigroup` index which has an `Op` index which has a `Type` index. 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. @@ -189,7 +190,8 @@ Class Monoid (A: Type) `{Op A, Unit A} := { }. {% endhighlight %} -This limits the "index depth" to 1, and thus limits term complexity to `O(n^2)`. +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. 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 search times when performing backtracking typeclass search: a `Semigroup (A*A)` can be obtained either by searching for a `Monoid (A*A)` or via `prod_semigroup`, and in case of backtracking Coq will go through a combinatorial explosion when trying all possible ways to derive `Semigroup (A*A*A*...)`.[^2] -- 2.30.2