Operational semantics for Lambda 5
Paper: Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning
Ollibot code: Robert J. Simmons
This is a straightforward transcription of Figure 8 from A Symmetric
Modal Lambda Calculus for Distributed Computing (Tech report
CMU-CS-04-105) into substructural operational semantics as described
by Simmons & Pfenning. It is also presented in the same form in the paper
of the same name published in LICS 2004 (it is Figure 6).
We will represent different "locations" with atomic propositions @ W in
the context. Unline the examples from the LICS 2009
paper by Simmons & Pfenning, the stack will grow out to the right of an
active proposition, instead of to the left.
Operational Semantics
The rules are given abbreviated names, but are otherwise comparable to
Figure 8 in A Symmetric Modal Lambda Calculus for Distributed Computing.
Abbreviations e and i mean elimination and introduction, respectively;
p means push, s means swap, r means reduce,
and v means value. The names given in the tech report are mentioned
in comments to the left.
Values
These rules are not necessary in the system presented by Murphy et al: in
effect, they do not distinguish between eval and return. Because we
do, it is necessary to have a rule that switches from evaluating to
returning when an immediate value is reached.
⊃i-v : @ W • eval(lam λx.M x) ->> @ W • return(lam λx.M x).
♢i-v : @ W • eval(there W L) ->> @ W • return(there W L).
□i-v : @ W • eval(box λω.M ω) ->> @ W • return(box λω.M ω).
Basic types
⊃e-p : %% app-push
@ W • eval(app M N) ->>
@ W • eval(M) • comp(app □ N).
⊃e-s : %% app-flip
@ W • return(V) • comp(app □ N) ->>
@ W • eval(N) • comp(app V □).
⊃e-r : %% app-reduce
@ W • return(V) • comp(app (lam λx.M x) □) ->>
@ W • eval(M V).
Modal types
"Publishing" a value V in the table at world W is done by
creating a persistent atomic proposition !bind W L V, where L is
a fresh parameter.
♢i-p : %% here-push
@ W • eval(here M) ->>
@ W • eval(M) • comp(here □).
♢i-r : %% here-reduce
@ W • return(V) • comp(here □) ->>
@ W • ∃L. return(there W L) • !bind W L V. %% Bindings are located at a world
♢e-p : %% letd-push
@ W • eval(letdia M λω.λx.N ω x) ->>
@ W • eval(M) • comp(letdia □ λω.λx.N ω x).
♢e-r : %% letd-reduce
@ W • return(there W' L) • comp(letdia □ λω.λx.N ω x) ->>
@ W • eval(N W' L).
The lookup rule requires that the the current world and the location both
match; this corresponds to the notion that we can only dereference addresses
in our own local table.
lookup :
@ W • eval(L) • !bind W L V ->>
@ W • return(V).
The authors used the non-let version of box elimination, though they
mention that a letbox constructor (like the letdia constructor)
could have alternatively been used.
□e-p : %% unbox-push
@ W • eval(unbox M) ->>
@ W • eval(M) • comp(unbox □).
□e-r : %% unbox-reduce
@ W • return(box λw.M w) • comp(unbox □) ->>
@ W • return(M W).
Communication
Each rule for remote communication is split into two steps; the first
creates a mobile message, and the second connects that mobile message at
the correct position.
ret1 : %% return (first part)
@ W' • return(V) • comp-return(W) ->>
@ W' • ¡msg-return W V.
ret2 : %% return (second part)
@ W • ¡msg-return W V ->>
@ W • return(V).
The two expressions fetch W M and get W M have the same operational
semantics but different typing rules (in particular, fetch requires
its subexpression to be of box type, and get requires its subexpression to
be of diamond type). In Tom Murphy's thesis work, this was generalized
to to a single get expression, which requires its subexpression to have
some mobile type; among the mobile types are box and diamond types.
fetch1 : %% fetch-push (first part)
@ W • eval(fetch W' M) ->>
@ W • ¡msg-send W W' M.
fetch2 : %% fetch-push (second part)
@ W' • ¡msg-send W W' M ->>
@ W' • eval(M) • comp-return(W).
get1 : %% get-push (first part)
@ W • eval(get W' M) ->>
@ W • ¡msg-send W W' M.
get2 : %% get-push (second part)
@ W' • ¡msg-send W W' M ->>
@ W' • eval(M) • comp-return(W).
Example traces
First, we show a "round trip" - a valid value being passed from the
client to the server, and then back to the client.
%trace * @ server • @ client • eval(get server (get client (box λω. lam λx.x))).
@(server)•@(client)•eval(get server (get client (box(λω. lam(λx. x)))))
¡msg-send client server (get client (box(λω. lam(λx. x))))•@(server)•@(client)
@(server)•eval(get client (box(λω. lam(λx. x))))•comp-return(client)•@(client)
¡msg-send server client (box(λω. lam(λx. x)))•@(server)•comp-return(client)•@(client)
@(server)•comp-return(client)•@(client)•eval(box(λω. lam(λx. x)))•comp-return(server)
@(server)•comp-return(client)•@(client)•return(box(λω. lam(λx. x)))•comp-return(server)
¡msg-return server (box(λω. lam(λx. x)))•@(server)•comp-return(client)•@(client)
@(server)•return(box(λω. lam(λx. x)))•comp-return(client)•@(client)
¡msg-return client (box(λω. lam(λx. x)))•@(server)•@(client)
@(server)•@(client)•return(box(λω. lam(λx. x)))
We can escalate this as much as we want... this trace stops after
17 steps at the point where the client is finally prepared to return
the value to the server. Both the client and the server have four
local stacks at this point that are waiting to receive a value
(from anywhere; it is up to the typing invariant ensures that it is from
the "right place") and send the recieved item on to somewhere else.
%trace 17 @ server •
@ client • eval(get server
(get client
(get server
(get client
(get server
(get client
(get server
(get client (box λω. lam λx.x))))))))).
@(server)•@(client)•eval(get server (get client (get server (get client (get server (get client (get server (get client (box(λω. lam(λx. x)))))))))))
¡msg-send client server (get client (get server (get client (get server (get client (get server (get client (box(λω. lam(λx. x))))))))))•@(server)•@(client)
@(server)•eval(get client (get server (get client (get server (get client (get server (get client (box(λω. lam(λx. x))))))))))•comp-return(client)•@(client)
¡msg-send server client (get server (get client (get server (get client (get server (get client (box(λω. lam(λx. x)))))))))•@(server)•comp-return(client)•@(client)
@(server)•comp-return(client)•@(client)•eval(get server (get client (get server (get client (get server (get client (box(λω. lam(λx. x)))))))))•comp-return(server)
¡msg-send client server (get client (get server (get client (get server (get client (box(λω. lam(λx. x))))))))•@(server)•comp-return(client)•@(client)•comp-return(server)
@(server)•eval(get client (get server (get client (get server (get client (box(λω. lam(λx. x))))))))•comp-return(client)•comp-return(client)•@(client)•comp-return(server)
¡msg-send server client (get server (get client (get server (get client (box(λω. lam(λx. x)))))))•@(server)•comp-return(client)•comp-return(client)•@(client)•comp-return(server)
@(server)•comp-return(client)•comp-return(client)•@(client)•eval(get server (get client (get server (get client (box(λω. lam(λx. x)))))))•comp-return(server)•comp-return(server)
¡msg-send client server (get client (get server (get client (box(λω. lam(λx. x))))))•@(server)•comp-return(client)•comp-return(client)•@(client)•comp-return(server)•comp-return(server)
@(server)•eval(get client (get server (get client (box(λω. lam(λx. x))))))•comp-return(client)•comp-return(client)•comp-return(client)•@(client)•comp-return(server)•comp-return(server)
¡msg-send server client (get server (get client (box(λω. lam(λx. x)))))•@(server)•comp-return(client)•comp-return(client)•comp-return(client)•@(client)•comp-return(server)•comp-return(server)
@(server)•comp-return(client)•comp-return(client)•comp-return(client)•@(client)•eval(get server (get client (box(λω. lam(λx. x)))))•comp-return(server)•comp-return(server)•comp-return(server)
¡msg-send client server (get client (box(λω. lam(λx. x))))•@(server)•comp-return(client)•comp-return(client)•comp-return(client)•@(client)•comp-return(server)•comp-return(server)•comp-return(server)
@(server)•eval(get client (box(λω. lam(λx. x))))•comp-return(client)•comp-return(client)•comp-return(client)•comp-return(client)•@(client)•comp-return(server)•comp-return(server)•comp-return(server)
¡msg-send server client (box(λω. lam(λx. x)))•@(server)•comp-return(client)•comp-return(client)•comp-return(client)•comp-return(client)•@(client)•comp-return(server)•comp-return(server)•comp-return(server)
@(server)•comp-return(client)•comp-return(client)•comp-return(client)•comp-return(client)•@(client)•eval(box(λω. lam(λx. x)))•comp-return(server)•comp-return(server)•comp-return(server)•comp-return(server)
@(server)•comp-return(client)•comp-return(client)•comp-return(client)•comp-return(client)•@(client)•return(box(λω. lam(λx. x)))•comp-return(server)•comp-return(server)•comp-return(server)•comp-return(server)
Multiple worlds are not necessary, here is a one-world trace where the
client continually gets from itself.
%trace *
@ client • eval(get client (get client (get client (box λω. lam λx.x)))).
@(client)•eval(get client (get client (get client (box(λω. lam(λx. x))))))
¡msg-send client client (get client (get client (box(λω. lam(λx. x)))))•@(client)
@(client)•eval(get client (get client (box(λω. lam(λx. x)))))•comp-return(client)
¡msg-send client client (get client (box(λω. lam(λx. x))))•@(client)•comp-return(client)
@(client)•eval(get client (box(λω. lam(λx. x))))•comp-return(client)•comp-return(client)
¡msg-send client client (box(λω. lam(λx. x)))•@(client)•comp-return(client)•comp-return(client)
@(client)•eval(box(λω. lam(λx. x)))•comp-return(client)•comp-return(client)•comp-return(client)
@(client)•return(box(λω. lam(λx. x)))•comp-return(client)•comp-return(client)•comp-return(client)
¡msg-return client (box(λω. lam(λx. x)))•@(client)•comp-return(client)•comp-return(client)
@(client)•return(box(λω. lam(λx. x)))•comp-return(client)•comp-return(client)
¡msg-return client (box(λω. lam(λx. x)))•@(client)•comp-return(client)
@(client)•return(box(λω. lam(λx. x)))•comp-return(client)
¡msg-return client (box(λω. lam(λx. x)))•@(client)
@(client)•return(box(λω. lam(λx. x)))
We can have more than two worlds, as this example with worlds a, b,
and c shows.
%trace *
@ a • eval(get b (get c (get b (get a (box λω. lam λx.x))))) • @ b • @ c.
@(a)•eval(get b (get c (get b (get a (box(λω. lam(λx. x)))))))•@(b)•@(c)
¡msg-send a b (get c (get b (get a (box(λω. lam(λx. x))))))•@(a)•@(b)•@(c)
@(a)•@(b)•eval(get c (get b (get a (box(λω. lam(λx. x))))))•comp-return(a)•@(c)
¡msg-send b c (get b (get a (box(λω. lam(λx. x)))))•@(a)•@(b)•comp-return(a)•@(c)
@(a)•@(b)•comp-return(a)•@(c)•eval(get b (get a (box(λω. lam(λx. x)))))•comp-return(b)
¡msg-send c b (get a (box(λω. lam(λx. x))))•@(a)•@(b)•comp-return(a)•@(c)•comp-return(b)
@(a)•@(b)•eval(get a (box(λω. lam(λx. x))))•comp-return(c)•comp-return(a)•@(c)•comp-return(b)
¡msg-send b a (box(λω. lam(λx. x)))•@(a)•@(b)•comp-return(c)•comp-return(a)•@(c)•comp-return(b)
@(a)•eval(box(λω. lam(λx. x)))•comp-return(b)•@(b)•comp-return(c)•comp-return(a)•@(c)•comp-return(b)
@(a)•return(box(λω. lam(λx. x)))•comp-return(b)•@(b)•comp-return(c)•comp-return(a)•@(c)•comp-return(b)
¡msg-return b (box(λω. lam(λx. x)))•@(a)•@(b)•comp-return(c)•comp-return(a)•@(c)•comp-return(b)
@(a)•@(b)•return(box(λω. lam(λx. x)))•comp-return(c)•comp-return(a)•@(c)•comp-return(b)
¡msg-return c (box(λω. lam(λx. x)))•@(a)•@(b)•comp-return(a)•@(c)•comp-return(b)
@(a)•@(b)•comp-return(a)•@(c)•return(box(λω. lam(λx. x)))•comp-return(b)
¡msg-return b (box(λω. lam(λx. x)))•@(a)•@(b)•comp-return(a)•@(c)
@(a)•@(b)•return(box(λω. lam(λx. x)))•comp-return(a)•@(c)
¡msg-return a (box(λω. lam(λx. x)))•@(a)•@(b)•@(c)
@(a)•return(box(λω. lam(λx. x)))•@(b)•@(c)