Re: [isabelle] fixed-point types?

Dear Eddy,

Of course you can construct your fixpoint type manually, but this will be a lot of work. Or, you just continue to axiomatize the structure of the resumption monad transformer, too, but axioms are better avoided.

The new datatype package might, however, offer a solution, because it supports fixpoint types for natural functors that are *bounded*. Boundedness means that the cardinality of the elements of the type is bounded by some cardinal that does not depend on the type variable over which the fixpoint is built. To that end, you have to register your monad type as a BNF.

In Isabelle2013-2, you have to import the BNF package via "~~/src/HOL/BNF/BNF", in the coming Isabelle2014 release, the datatype_new command will already be part of Main. The tutorial on datatypes tells you what is needed and provides further references.

By the way, I would also suggest to think about taking the greatest fixpoint (codatatype) rather than the least (datatype) for ResumpT. Then you can also reason about possibly infinite computations.


On 04/08/14 18:49, Eddy Westbrook wrote:

I was wondering if there is any way to directly construct a fixed-point type in Isabelle, without (at least, without directly) using datatypes. That is, I have a type constructor F x, and I would like to construct a fixed-point type tau = F tau. Any ideas on how to go about this? Of course, this should only be possible if F is a functor, since otherwise it doesn’t have a fixed-point.

In more detail, I am trying to axiomatize the resumption monad transformer, as follows. I start by declaring the underlying monad type, as follows:

typedecl ‘a Monad

By positing the monad laws as axioms, I am assured that Monad is a functor. Then I would like to define the resumption transformer like this:

datatype 'a ResumpT
    = Done 'a
    | Pause "('a ResumpT) Monad"

Of course, this is not a valid datatype, because Isabelle does not know that Monad is positive. I was thinking, however, that I could turn ResumpT into a type-level function, as follows:

datatype (‘a, ’t) ResumpT
    = Done 'a
    | Pause “’t Monad"

Then, if I could build a fixed-point type over the ’t type argument, I would by able to define ResumpT, at least indirectly.

Any help on this front would be appreciated.


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