[Hol-info] How to define "infinite sums" of custom datatypes?

[Chun Tian (binghe)]

Hi,

Currently I have the following Datatype "(‘a, ‘b) CCS" which supports binary “sum” operation:

val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| sum CCS CCS
...`;

I also have a recursive function for calculating the “sum” of this datatype stored in a function: f(0) + f(1) + f(2) + 
 + f(n)

val CCS_SIGMA_def = Define `
(CCS_SIGMA (f :num -> ('a, 'b) CCS) 0 = f 0) /\
(CCS_SIGMA f (SUC n) = sum (CCS_SIGMA f n) (f (SUC n))) `;

val _ = overload_on ("SIGMA", ``CCS_SIGMA``);

I don’t like above CCS_SIGMA_def, maybe later I’ll switch to another definition more like the SUM_IMAGE defined in HOL’s pred_setTheory:

val SUM_IMAGE_DEF = new_definition(
"SUM_IMAGE_DEF",
``SUM_IMAGE f s = ITSET (\e acc. f e + acc) s 0``);

which takes a set of numbers as the second parameter, looks more flexible. But it seems that all related theorems have to assume the finiteness of the set parameter.

My questions are:

1. is it possible to define a special SUM_IMAGE for my CCS datatype, and it also supports (countable) infinite sums: ``SUM_IMAGE p (UNIV: num)`` valid and meaningful?

2. if this is impossible, what’s the necessary modification to the original datatype definition?

3. what’s the necessary modification to support sums over limit ordinals (using HOL’s ordinalTheory in examples)? that is, for L a limit ordinal, I need to construct a sum of all ordinals M smaller than L: SUM f(M), for all M < L

Regards,

Chun Tian

[Chun Tian (binghe)]

Yesterday I wanted to change the definition of my datatype to support
summing over a set of values of the same type:

val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| summ (CCS set) (num set)`;

if so, then the original binary "sum" will become the new summ operator
over a two-element set. Later I may even change "num set" into ('a ordinal
-> bool).

But HOL doesn't allow me to do so, strangely saying "can't find definition
for nested type: fun"

Exception raised at Datatype.Hol_datatype:
at ind_types.define_type:
at ind_types.define_type_nested:
Can't find definition for nested type: fun
Exception-
HOL_ERR
{message =
"at ind_types.define_type:\nat ind_types.define_type_nested:\nCan't
find definition for nested type: fun",
origin_function = "Hol_datatype", origin_structure = "Datatype"}
raised

What's the problem here? How can I correctly define such a datatype?

Regards,

Chun

Post by Chun Tian (binghe)
Hi,
Currently I have the following Datatype "(‘a, ‘b) CCS" which supports
val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| sum CCS CCS
...`;
I also have a recursive function for calculating the “sum” of this
datatype stored in a function: f(0) + f(1) + f(2) + 
 + f(n)
val CCS_SIGMA_def = Define `
(CCS_SIGMA (f :num -> ('a, 'b) CCS) 0 = f 0) /\
(CCS_SIGMA f (SUC n) = sum (CCS_SIGMA f n) (f (SUC n))) `;
val _ = overload_on ("SIGMA", ``CCS_SIGMA``);
I don’t like above CCS_SIGMA_def, maybe later I’ll switch to another
val SUM_IMAGE_DEF = new_definition(
"SUM_IMAGE_DEF",
``SUM_IMAGE f s = ITSET (\e acc. f e + acc) s 0``);
which takes a set of numbers as the second parameter, looks more flexible.
But it seems that all related theorems have to assume the finiteness of the
set parameter.
1. is it possible to define a special SUM_IMAGE for my CCS datatype, and
it also supports (countable) infinite sums: ``SUM_IMAGE p (UNIV: num)``
valid and meaningful?
2. if this is impossible, what’s the necessary modification to the
original datatype definition?
3. what’s the necessary modification to support sums over limit ordinals
(using HOL’s ordinalTheory in examples)? that is, for L a limit ordinal, I
need to construct a sum of all ordinals M smaller than L: SUM f(M), for all
M < L
Regards,
Chun Tian

[M***@data61.csiro.au]

You can’t define a type that recurses under the set “constructor” (your summ constructor has (CCS set) as an argument). Ignoring the num set argument, you would then have an injective function (the summ constructor itself) from sets of CCS values into single CCS values. This ultimately falls foul of Cantor’s proof that the power set is strictly larger than the set.

You *could* use finite sets in this context, but HOL4 has no separate type of finite set. While it’s certainly possible to define a type of finite sets, I’m afraid it would then be beyond the Datatype package to define the type you want. There are various ways to do what you want by hand: perhaps the obvious one would be to define a type using (CCS list), and to then quotient the resulting type by the equivalence relation that collapses the lists.

Michael

From: "Chun Tian (binghe)" <***@gmail.com>
Date: Wednesday, 5 July 2017 at 20:37
To: hol-info <hol-***@lists.sourceforge.net>
Subject: Re: [Hol-info] How to define "infinite sums" of custom datatypes?

Yesterday I wanted to change the definition of my datatype to support summing over a set of values of the same type:

val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| summ (CCS set) (num set)`;

