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<https://lists.sourceforge.net/lists/listinfo/hol-info>
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<https://lists.sourceforge.net/lists/listinfo/hol-info>
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<https://lists.sourceforge.net/lists/listinfo/hol-info>
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
*****************************************
------------------------------------------------------------------------------
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
