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
