[plt-scheme] redex model of pi calculus?

From: John Clements (johnbclements at gmail.com)
Date: Fri Oct 30 10:52:06 EDT 2009

On Oct 29, 2009, at 2:32 PM, Daniel Brown wrote:

> Hi John,
> I built a small redex model of communication in CCS a while back
> (attached). It's quite bare—just enough to do communication. I think
> the hardest part was devising a way to model the traces. Since redex
> doesn't let you compute labels for transitions, I just used a writer
> monad to accumulate a sequence of actions in the term configuration.
> Generalizing it from CCS to pi should be easy: just add substitutions.
> I haven't put any thought into modeling ν...

Well, my model is enormous and ungainly compared to yours, but I don't  
see a better way to do it. In particular, I gave up on trying to  
formulate a single canonical "flattest" representation for a given  
term as you were able to do, because of the replication nodes.  
Instead, I used evaluation contexts to look for reducible pairs, and  
stuck really close to the published algebra of terms; I even model  
parallel composition and zero directly rather than flattening them  
into lists.

Model attached, if you care to take a look.



-------------- next part --------------
A non-text attachment was scrubbed...
Name: pi-calculus.ss
Type: application/octet-stream
Size: 14870 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20091030/f25ad688/attachment.obj>
-------------- next part --------------

> Also, John Reppy's thesis has a reduction semantics for concurrent ML,
> so it might be a good source of ideas on how to model communicating
> systems in redex.
> I'd be interested to see what you come up with for modeling pi.
> (Feel free to copy this back to plt-scheme. I don't have a handle on
> the original thread, otherwise I would have replied to it instead.)
> Dan
> On Tue, Oct 27, 2009 at 14:50, Sam TH <samth at ccs.neu.edu> wrote:
>> ---------- Forwarded message ----------
>> From: John Clements <clements at brinckerhoff.org>
>> Date: Tue, Oct 27, 2009 at 2:36 PM
>> Subject: [plt-scheme] redex model of pi calculus?
>> To: Robby Findler <robby at eecs.northwestern.edu>
>> Cc: PLT-Scheme Mailing List <plt-scheme at list.cs.brown.edu>
>> I'm trying to model a pi-calculus-like system in redex, and running
>> into a couple of issues that would be solved by any model for the pi
>> calculus in redex. Before I try solving them all myself (parallel
>> composition, lifting nu's) I thought I'd ask: are there existing
>> models of the pi calculus written using redex?
>> John
>> _________________________________________________
>>  For list-related administrative tasks:
>>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>> --
>> sam th
>> samth at ccs.neu.edu
> <ccs.scm>

Posted on the users mailing list.