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.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
>>>>
>>>>
>>>> ------------------------------------------------------------------------------
>>>> 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
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
