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