Hi,
sorry for keeping asking questions. In my current CCS datatype, there's a
recursive constructor:
val _ = Datatype `CCS = nil
| var 'a
...
| rec 'a CCS `;
A term ``rec X (f (var X))`` is like the solution of an equation X = f(X),
or the fixed-point of f(), and its behavior is then defined by a set of
rules. What the Datatype package gives me, is to make sure "rec" and "var"
are kind of *primitive* constants, such that they're part of the one_one
and distinctness theorems of the CCS. (if I simply define a constant
outside of the datatype, I don't have such benefits at all, and many
theorems will not be proved)
Now (as a long-term plan) I want to implement the ultimate, original form
of Milner's CCS [1], in which there's a "fix" (fixed-point) constructor.
It's like a multi-variable version of above "rec" costructor, something
like:
fix X p1 Y p2 Z p3 ...
If you think above term as a multi-variable equation groups, then each part
in its solution will be defined as a valid CCS term. Such a "solution" (as
a container of CCS terms) may be represented as a finite_map ``:('a |->
('a, 'b) CCS)`` or simply a list ``:('a, 'b) CCS list``.
Obviously I can't put this "fix" directly into the definition of above CCS
datatype (let's assume HOL4 can do support nesting recursive datatype),
because the type of ``fix ...`` is *not* CCS at all. But what is it if I
want such a constant? some kind of specification?
Regards,
Chun Tian
--
Chun Tian (binghe)
University of Bologna (Italy)
[1] Milner, R.: Operational and Algebraic Semantics of Concurrent
Processes. 1–41 (2017).
------------------------------------------------------------------------------
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
