There can't be such an injection: Datatype can produce finite types.
(Datatype`foo = A | B`;)
On 24 July 2017 at 18:02, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> Hi, Michael
>
> Is there an injection from :num to any type defined by HOL’s Datatype? if
> so, maybe I can still work out something…
>
> Regards,
>
> Chun
>
> > Il giorno 24 lug 2017, alle ore 03:27, michael.norr...@data61.csiro.au
> ha scritto:
> >
> > Even if you can’t prove your result for an arbitrary injective f, does
> it hold for the particular f that you have defined?
> >
> > (There are plenty of injective functions between equi-numerous sets that
> are not onto…)
> >
> > Michael
> >
> > On 23/7/17, 01:07, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
> >
> > Hi Konrad,
> >
> > Thanks again. But unfortunately I found that, my problem won’t get
> resolved even if I have the desired datatype defined… Suppose I already
> have the datatype defined by whatever method, now it contains the infinite
> sum based on ordinals:
> >
> > CCS = Summ (‘c ordinal -> CCS)
> >
> > My CCS datatype already has two type variables ‘a, ‘b. Now it has
> three: ``:(‘a, ‘b, ‘c) CCS``. The recursive function f() defined in my
> proof was having the type ``:‘c ordinal -> (‘a, ‘b) CCS``, now it has the
> type ``:‘c ordinal -> (‘a, ‘b, ‘c) CCS``. But it’s impossible to make
> the cardinality of ``univ(:’c)`` bigger than any set A of type ``:(‘a, ‘b,
> ‘c) CCS set``, so that there must exist an ordinal n such that ``f(n) NOTIN
> A`` (f is ONE_ONE), because the theorem “univ_ord_greater_cardinal" in
> ordinalTheory only works between ``univ(:’c ordinal)`` and any set of type
> (:‘c inf). No matter how I change ‘c, no way to unify ``:’c ordinal`` and
> ``:(‘a, ‘b, ‘c) CCS set``. (But previously it was possible when ‘c is not
> part of type variables in CCS, I can choose ``:(‘a, ‘b) CCS ordinal`` as
> ``:’c ordinal``)
> >
> > |- 𝕌(:α inf) ≺ 𝕌(:α ordinal) [univ_ord_greater_cardinal]
> >
> > On the other side, if I have the (impossible) infinite set
> constructor: CCS = Summ (CCS -> bool), then above problem doesn’t exist at
> all, because type variable of ordinals (‘c) is not part of CCS datatype.
> >
> > In Michael’s paper [1], he said "Unfortunately, the typed logic
> implemented in the various HOL systems (including Isabelle/HOL) is not
> strong enough to define a type for all possible ordinal values”, thus
> essentially this is a limitation in higher order logic. Let me know if
> you see different situations...
> >
> > I’m going to deliver the project as is, with the a minimized infinite
> sum axiom isolated in a very small part of the project concerning only the
> last part of the last theorem. In the future, I consider to use LTS
> (labeled transition systems, or (possibly infinite) directed graphs) to
> finish the proof. Infinite graphs can easily be defined using
> pred_setTheory, no need to use Datatype at all.
> >
> > P. S. I’ll still investigate your sample code and the paper I got
> from Andrei Popescu yesterday, and try to extend my datatype with countably
> infinite sums (num -> CCS) , but this work will be irrelevant with the
> proof of the “last theorem” in my project.
> >
> > Regards,
> >
> > Chun Tian
> >
> > [1] Norrish, M., Huffman, B. (2013). Ordinals in HOL: Transfinite
> Arithmetic up to (and Beyond), 1–14.
> >
> >> Il giorno 22 lug 2017, alle ore 16:25, Konrad Slind <
> konrad.sl...@gmail.com> ha scritto:
> >>
> >> You are welcome. If you are interested, we can try to specialize it to
> your
> >> datatype. The one I was working with was quite complicated, but yours
> >> is much smaller.
> >>
> >> Konrad.
> >>
> >>
> >> On Sat, Jul 22, 2017 at 2:58 AM, Chun Tian (binghe) <
> binghe.l...@gmail.com> wrote:
> >> Hi Knorad,
> >>
> >> Sorry for late response. Thank you very much for providing this sample
> script, although I have to admit that, currently I couldn’t understand such
> complicated HOL code, obviously I still have long way to learn:)
> >>
> >> Regards,
> >>
> >> Chun
> >>
> >>> Il giorno 14 lug 2017, alle ore 16:41, Konrad Slind <
> konrad.sl...@gmail.com> ha scritto:
> >>>
> >>> I can send you a hand-rolled development that I did a few years ago
> >>> (with Michael's help) of Norbert Schirmer's SIMPL. The type
> constructor defined is
> >>>
> >>> ('a,'b,'c) prog
> >>>
> >>> and one of the constructors has type
> >>>
> >>> ('a -> ('a,'b,'c) prog) -> ('a,'b,'c) prog
> >>>
> >>> which seems close to what you want.
> >>>
> >>> Konrad.
> >>>
> >>>
> >>> On Fri, Jul 14, 2017 at 1:47 AM, Chun Tian (binghe) <
> binghe.l...@gmail.com> wrote:
> >>> 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.Norrish@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
> >>>>
> >>>>
> >>>> ------------------------------------------------------------
> ------------------
> >>>> 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
> >>>
> >>>
> >>> <progScript.sml>
> >>
> >>
> >
> >
> >
> > ------------------------------------------------------------
> ------------------
> > 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
>
>
------------------------------------------------------------------------------
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
