From 5f79366c662bdd8c66d8ad1e207eba7dfca81d37 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 25 Jul 2018 15:21:40 +0200 Subject: [PATCH] add Coq typeclass index problem draft --- personal/_drafts/typeclasses-exponential-blowup.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 personal/_drafts/typeclasses-exponential-blowup.md diff --git a/personal/_drafts/typeclasses-exponential-blowup.md b/personal/_drafts/typeclasses-exponential-blowup.md new file mode 100644 index 0000000..ec6e6dd --- /dev/null +++ b/personal/_drafts/typeclasses-exponential-blowup.md @@ -0,0 +1,13 @@ +--- +title: "Exponential blowup when using typeclasses with nested indices" +categories: research coq +--- + +When formalizing a proof in an interactive theorem prover like [Coq](https://coq.inria.fr/), one reoccuring issue is handling algebraic hierarchies. +Such hierarchies are everywhere: Some operations are associative, while others also 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. +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](https://arxiv.org/abs/1102.1323). +However, as [has been observed before](https://pastel.archives-ouvertes.fr/pastel-00649586), and as learned the hard way in the Coq formalization of the [original Iris paper](http://iris-project.org/pdfs/2015-popl-iris1-final.pdf), this approach quickly leads to terms that seem to be exponential in size. + -- 2.30.2