Re: [isabelle] Problems with datatype definition



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:
> 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.