Let me describe the problem again: (actually I have a candidate solution)
The central idea in the CCS grammar designed by Robin Milner is to use
inductively defined finite structures to represent potential infinite
structures. If I have the following equation of CCS:
X = a + X
The only solution would be an infinite sum of a:
X = a + a + a + ...
But we don't really need the infinite sum as part of CCS grammar, we can
write this form instead:
rec X (a + var X)
So the "equation with single variable" itself can be treated as a CCS
process. But if I have multi-variable equations:
X = a + Y
Y = b + X
the solution should be:
X = a + b + a + b + ...
Y = b + a + b + a + ...
to represent the equation itself as a CCS process, I should at least put
the following "fix" constructor into the datatype:
fix ('a list) (CCS list) 'a
so that I can write a term
``fix [X; Y] [a + var Y; b + var X] X``
which means "the value of X in the equation group in which X and Y are
unknown variables". But if I write only partially:
``fix [X; Y] [a + var Y; b + var X]``
above term should have the type ``:'a -> ('a, 'b) CCS``, which works like a
choice function, given any variable it returns the corresponding value of
that variable.
In my initial question, I wanted to put only ``fix ('a list) (CCS list)``
into the CCS datatype, and that was wrong because the type of ``fix ('a
list) (CCS list)`` is not CCS, but (CCS list).
Can you see a better way to have a similar datatype?
Regards,
Chun Tian
On Thu, Oct 26, 2017 at 1:20 AM, <michael.norr...@data61.csiro.au> wrote:
> I’m not sure why you say that you can’t add “fix” to the datatype
> declaration.
>
> A line like
>
> | fix (CCS list)
>
> would be accepted by Datatype. Then the type of the constructor “fix”
> would be
>
> fix : ('a,'b) CCS list -> ('a,'b) CCS
>
> In short, I don't understand why you write "the type of ``fix …`` is *not*
> CCS at all".
>
> If your underlying constructors don't allow for "infinite" CCS terms (or
> their encoding), then it's hard to know how you would ever define the sorts
> of CCS constants that have infinite behaviours in time. Perhaps one
> approach would be to define the syntax as a co-datatype, allowing the
> syntax itself to be infinite. This'd be a bit weird though…
>
> Michael
>
> From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
> Date: Thursday, 26 October 2017 at 00:05
> To: hol-info <hol-info@lists.sourceforge.net>
> Subject: [Hol-info] How to define term-like multi-recursive structures?
>
> 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
>
--
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
