My work-in-progress pi-calculus in k framework

pi.k

module PI-SYNTAX
  imports DOMAINS

  // Processes
  syntax Proc ::= Norm                   // Normal processes are still processes
                | Proc "|" Proc          // Parallel
                | "!" Proc               // Replication
                | "(" "v" Id ")" Proc    // New name
                | "(" Proc ")"           // Allow parens for grouping

  // Normal Processes
  syntax Norm ::= Pi "." Proc      // Prefixing
                | "@"              // Trivial Process. Looks kinda like empty set.
                | Norm "+" Norm    // Summation
             // | Pi               // Could allow Milner shorthand for Pi.0

  // Atomic Actions
  syntax Pi ::= Id "(" Id ")"    // Receive
              | Id "~" Id        // Send. Looks kinda like overbar
endmodule

module PI
  imports PI-SYNTAX
endmodule

// Questions:
// Why can I just refer to a name like "x"? Is that what DOMAINS gets me? (reference below)
// Since the shorthand is commented, x~y shouldn't be a thing. How do I tell kompile that the top level entity should be a Proc?
// How do we teach kframework the actual reduction rules? Maybe involves importing SUBSTITUTION ?


// Helpful references:
// Our zoom sesssion: https://youtu.be/iX5L8lGynNo?t=32m23s
// Official lambda example:  https://github.com/kframework/k5/blob/master/k-distribution/tutorial/1_k/1_lambda/lesson_1/lambda.k
// DOMAINS package: https://github.com/kframework/k5/blob/master/k-distribution/include/builtin/domains.k

test1.log

joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ cat test1
(@)

joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ krun test1
<k>
  ( @ )
</k>

test2.log

joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ cat test2 
x~y

joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ krun test2
<k>
  x ~ y
</k>

test3.log

// This example taken from Milner tutorial. Be careful not to use v as a name. v mean nu!

joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ cat test3
(v x)(x~y.@ | x(u).u~w.@) | x~z.@

joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ krun test3
<k>
  ( ( v x ) ( x ~ y . ( @ | x ( u ) . u ~ w . @ ) ) ) | x ~ z . @
</k>

test4.log

// This example taken from Milner tutorial. Be careful not to use v as a name. v mean nu!

joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ cat test4
x~y.@ | !x(u).u~w.@ | x~z.@

joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ krun test4
<k>
  ( x ~ y . @ ) | ( ( ! x ( u ) . u ~ w . @ ) | x ~ z . @ )
</k>

Why can I just refer to a name like "x"? Is that what DOMAINS gets me? (reference below)

Yup, more specifically the ID module within domains.k, which you can import instead of DOMAINS (since you aren't using Int or anything else in that package for now) with imports ID. See the regex that your "x" matches to become an Id here

Since the shorthand is commented, x~y shouldn't be a thing. How do I tell kompile that the top level entity should be a Proc?

Great question! Check out the kast --sort option. We will also find a fun way to define the default top level entity when we get into defining configurations.

How do we teach kframework the actual reduction rules? Maybe involves importing SUBSTITUTION ?

That would be a start. The full answer is I'm not totally sure yet. If you want to cheat and look ahead, I know that there is an implementation of the semantics for pi in this paper and in the rchain repo.

Other hints for improvement: there are still ambiguities in your grammar. To see the ambiguities in say, test3, run kast -w all test3.pi (and you might want to add a -s option to that command as well...). To resolve these ambiguities, you will need to figure out how to define rule precedence and associativity (hint, hint, hint)