Skip to content

Instantly share code, notes, and snippets.

@JoshOrndorff JoshOrndorff/pi.k
Last active Jun 5, 2018

Embed
What would you like to do?
My work-in-progress pi-calculus in k framework
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
joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ cat test1
(@)
joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ krun test1
<k>
( @ )
</k>
joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ cat test2
x~y
joshy@MicrosoftSurface:~/ProgrammingProjects/k-framework/piCalc.k$ krun test2
<k>
x ~ y
</k>
// 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>
// 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>
@Jake-Gillberg

This comment has been minimized.

Copy link

Jake-Gillberg commented Jun 5, 2018

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)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.