Chemical Abstract Machines (ChAMs) and Related Calculi: HoPL 3/22/2004

Presented by Peter Douglass
Transcribed by Jeffrey Palm

Berry and Boudol '90: Reflexive Chemical Abstract Machine

Model a system by a solution or multiset S. Analogy to chemistry where molecules in a solution move freely, recombine, ...

Example

Consider a multiset S containing the integers 2 thru k, the reaction rule. 
m,nm -> n
Gives all prime numbers.

Can't do factorial easily. Can do lambda calculus, tccs, and a subsest of ccs.

Notation

Solutation: {|a, b, c |}
Air lock law: {| m,a,b,c,... |} <--> {| m <| {| --> --a,b,c,... |} |}

Constraint on rules: Any subexpression that is a multiset must be of the form:

Example

Rules:
ant,S-> do_and, {| end_and <| S |}
end_and,T-> end_and
end_and,F-> fail_and
fail_and,T-> fail_and
fail_and,F-> fail_and
do_and, {| end_and|}-> T
do_and, {| fail_and|}-> F
Example:
and, {| T,F |}
do_and, {| end_and <| {| T,F |} |}
do_and, {| end_and,T,F |}
do_and, {| end_and,F |}
do_and, {| fail_end |}
F
(Peter chastized me. Then Matthias chastized others)

Example

VT
forall(x) (2x)int -> eventparity
forall(x) (2x+1)int -> oddparity
forall(x,t) XT,XT -> XT

Example

forall(s) m,s -> {| start, {| finish, <| S |} |}
forall(x notin finish), forall(s) start, {| x <| S } -> f(x), start, x
start, {| finish |} ->???
What is this? map f Notice the "start" on both sides... this is a catalyst and this mimics changing dynamic scope.

Fournet and Gontheir '96:Reflexive ChAMs and the Join Calculus

Authors of CHAM thought writing programs that use channel hardwires things together and would be more flexible without them. However, current paper reintroduces channels.

Notation

X<V~> ::= send message X to all members of V.

P ::= X<V~>
| P1 | P2
| def D in P

J ::= X <V~ >
| J1 | J2

D ::= J |> P
| D1 ^ D2

Example

def ( ready(x) | job(y) ) |> x<y> in
   ( ready(laser1) | job(job1) | job(job2) ) 		--> laser1<job1> | job<job2>

Example

def x <A> | y<b> |> z<a+b> in
    x<1> | y<2> | x<3> | y<4> 		--> z<3> | z<7>
-or-
z<5> | z<5>

GC in RChAM

Couldn't do GC in RChAM because there were no containers.

Cardelli and Gordon '99Mobile Ambients

Define a calculus with
nNames
p,q::= Processes
| (Vn) P restriction
| 0 inactivity
| P|Q composition
| !P replication
| n[P] ambient
| m,P action
m::= Capabilities
|in n
|out n
|open n

Rules

in: 
                                  m
 n              m                *----------*
*--------*     *--------*        |          |
|        |  |  |        |        |  n       | 
| in m.P |  |  |   Q    |  --->  | *-*      |
|        |  |  |        |        | |P| | Q  |
*--------*     *--------*        | *-*      |
                                 *----------*
out: 
         m                          
       *-----------------* 
       | n               |      n        m
       | *---------* |   |     *---*  | *---*
       | | out m.P | | Q | --> | P |  | | Q |
       | *---------* |   |     *---*  | *---*
       |                 |
       *-----------------*
open: 
                      m
      *----------* | *---*     *-----*
      | open m.P | | | Q | --> | P|Q |
      *----------* | *---*     *-----*

Example

I'll scan and put in here.

Punchline

Dynamic scopes are useful for mobility. Matthias adds "this isn't dynamic scope, but symbols" and explains how one accomplishes this in Scheme.