Email Gateway (Aug 18 2022 at 13:32): Email Gateway (Aug 18 2022 at 13:32):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
the following datatype definition is not accepted in Isabelle/HOL,
presumably since the parameter of foo has been changed to "'a option".
datatype 'a foo = Bar 'a | Com "'a option foo"
Is there some known workaround for this problem?
Thanks in advance,
René
Email Gateway (Aug 18 2022 at 13:32):From: Brian Huffman <brianh@cs.pdx.edu>
This is an instance of "nested" or "non-regular" recursion, which is
not supported by Isabelle's datatype package. I think you can define
those kinds of datatypes in Coq, but Isabelle has a much less
sophisticated type system that makes working with nested recursive
datatypes very difficult.
The first problem is, what would an induction rule for type 'a foo
look like? Here's a first try:
lemma foo_induct:
assumes "ALL a. P (Bar a)"
assumes "ALL x. P x --> P (Com x)"
shows "ALL x. P x"
But the above rule doesn't work because it is not type-correct.
Because of the nested recursion, the predicate in the inductive
hypothesis needs to have a different type than the one in the
conclusion. In Coq, I think this can work by giving P a polymorphic
type like "forall a, foo a -> Prop". But in Isabelle you can't talk
about polymorphic types in this way.
The other (related) problem is how to define recursive functions over
a nested recursive datatype. Here's a definition you might like to be
able to write:
primrec "size :: 'a foo => nat" where
"size (Foo a) = 0" |
"size (Com x) = Suc (size x)"
The problem is that the recursive call to "size" on the rhs is at a
different type. This means that it is impossible to translate this
definition into a non-recursive one that uses a fixed-point
combinator; at what type would you take the fixed-point? In Coq, the
workaround would be to define a recursive value of type "forall a. foo
a -> nat", with the type parameter made explicit.
So basically, unless Isabelle's type system is extended with rank-2
polymorphism, these kinds of definitions will never be supported. The
only workaround I can think of would be to use something like ZF set
theory to encode everything in a single Isabelle type, allowing you to
essentially bypass Isabelle's type system altogether.
Email Gateway (Aug 18 2022 at 13:33):From: Tobias Nipkow <nipkow@in.tum.de>
It often works to define a supertype. The example below can be encoded as
datatype 'a foo = Bar 'a | Com' "'a foo" nat
where "Com' f n" encodes "Com (Some(...(Some f)...))", with n nested
Somes. Fine-grained constraints are expressed as propositions on this type.
Tobias
Brian Huffman schrieb:
Last updated: May 03 2024 at 04:19 UTC