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
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
