>> Obviously, I am one of the people who find such efforts trustworthy.
I meant to write worthwhile -- although they are clearly also trustworthy. :-)
Best,
Andrei
________________________________
From: Andrei Popescu
Sent: 24 July 2017 13:07
To: Chun Tian (binghe)
Cc: hol-info@lists.sourceforge.net; Michael Norrish
Subject: Re: On the use of new_axiom() in formal projects
Hi Chun,
>> Thank you very much for letting me know this great paper.
I am happy you find it helpful. Incidentally, this construction is not only
more general, but also much simpler than the traditional one: Roughly, one just
takes the product ofall algebras of the desired functor (in a suitably bounded
fashion), which immediately gets weak initiality (meaning there exists at least
one morphism to any other algebra -- here, of course, the cartesian
projection), and then one takes its smallest subalgebra by a straightforward
inductive construction -- the latter ensures uniqueness of the morphism, hence
initiality.
As a historical note: John Reynolds had performed a similar construction back
in 1984, for a particular functor, in his famous "polymorphism is not set
theoretic," and 10 years later Coquand adapted it to show that HOL cannot be
extended with _impredicative_ polymorphism. My ITP 2014 slides discuss the high
level ideas of the construction, as a bounded adaptation of the
Reynolds-Coquand one:
http://andreipopescu.uk/slides/ITP2014-card-slides.pdf
Note also that Jan Rutten presents the dual of this construction for coalgebras
(yielding what we call coinductive datatypes) in his standard monograph:
https://fldit-www.cs.uni-dortmund.de/~peter/Rutten/UniversalCoalgebra.pdf
>> 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.
This will probably be a lot of work, and require serious HOL4 expertise.
Obviously, I am one of the people who finds such efforts trustworthy. :-)
Besides allowing flexeble and compositional datatypes, they offer the
infrastructure for expressive (co)recursion
(http://andreipopescu.uk/pdf/ICFP2015.pdf
http://andreipopescu.uk/pdf/amico.pdf),<http://andreipopescu.uk/pdf/amico.pdf%29,>
which is also useful for process algebra. But be warned they would be a
serious detour from your specific process algebra research.
Best regards,
Andrei
> 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
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 ...
> 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<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 ...
> 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<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 ...
> 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
> *****************************************
------------------------------------------------------------------------------
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
