Tiny Ollibot Example Server - Call-by-need functions

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.


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


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)