Hi Chun,
I have not followed carefully the technical discussion on this thread, but I
want to give you my two cents here:
1) You must decide which kind of datatype you want: either one that recurses
through bounded sets, as in
datatype proc = ... | Sum (proc bounded_set)
where the bounded_set type constructor (which you would need to define) can put
any fixed cardinality bound (which can also be taken as a parameter, via a type
variable).
or one that recurses through functions, as in
datatype proc = ... | Sum (num -> proc)
where the branching is encoded in num.
Personally, I would suggest the second, since then you could easily adapt
Konrad's type.
2) The constraint to define a function from process terms to the _class_ of all
ordinals is typically a red herring: You almost never need the class of all
ordinals, but can a priori restrict to a large enough host ordinal, e.g.,
depending on the branching allowed for your processes. Then you can safely use
the existing theory of ordinals in HOL4.
Best regards,
Andrei
----------------------------------------------------------------------
Message: 1
Date: Sat, 22 Jul 2017 17:05:34 +0200
From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
To: Konrad Slind <konrad.sl...@gmail.com>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom()
in formal projects
Message-ID: <4765d98a-3b4e-419b-aad4-7db9a55ec...@gmail.com>
Content-Type: text/plain; charset="utf-8"
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
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 ...
> > >
> > >
> > > ------------------------------------------------------------------------------
> > > 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 ...
> >
> >
> > <progScript.sml>
>
>
-------------- 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
------------------------------
Message: 2
Date: Sat, 22 Jul 2017 23:23:08 +0200
From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] How to write a general EQ_CONV ?
Message-ID: <5a7cfbfd-37e0-49be-bf57-97fbe139e...@gmail.com>
Content-Type: text/plain; charset="utf-8"
Hi,
If I have two terms s1 and s2 of type ``:string``, then
string_EQ_CONV ``^s1 = ^s2``
returns a theorem like: |- ``^s1 = ^s2 = T`` or |- ``^s1 = ^s2 = F`` about the
equality the two terms. But if I don?t know the types of s1 and s2, how can I
achieve the same goal by finding a function like string_EQ_CONV and call it?
Regards,
Chun Tian
-------------- 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
------------------------------
Message: 3
Date: Sat, 22 Jul 2017 19:17:50 -0500
From: Konrad Slind <konrad.sl...@gmail.com>
To: "Chun Tian (binghe)" <binghe.l...@gmail.com>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] How to write a general EQ_CONV ?
Message-ID:
<CA+JLB=_GzB2s3eJMb6WLa8DQQFfPZh9jLKi0vL5NH=pboef...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
EVAL_CONV should do it. It is a general-purpose evaluator that works by
deduction. It may even be that string_EQ_CONV is implemented in terms
of it. The documentation about computeLib in
the Description should tell you more.
Konrad.
On Sat, Jul 22, 2017 at 4:23 PM, Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> Hi,
>
> If I have two terms s1 and s2 of type ``:string``, then
>
> string_EQ_CONV ``^s1 = ^s2``
>
> returns a theorem like: |- ``^s1 = ^s2 = T`` or |- ``^s1 = ^s2 = F``
> about the equality the two terms. But if I don?t know the types of s1 and
> s2, how can I achieve the same goal by finding a function like
> string_EQ_CONV and call it?
>
> Regards,
>
> Chun Tian
>
>
> ------------------------------------------------------------
> ------------------
> 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 ...
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
------------------------------
------------------------------------------------------------------------------
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 ...
------------------------------
End of hol-info Digest, Vol 134, Issue 31
*****************************************
________________________________
------------------------------------------------------------------------------
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
