Using alists rather than finite-maps will have the issue that
fix [(X, a + Y); (Y, b + X)] X
will be seen as different to
fix [(Y, b + X); (X, a + Y)] X
when you might prefer them to be syntactically identical, but there are so many
“structural congruences” in this syntax that having to deal with one more
perhaps won’t be such a big deal.
And of course, you could try quotienting it up to all those identities….
Michael
From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
Date: Thursday, 26 October 2017 at 21:00
To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] How to define term-like multi-recursive structures?
Hi again,
I'm surprised that, ``('a, 'b) alist`` (or ``('a # 'b) list``) is supported by
datatype package. So I'm going to have the following datatype in the future:
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)
| fix (('a # CCS) list) 'a `;
I wanted to use finite_map (learnt from Konrad Slind) but datatype package
doesn't support it, however alist is a prefect replacement.
Thus I would say my question can be closed, if there's no other suggestions.
Regards,
Chun Tian
On Thu, Oct 26, 2017 at 10:56 AM, Chun Tian (binghe)
<binghe.l...@gmail.com<mailto:binghe.l...@gmail.com>> wrote:
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<mailto: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<mailto:binghe.l...@gmail.com>>
Date: Thursday, 26 October 2017 at 00:05
To: hol-info
<hol-info@lists.sourceforge.net<mailto: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<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Chun Tian (binghe)
University of Bologna (Italy)
--
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
