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
