K-user mailing list

[Traian Florin Şerbănuţă <traian.serbanuta AT unibuc.ro>]

We used to have visiting capacity in an earlier version of K.  That could be used to implement operations like quote/unquote and substitution and basically any kind of term traversal.

Some hints of that can be seen in https://github.com/kframework/k/blob/master/k-distribution/samples/agent/quote-unquote.k

Unfortunately, as the codebase transformed, this functionality seems to have been lost in the newer versions.

I'll try to see if I can get something working out of it for you to get an idea.

best wishes,

Traian

On Tue, Jul 25, 2017 at 7:56 PM Mike Stay <stay AT pyrofex.net> wrote:

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.