K-user mailing list

[Mike Stay <stay AT pyrofex.net>]

On Jul 24, 2017 7:34 PM, "Chen, Xiaohong" 
<xc3 AT illinois.edu>
 wrote:
> Dear Mike,
>
> I don't quite get your point. Why do want the variables appearing in a
> quoted program be bound variables? It would help us answering your
> questions if you could provide an example showing what you want to do.

Well, they really shouldn't be considered variables at all; a quoted
subtree should be thought of as merely describing a structure,
something like a string.  Since substitution only affects free
variables, binding all the variables accomplishes the same purpose.
Another way I thought of was to say

syntax Var ::= Id
syntax QuotedVar ::= Id
syntax KVariable ::= Var

and then rewrite all Vars under a quote to QuotedVars before allowing
the substitution rule to proceed.

My eventual goal is to implement Meredith and Radestock's reflective
higher-order pi calculus, in which names are quoted processes.  I
don't know if it's even possible to model in K framework, since in
this calculus, name equivalence is based on process equivalence.  The
first aspect I was trying to model was the fact that names appearing
in a quoted process are not free.

Syntax:

P,Q ::=
0   do nothing
| for (y <- x) { P }   input
| x!P   output
| P | Q   parallel composition
| *x   dereference

x,y ::= &P   quote
          | Id


Structural equivalence:
- (|, 0 form a commutative monoid)

  0 | P = P
  P | Q = Q | P
  (P | Q) | R = P | (Q | R)

- Quote and dereference are one-sided inverses

  &*n = n

- Structurally equivalent processes give equivalent names

  P ≡ Q => &P ≡ &Q


Rewrite rules:

for (y <- x) { P } | x!Q   =>   P[&Q / y]


Note that we send processes but receive names.  To illustrate free vs
bound names in the context of quoting, consider a process listening on
x for a message y in parallel with a process sending on x:

for ( y <- x ) {
    z!*y
    | &(&0 ! *y) ! 0
}
| x ! *r

=>

z ! *r
| &(&0 ! *y) ! 0

The first y gets replaced by &*r = r, but the second does not because
it is in a subtree under an &.

--
Mike Stay
CTO, Pyrofex Corp.