Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] termination of mutually recursive functions

Email Gateway (Aug 18 2022 at 18:20):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,

I have the following recursive function definitions:

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"

apply pat_completeness
by auto
termination
apply (relation "test_rel")
sorry

function
A_f :: "nat => 'b"
and B_f :: "int => 'd"
and C_f :: "bool => 'f"
where
"A_f x = const_a" |
"B_f y = const_a" |
"C_f y = const_a"

apply pat_completeness
by auto
termination
apply (relation "test_rel")
sorry

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?

Best regards,

Viorel Preoteasa

Email Gateway (Aug 18 2022 at 18:20):

From: Brian Huffman <brianh@cs.pdx.edu>
On Wed, Sep 7, 2011 at 6:17 AM, Viorel Preoteasa
<viorel.preoteasa@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

Last updated: Nov 21 2024 at 12:39 UTC