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>
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> 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)
>
>


-- 
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

Reply via email to