Re: [isabelle] Problems with datatype definition



2009/5/20 René Thiemann <rene.thiemann at 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?

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.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.