Christian Sternagel c-sterna at jaist.ac.jp
Fri May 11 10:33:51 CEST 2012

```Hi all,

recently I thought about something which is slightly related to giving
sort constraints for datatypes (but also raised a completely unrelated
question). Let me just give my idea:

Currently I am working on a formalization of Kruskal's Tree Theorem (but
I am still far from finished ;)) which shows that when a set A is
well-quasi-ordered (wqo), then the set of finite trees over A is wqo.

Since the strict part of any wqo is well-founded, they can be employed
in termination analysis.

Moreover, every datatype represents (somehow) a set of finite trees.

So if the type parameters of a datatype are restricted to wqo, we have
that values of this datatype are wqo. (I guess, also here, as Tobias
suggested, you can first use an unconstrained datatype and later on add
the constraints by hand; but I was thinking about something like
"deriving" in Haskell, where we automatically obtain an instance.)

Now to the unrelated question this raised (maybe "the transfer guys"
could comment): What would be the best way to prove something about
"finite trees" (like Kruskal's Tree Theorem) and then obtain this result

Before I heard about the transfer machinery I thought of axiomatizing
what it means to be a finite tree in a locale and do the proof inside
this locale (but this seems a bit cumbersome). Is there any chance that
having a proof for, lets say

datatype 'a tree = Empty | Node 'a "'a tree list"

to obtain the same result "for free" for any other datatype (as long as
this proof only depends on the property "being a finite tree").

If this all would work out, maybe wqo could be incorporated (in addition
to the existing measures) into Isabelle's termination checker (at least
something similar to primrec is conceivable, where we check for
tree-embedding of arguments).

As I said, this is just a recent idea (which may contain several flaws).

cheers

chris

On 05/09/2012 01:43 AM, Tobias Nipkow wrote:
> Am 08/05/2012 14:44, schrieb Makarius:
>> So apart from the observation that the foundational kernel does not require sort
>> constraints (apart from HOL.type of course), were there any reasons against them?
>
> They are not allowed in Haskell anymore, so why do we allow them (and complicate
> the code generation for Haskell in the future)? That was the starting point.
>
> That the kernel does not require sort constraints is not the point. Even if it
> did, you would still not need sort constraints in datatypes because their
> construction does not involve any sorts. You could always (I think) define an
> unconstrained datatype, even if its intended usage is in a constrained setting.
>
> I now see that there are certain extra-logical uses and accept that some people
> just like to explicitly constrain the usage of a datatype.
>
> Now that the machinery works smoothly, I would not suggest to remove it.
>
> Tobias
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

```