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 > Il giorno 10 lug 2017, alle ore 02:40, michael.norr...@data61.csiro.au ha > scritto: > > 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> 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
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
