Email Gateway (Aug 19 2022 at 09:53): Email Gateway (Aug 19 2022 at 09:53):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
Suppose I want a datatype for finitely-branching trees. I might write something like this:
datatype 'a mytree = Lf 'a | Br "('a mytree) fset"
where fset is the type of finite sets (defined by quotienting lists up to permutations and duplications). This doesn't work, because fset is not a datatype. The usual way to handle this is to use lists instead of fsets, but then deciding the equivalence of trees is more complicated than just checking equality of terms.
Does there exist a way of making datatypes such as mytree? Is anybody working on such a thing? I feel it would be rather useful. I'm imagining an extension to the datatype package that allows the user to provide their own proof that the datatype is admissible -- rather like the way inductive definitions can be annotated with monotonicity lemmas, or the way functions can be annotated with a custom proof of termination.
Best wishes,
John
Email Gateway (Aug 19 2022 at 09:54):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear John,
Suppose I want a datatype for finitely-branching trees. I might write something like this:
datatype 'a mytree = Lf 'a | Br "('a mytree) fset"
where fset is the type of finite sets (defined by quotienting lists up to permutations and duplications). This doesn't work, because fset is not a datatype. The usual way to handle this is to use lists instead of fsets, but then deciding the equivalence of trees is more complicated than just checking equality of terms.
Does there exist a way of making datatypes such as mytree?
In the repository version of Isabelle, and in the forthcoming Isabelle2013 (expected to come out in February), there's a definitional package for defining such types. The "BNF" package (BNF = Bounded Natural Functor) provides a command called "data" that generates all the characteristic lemmas you would expect from "datatype". It works as you would expect:
data 'a mytree = Lf 'a | Br "('a mytree) fset"
The long-term goal (for Isabelle2015 maybe) is to replace the existing "datatype" command.
Is anybody working on such a thing? I feel it would be rather useful. I'm imagining an extension to the datatype package that allows the user to provide their own proof that the datatype is admissible -- rather like the way inductive definitions can be annotated with monotonicity lemmas, or the way functions can be annotated with a custom proof of termination.
Yes, this is exactly how the package work. You can register custom BNFs, as long as they have some properties; some type constructors (functors) are pre-registered, notably "fset"; and the "data" and "codata" commands introduce new inductive and coinductive datatypes (e.g. lazy lists) and registers them as BNFs. Another advantage of the BNF package is that it can be used within local contexts (e.g. locales).
The following papers describe the package in more detail:
http://www21.in.tum.de/~blanchet/lics2012-codat.pdf
http://www21.in.tum.de/~blanchet/codata_wit.pdf
Please let us [*] know if you have further questions. The package is brand new, and we'll happily help you get started with it.
Regards,
Jasmin
[*] Dmitriy Traytel <traytel@in.tum.de>, Andrei Popescu <popescua@in.tum.de>, and me
Last updated: Apr 27 2024 at 01:05 UTC