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 <[email protected]>
> 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) <[email protected]>
> 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
> > <[email protected]> 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) <[email protected]>
> > 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, <[email protected]>
> > > <[email protected]> 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, "[email protected]"
> > > <[email protected]> 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)" <[email protected]> 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
> > >> <[email protected]> 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) <[email protected]>
> > >> 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
> > >> [email protected]
> > >> 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
> > > [email protected]
> > > 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
> > > [email protected]
> > > 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
> > [email protected]
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
> > <progScript.sml>
>
>
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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
