From: Ralf Jung Date: Wed, 15 May 2019 08:06:47 +0000 (+0200) Subject: more editing and a new link X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/a448e297bd91c98e949afcef1cd63855be7a2375 more editing and a new link --- diff --git a/personal/_drafts/typeclasses-exponential-blowup.md b/personal/_drafts/typeclasses-exponential-blowup.md index f081e79..4c4c0a0 100644 --- a/personal/_drafts/typeclasses-exponential-blowup.md +++ b/personal/_drafts/typeclasses-exponential-blowup.md @@ -194,7 +194,7 @@ 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] +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] [^2]: In genaral, such combinatorial blowups happen very easily with backtracking, and they are hard to detect in advance. This is one reason why I believe that backtracking-per-default is a bad choice for proof search. @@ -204,6 +204,7 @@ Or maybe the proof assistant could exploit the huge amounts of sharing that are If all subterms are properly shared, I think the overall term size remains linear. Coq deduplicates term representation in memory, but (to my knowledge) does not exploit sharing when traversing the term (for unification or type-checking or any other purpose). Defeating the exponential complexity here would require exploiting the sharing in *every* pass over the term. +An alternative to opportunistically discovering and exploiting sharing might be to [bake it more deeply into metavariable inference](https://eutypes.cs.ru.nl/eutypes_pmwiki/uploads/Meetings/Kovacs_slides.pdf). In Iris, we instead went with an adaptation of [this approach based on canonical structures](https://hal.inria.fr/hal-00816703v1/document). This fully bundled approach avoids indices entirely and thus maintains a linear term size.