Hi Andrei, Thank you very much for letting me know this great paper. If I managed to understand your method, instead of creating my datatype manually, I have more willing to try to implement it in HOL4 (as extension to the Datatype command), with the existing implementation in Isabelle/HOL referenced.
P. S. I found your other publications also very useful to me, especially those related to Concurrency Theory. Regards, Chun Tian > Il giorno 21 lug 2017, alle ore 23:58, Andrei Popescu <a.pope...@mdx.ac.uk> > ha scritto: > > Hi Chun, > > That paper by Melham is important pioneering work, but will be of little help > to you since it only shows how to construct non-permutative datatypes, like > lists and ordered trees. The following paper > > http://andreipopescu.uk/pdf/LICS2012.pdf > > shows how to construct in HOL (inductive or coinductive) types of a more > general kind, which include, e.g., those that recurse through > bounded-cardinality powersets -- like the one you need. > > Best wishes, > > Andrei > > > Message: 1 > Date: Fri, 14 Jul 2017 08:47:38 +0200 > From: "Chun Tian (binghe)" <binghe.l...@gmail.com> > To: Michael Norrish <michael.norr...@data61.csiro.au> > Cc: hol-info@lists.sourceforge.net > Subject: Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom() > in formal projects > Message-ID: <730f82c8-3234-454a-bf19-5354a927a...@gmail.com> > Content-Type: text/plain; charset="utf-8" > > Hi Michael, > > Great, thanks! Then I guess the only remain issue in my project is to define > this datatype by hand. I?ll make a deeper reading in Tom Melham?s paper [1] > and see how such job can be done. If there're other relevant materials, > please let me know (at least the title). > > Regards, > > Chun Tian > > [1] Melham, Tom. Automating recursive type definitions in higher order logic. > 1989. > > > Il giorno 14 lug 2017, alle ore 08:24, <michael.norr...@data61.csiro.au> > > <michael.norr...@data61.csiro.au> ha scritto: > > > > Note further that a type where you have > > > > Datatype?CCS = C1 ? | C2 .. | SUM (num -> CCS)?; > > > > does not fall foul of cardinality problems. (You can recurse to the right > > of a function arrow as above, but not to the left, as would happen in SUM > > (CCS -> bool).) > > > > So, when I wrote ?you just can?t have infinite sums?, I was over-stating. > > If you see num -> CCS as enough of an infinite sum, then you?re OK. (And > > you could certainly also have ?SUM : ('a ordinal -> CCS) -> CCS?.) > > > > Unfortunately, HOL4?s Datatype principle doesn?t allow the definition above > > as I?ve written it, but such types can be defined by hand with sufficient > > patience. > > > > Michael > > > > On 14/7/17, 14:47, "michael.norr...@data61.csiro.au" > > <michael.norr...@data61.csiro.au> wrote: > > > > You just can?t have infinite sums inside the existing type for the > > cardinality reasons. But there?s no reason why you couldn?t have a type > > that featured infinite sums over a base type that didn?t itself include > > infinite sums. > > > > Something like > > > > Datatype`CCS = ? existing def ? (* with or without finite/binary sums > > *)` > > > > Datatype`bigCCS = SUM (num -> CCS)` > > > > Depending on the degree of branching you want, you might replace the num > > above with something else. Indeed, you could replace it with ?a ordinal. > > > > Michael > > > > On 14/7/17, 04:15, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote: > > > > Hi Ramana, > > > > Thanks for explanation and hints. Now it?s clear to me that, I > > *must* remove the new_axiom() from the project, even if this means I have > > to bring some ?ugly? solutions. > > > > Now I see ord_RECURSION is a universal tool for defining recursive > > functions on ordinals, for this part I have no doubts any more. But my > > datatype is discrete, no order, no accumulation, currently I can?t see a > > function (lf :?a ordinal -> ?b set -> ?b) which can be supplied to > > ord_RECURSION .. > > > > Currently I?m trying to something else in the datatype, and I have > > to replay all theorems in the project to see the side effects. Meanwhile I > > would like to hear from other HOL users for possible solutions on the > > infinite sum problem which looks quite a common need .. > > > > Regards, > > > > Chun > > > >> Il giorno 13 lug 2017, alle ore 14:35, Ramana Kumar > >> <ramana.ku...@cl.cam.ac.uk> ha scritto: > >> > >> Some very quick answers. Others will probably go into more detail. > >> > >> 1. If you use new_axiom, it becomes your responsibility to ensure that > >> your axiom is consistent. If it is not consistent, the principle of > >> explosion makes any subsequent formalisation vacuous. (If you don't use > >> new_axiom, it can be shown that any formalisation is consistent as long as > >> set theory is consistent.) > >> > >> 2. Yes. But you should probably detail why you claim that the axiom is > >> consistent and that you wrote it down correctly. It also makes it less > >> appealing for others to build on your work subsequently. > >> > >> 3. Yes. Prove the existence of functions defined on ordinals, specialise > >> that existence theorem with your desired definition, then use > >> new_specification. Maybe the required theorem exists already? Does > >> ord_RECURSION do it? See how ordADD is defined. (I haven't looked at this > >> in detail.) > >> > >> On 13 July 2017 at 21:10, Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > >> Hi, > >> > >> (Thank you for your patience for reading this long mail with the question > >> at the end) > >> > >> Recently I kept working on the formal proof of an important (and elegant) > >> theorem in CCS, in which the proof requires the construction of a > >> recursive function defined on ordinals (returning infinite sums of CCS > >> processes). Here is the informal definition: > >> > >> 1. Klop a 0o := nil > >> 2. Klop a (ordSUC n) := Klop a n + (prefix a (Klop a n)) > >> 3. islimit n ==> > >> Klop a n := SUM (Klop a m) for all ordinals m < n > >> > >> (here the "+" operator is overloaded, it's the "sum" of an custom datatype > >> (CCS) defined by HOL's Define command. "prefix" is another operator, both > >> are 2-ary) > >> > >> I think it's a well-defined function, because the ordinal arguments > >> strictly becomes smaller in each recursive call. But I don't know how to > >> formall prove it, and of course HOL's Define package doesn't support > >> ordinals at all. > >> > >> On the other side, my datatype doesn't support infinite sums at all, and > >> it seems no hope for me to successfully defined it, after Michael has > >> replied my easier email and explained the cardinality issues for such > >> nested types. > >> > >> So I got two issues here: 1) no way to define infinite sums, 2) no way to > >> define resursive functions on ordinals. But I found a "solution" to > >> bypass both issues: instead of trying to express infinite sums, I turn to > >> focus on the behavior of the infinite sums and define the behavior > >> directly as an axiom. In CCS, if a process p transits to p', then p + q + > >> ... (infinite other process) still transit to p'. Thus I wrote the > >> following "cases" theorem (which looks quite like the 3rd return values by > >> Hol_reln) talking about a new constant "Klop" > >> > >> val _ = new_constant ("Klop", ``:'b Label -> 'c ordinal -> ('a, 'b) CCS``); > >> > >> |- (!a. Klop a 0o = nil) ? > >> (!a n u E. > >> Klop a n? --u-> E <==> > >> u = label a ? E = Klop a n ? Klop a n --u-> E) ? > >> !a n u E. > >> islimit n ==> (Klop a n --u-> E <==> !m. m < n ? Klop a m --u-> E) > >> > >> I used new_axiom() to make above definion accepted by HOL. I don't know > >> how to "prove" it, don't even know what to prove, because it's just a > >> definition on a new logical constant (acts as a black-box function), while > >> it's behaviour is exactly the same as if I have infinite sums in my > >> datatype and HOL has the ability to define recursive function on ordinals. > >> > >> From now on, I need no other axioms at all. Then I can prove the following > >> "rules" theorems which looks like the first return value of Hol_reln: > >> > >> |- (!a n. Klop a n? --label a-> Klop a n) ? > >> !a n m u E. islimit n ? m < n ? Klop a m --u-> E ==> Klop a n --u-> E > >> > >> Then I can use transfinite inductino to prove a lot of other properties of > >> the function ``Klop a``. And with a lot of work, finally I have proved the > >> following elegant theorem in Concurrent Theory: > >> > >> Thm. (Coarsest congruence contained in weak equivalence) > >> |- !g h. g ?? h <==> !r. g + r ? h + r > >> > >> ("??" is observation congruence, or rooted weak bisimulation equivalence. > >> "?" is weak bisimulation equivalence) > >> > >> Every lemma or proof step corresponds to the original paper [1] with > >> improvements or simplification. And if you let me to write down the > >> informal proof (from the formal proof) using strict Math notations and > >> theorems from related theories, I have full confidence to convince people > >> that it's a correct proof. > >> > >> But I do have used new_axiom() in my proof script. My questions: > >> > >> 1. What's the risk for a new_axiom() used on a new constant to break the > >> consistency of entire HOL Logic? > >> 2. With new_axiom() used, can I still claim that, I have correctly > >> formalized the proof of that theorem? > >> 3. (optionall) is there any hope to prevent using new_axiom() in my case? > >> > >> Best regards, > >> > >> Chun Tian > >> > >> [1] van Glabbeek, Rob J. "A characterisation of weak bisimulation > >> congruence." Lecture notes in computer science 3838 (2005): 26. > >> > >> -- > >> 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 > >> > >> > > > > > > > > > > ------------------------------------------------------------------------------ > > 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 > hol-info Info Page - SourceForge > lists.sourceforge.net > hol-info is for general discussions about the HOL system, and for relevant > announcements (of system updates, and also of conferences that the moderators > feel will be ... > > > > > > > > ------------------------------------------------------------------------------ > > 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 > hol-info Info Page - SourceForge > lists.sourceforge.net > hol-info is for general discussions about the HOL system, and for relevant > announcements (of system updates, and also of conferences that the moderators > feel will be ... > > > > -------------- next part -------------- > A non-text attachment was scrubbed... > Name: signature.asc > Type: application/pgp-signature > Size: 203 bytes > Desc: 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 > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > hol-info Info Page - SourceForge > lists.sourceforge.net > hol-info is for general discussions about the HOL system, and for relevant > announcements (of system updates, and also of conferences that the moderators > feel will be ... > > > > > ------------------------------ > > End of hol-info Digest, Vol 134, Issue 24 > *****************************************
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
