[plt-scheme] redex model of pi calculus?

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.

Thanks!

John

-------------- 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>