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
