Hi, This mail is long, it’s very important for me, and it's a continuation of my previous two big questions in 3 months ago, titled "On the use of new_axiom() in formal projects” and "How to define "infinite sums" of custom datatypes?”.
The good thing is, I have resolved the previous difficulties in expressing
infinite sums in process algebra, and have prevented using an axiom. I didn’t
use the paper of Dr. Andrei Popescu, simply because it’s too hard for my
current skills. I also didn’t use the idea from Michael Norrish, by
introducing another larger Datatype:
Datatype`CCS = … existing def … (* with or without finite/binary sums *)`
Datatype`bigCCS = SUM (num -> CCS)`
Because the "infinite sum” in my problem happens at infinite levels, but this
“bigCCS” cannot further include itself.
My solution is to embed LTS (labeled transition system) into CCS datatype:
val _ = type_abbrev ("LTS", ``:('a ordinal, 'b Action) graph``);
(* Define the type of (pure) CCS agent expressions. *)
val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| sum CCS CCS
| par CCS CCS
| restr (('b Label) set) CCS
| relab CCS ('b Relabeling)
| rec 'a CCS
| lts ('a ordinal) (('a, 'b) LTS)`;
here the type “:(‘a, ‘b) graph” is my creation in response of providing a
general graph theory formalization [1], ‘a is the type of vertex, ‘b is the
type of edge label. Currently it’s far from complete, with lots of possibly
wrong definitions but no much supporting theorems. But it worked for my current
needs. For my problem described in this mail, the structure of this graph
doesn’t matter, you can safely think it’s a set (defined by pred_setTheory)
with 'a ordinals as vertices.
The “lts” constructor in above CCS datatype is my creation without knowing any
similar work. the term ``lts r G`` means a rooted LTS, where “r” is a vertex
in the graph G, as the root node. For this new constructor, I have defined a
single transition rule:
val (TRANS_rules, TRANS_ind, TRANS_cases) = Hol_reln `
(!E u. TRANS (prefix u E) u E) /\ (*
PREFIX *)
(!E u E1 E'. TRANS E u E1 ==> TRANS (sum E E') u E1) /\ (* SUM1
*)
(!E u E1 E'. TRANS E u E1 ==> TRANS (sum E' E) u E1) /\ (* SUM2
*)
...
(!E u E' G. (E, u, E') IN (TS G)
==> TRANS (lts E G) u (lts E' G)) `; (* LTS
*)
That is, TRANS (lts E G) u (lts E' G) is true if and only if there is a
labeled edge E—u—>E’ in the graph G. The most surprising fact is, after
introducing such a new constructor “lts” and its transition rule, all my
previous proved theorems are still working. The only changes I have to do, is
very few theorems in which the TRANS_cases theorem is used, but the additional
sub-goal is trivial.
So, all my definitions like Bisimulation, Weak bisimulation, etc. now also work
in pure transition systems (as rooted directed graphs). I feel so happy for
having LTS included in my formalization of CCS and prevented for re-defining
almost everything again. And the mixing of LTS and CCS is now also
meaningful: two graphs can be connected directly by algebraic operators, and
the combined transition characteristics still make perfect sense.
Now I have the following so-called Klop process, which is actually an set of
“Arbitrary many non-bisimiar process”:
Klop l n =
ABS_graph ({m | m ≤ n},{{p} --label l--> {q} | p ≤ n ∧ q < p}):
without any new axiom, now I can prove the following properties:
[KLOP_PROP0] Theorem (all these processes are stable, i.e. has no
tau-transition)
|- ∀a n. STABLE (KLOP a n)
[KLOP_PROP1] Theorem (any transition from such a process, leads to a
smaller process by the same generator)
|- ∀a n E. KLOP a n --label a--> E ⇔ ∃m. m < n ∧ (E = KLOP a m)
[KLOP_PROP1'] Theorem (the same as above, but for weak transition, which is
actually strong transition because there’s no tau at all)
|- ∀a n E. KLOP a n ==label a=-> E ⇔ ∃m. m < n ∧ (E = KLOP a m)
[KLOP_PROP2] Theorem (two different sized such processes are not strong
bisimilar)
|- ∀a n m. m < n ⇒ ¬(KLOP a m ∼ KLOP a n)
[KLOP_PROP2'] Theorem (two different sized such processes are also not weak
bisimilar)
|- ∀a n m. m < n ⇒ ¬(KLOP a m ≈ KLOP a n)
Again, I feel so happy for successfully proved and defined above function and
its properties. Now it remains to use it for proving the ultimate “simple”
theorem above process algebra:
``!p q. OBS_CONGR p q = !r. WEAK_EQUIV (sum p r) (sum q r)`` (observation
congruence is the coarsest congruence contained in weak bisimulation)
Now it’s touching my question and two difficulties:
The proof of above theorem has been reduced to: finding a special process K,
which is not (weak) bisimilar with any node in the transition graph of two
given processes p and q. The informal proof [2] is like this:
“Let c be the smallest infinite cardinal, such that NODES(p) and
NODES(q) has less than c nodes. So there are less than c processes in NODES(p)
and NODES(q). Then there’s a tau-free process K with NODES(K) < c, such that
k is not bisimiar with any nodes in NODES(p) and NODES(q), BECAUSE: for
each infinite cardinal c there are c ordinals smaller than c.”
If I've learnt correctly, in standard set theory, all cardinals are ordinals,
but the reverse is not true, because not every ordinals “has the same number
(as itself) of smaller ordinals”. But in HOL’s currently formalization,
cardinalTheory is depended by ordinalTheory, and ordinalTheory didn’t define
“cardinal numbers” at all. Whenever an informal proof says "Let xxx be the
smallest infinite cardinal, such that …”, I don’t know how to formalize it at
all, because there’s no concept of “cardinal (number)” that I can use.
Further more, my Klop function has the type: ‘a ordinal -> (‘a, ‘b) CCS. I
have no way to change the first type variable to ‘c so that it’s independent
with type variables used in CCS, because ordinal numbers were actually written
as part of the CCS processes (as vertices in the lts graph). But this means I
have no way to use my previous proved theorem:
[ONE_ONE_IMP_NOTIN] Theorem
|- ∀A f. ONE_ONE f ⇒ ∃n. f n ∉ A
which is based on “univ_ord_greater_cardinal” in ordinalTheory. Because the
type unification will fail: for any set of type ``(:’a, ‘b) CCS -> bool``, I
have no way to say there’s always a bigger ‘a ordinal, which is “larger” than
the “cardinality” of the set. Also please noticed that, now my CCS is at
least as large as the “set" of all ‘a ordinals, because I do can inject each
single ordinals into a CCS process, i.e. my Klop function defined above.
I hope I’ve explained well for my two questions, let me summarize them again:
1. How to express the cardinality of a set as “cardinal numbers” in HOL?
2. How to find a larger ordinal for a set of custom-defined datatype, when
their type variables are related?
Best regards,
Chun Tian
[1]
https://github.com/binghe/informatica-public/blob/master/thesis/GraphScript.sml
[2] van Glabbeek, R.J.: A characterisation of weak bisimulation congruence.
Lecture notes in computer science. 3838, 26–39 (2005).
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
