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)" <binghe.l...@gmail.com>
Date: Wednesday, 5 July 2017 at 20:37
To: hol-info <hol-info@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)
<binghe.l...@gmail.com<mailto:binghe.l...@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)
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
