Re: [isabelle] termination of mutually recursive functions



On Wed, Sep 7, 2011 at 6:17 AM, Viorel Preoteasa
<viorel.preoteasa at abo.fi> wrote:
> consts const_a:: "'a"
>
> function
>  A_fun :: "nat => 'b"
>  and B_fun :: "int => 'd"
>  and C_fun :: "bool => 'f"
>  and D_fun :: "bool => 'g"
>  and E_fun :: "nat => 'j"
>  where
>  "A_fun x = const_a" |
>  "B_fun y = const_a" |
>  "C_fun y = const_a" |
>  "D_fun y = const_a" |
>  "E_fun y = const_a"
[...]
> The first collection of functions needs a termination relation of the type
>    (((nat + int) + bool + bool + nat) * ((nat + int) + bool + bool + nat))
> set
> and the second collection  needs a termination relation of the type
> ((nat + int + bool) * (nat + int + bool)) set
>
> The question is why in the first case the first two types (nat and int) are
> grouped
> together  and in the second case they are not? What is the general rule
> for type of the termination relation?

It seems that the "+" type constructors are grouped in such a way as
to make a balanced binary tree. (This is much more evident if you go
to 8 or 16 functions, which gives you a perfectly balanced tree of sum
types.) I suppose there must be an efficiency reason for doing this.

- Brian





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