Thanks for your comments. If I quotient [1] the original CCS datatype into another one, I could expect to have the a “fix” constructor with a finite map, right?
On the the other side, what if I directly define another similar constant, say “Fix” in this form: |- Fix fm X = fix (alist_to_fmap ls) X And in all theorems I only use “Fix”. Is this possible (as a cheap solution) for resolving the “structural congruences” issue? Regards, Chun Tian [1] Homeier, P.V.: Higher Order Quotients in Higher Order Logic. preparation; draft available at http://www cis …. (1969). > Il giorno 27 ott 2017, alle ore 00:20, michael.norr...@data61.csiro.au ha > scritto: > > 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> > 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
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