if so, then the original binary "sum" will become the new summ operator over a two-element set. Later I may even change "num set" into ('a ordinal -> bool).

But HOL doesn't allow me to do so, strangely saying "can't find definition for nested type: fun"

Exception raised at Datatype.Hol_datatype:
at ind_types.define_type:
at ind_types.define_type_nested:
Can't find definition for nested type: fun
Exception-
HOL_ERR
{message =
"at ind_types.define_type:\nat ind_types.define_type_nested:\nCan't find definition for nested type: fun",
origin_function = "Hol_datatype", origin_structure = "Datatype"} raised

What's the problem here? How can I correctly define such a datatype?

Regards,

Chun


On 3 July 2017 at 13:22, Chun Tian (binghe) <***@gmail.com<mailto:***@gmail.com>> wrote:
Hi,

Currently I have the following Datatype "(‘a, ‘b) CCS" which supports binary “sum” operation:

val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| sum CCS CCS
...`;

I also have a recursive function for calculating the “sum” of this datatype stored in a function: f(0) + f(1) + f(2) + 
 + f(n)

val CCS_SIGMA_def = Define `
(CCS_SIGMA (f :num -> ('a, 'b) CCS) 0 = f 0) /\
(CCS_SIGMA f (SUC n) = sum (CCS_SIGMA f n) (f (SUC n))) `;

val _ = overload_on ("SIGMA", ``CCS_SIGMA``);

I don’t like above CCS_SIGMA_def, maybe later I’ll switch to another definition more like the SUM_IMAGE defined in HOL’s pred_setTheory:

val SUM_IMAGE_DEF = new_definition(
"SUM_IMAGE_DEF",
``SUM_IMAGE f s = ITSET (\e acc. f e + acc) s 0``);

which takes a set of numbers as the second parameter, looks more flexible. But it seems that all related theorems have to assume the finiteness of the set parameter.

My questions are:

1. is it possible to define a special SUM_IMAGE for my CCS datatype, and it also supports (countable) infinite sums: ``SUM_IMAGE p (UNIV: num)`` valid and meaningful?

2. if this is impossible, what’s the necessary modification to the original datatype definition?

3. what’s the necessary modification to support sums over limit ordinals (using HOL’s ordinalTheory in examples)? that is, for L a limit ordinal, I need to construct a sum of all ordinals M smaller than L: SUM f(M), for all M < L

Regards,

Chun Tian

[Chun Tian (binghe)]

Hi Michael,

Thank you very much for the detailed explanation. I’m going to give up with this direction (because modifying the fundamental datatype may break most of my existing theorems). In theory I could break the datatype into two parts (and then make a sum type), but that’s ugly in my view.

On the other side, it will be very interesting to see how other HOL/CCS authors [1] achieved this goal .. well, it should be in HOL88. I haven’t got the related old proof scripts yet, but once I got them, I may raise more question in this thread to you:)

Regards,

Chun Tian

[1] https://link.springer.com/article/10.1007/s001650050046

Post by M***@data61.csiro.au
You can’t define a type that recurses under the set “constructor” (your summ constructor has (CCS set) as an argument). Ignoring the num set argument, you would then have an injective function (the summ constructor itself) from sets of CCS values into single CCS values. This ultimately falls foul of Cantor’s proof that the power set is strictly larger than the set.
You *could* use finite sets in this context, but HOL4 has no separate type of finite set. While it’s certainly possible to define a type of finite sets, I’m afraid it would then be beyond the Datatype package to define the type you want. There are various ways to do what you want by hand: perhaps the obvious one would be to define a type using (CCS list), and to then quotient the resulting type by the equivalence relation that collapses the lists.
Michael
Date: Wednesday, 5 July 2017 at 20:37
Subject: Re: [Hol-info] How to define "infinite sums" of custom datatypes?
val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| summ (CCS set) (num set)`;
if so, then the original binary "sum" will become the new summ operator over a two-element set. Later I may even change "num set" into ('a ordinal -> bool).
But HOL doesn't allow me to do so, strangely saying "can't find definition for nested type: fun"
Can't find definition for nested type: fun
Exception-
HOL_ERR
{message =
"at ind_types.define_type:\nat ind_types.define_type_nested:\nCan't find definition for nested type: fun",
origin_function = "Hol_datatype", origin_structure = "Datatype"} raised
What's the problem here? How can I correctly define such a datatype?
Regards,
Chun
Hi,
val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| sum CCS CCS
...`;
I also have a recursive function for calculating the “sum” of this datatype stored in a function: f(0) + f(1) + f(2) + 
 + f(n)
val CCS_SIGMA_def = Define `
(CCS_SIGMA (f :num -> ('a, 'b) CCS) 0 = f 0) /\
(CCS_SIGMA f (SUC n) = sum (CCS_SIGMA f n) (f (SUC n))) `;
val _ = overload_on ("SIGMA", ``CCS_SIGMA``);
val SUM_IMAGE_DEF = new_definition(
"SUM_IMAGE_DEF",
``SUM_IMAGE f s = ITSET (\e acc. f e + acc) s 0``);
which takes a set of numbers as the second parameter, looks more flexible. But it seems that all related theorems have to assume the finiteness of the set parameter.
1. is it possible to define a special SUM_IMAGE for my CCS datatype, and it also supports (countable) infinite sums: ``SUM_IMAGE p (UNIV: num)`` valid and meaningful?
2. if this is impossible, what’s the necessary modification to the original datatype definition?
3. what’s the necessary modification to support sums over limit ordinals (using HOL’s ordinalTheory in examples)? that is, for L a limit ordinal, I need to construct a sum of all ordinals M smaller than L: SUM f(M), for all M < L
Regards,
Chun Tian
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot_______________________________________________
hol-info mailing list
https://lists.sourceforge.net/lists/listinfo/hol-info