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"
> A_fun :: "nat => 'b"
> and B_fun :: "int => 'd"
> and C_fun :: "bool => 'f"
> and D_fun :: "bool => 'g"
> and E_fun :: "nat => 'j"
> "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))
> 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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and