Tiny Ollibot Example Server - Call-by-need functions

Asynchronous communication

Robert J. Simmons, Frank Pfenning

This example is derived from Figures 3 and 6 in Substructural Operational Semantics as Ordered Logic Programming.

Call-by-value functions

r1 : eval(lam λx. E x) ->> return(lam E).
r2 : eval(app E1 E2) ->> comp(app1 E2) • eval(E1).
r3 : comp(app1 E2) • return(V1) ->> comp(app2 V1) • eval(E2).
r4 : comp(app2 (lam λx.E0 x)) • return(V2) ->> eval(E0 V2).

Asynchronous communication

enew : eval(new (λx. E x)) ->> ∃C. eval(E C).
esnd1 : eval(send C E) ->> comp(send1 C) • eval(E).
esnd2 : comp(send1 C) • return(V) ->> ¡msg C V • return(V).
ercv1 : eval(rcv C) ->> comp(await C).
ercv2 : comp(await C) • ¡msg C V ->> return(V).

Some constants

Just so that there's some slightly-meaningful messages to send around:

econst : eval(const C) ->> return(const C).

Example trace

The first process creates a channel, and then passes that newly generated channel along an existing channel chan1 to the third process. The third process is inside of a higher-order function that allows the process to send back an acknowledgement to the first process. The second process is just a dummy to emphasize that the communication is nonlocal.

%trace * 
∃chan1. eval(new λchan2. app (lam λx. rcv chan2) 
                              (send chan1 (lam λx. send chan2 x)))
      • eval (const unit)
      • eval(app (lam λx. const unit) (app (rcv chan1) (const ack))).
eval(new(λchan2. app (lam(λx. rcv(chan2))) (send d2 (lam(λx. send chan2 x)))))•eval(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
eval(app (lam(λx. rcv(d3))) (send d2 (lam(λx. send d3 x))))•eval(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
comp(app1(send d2 (lam(λx. send d3 x))))•eval(lam(λx. rcv(d3)))•eval(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
comp(app1(send d2 (lam(λx. send d3 x))))•return(lam(λx. rcv(d3)))•eval(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
comp(app2(lam(λx. rcv(d3))))•eval(send d2 (lam(λx. send d3 x)))•eval(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
comp(app2(lam(λx. rcv(d3))))•comp(send1(d2))•eval(lam(λx. send d3 x))•eval(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
comp(app2(lam(λx. rcv(d3))))•comp(send1(d2))•return(lam(λx. send d3 x))•eval(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
¡msg d2 (lam(λx. send d3 x))•comp(app2(lam(λx. rcv(d3))))•return(lam(λx. send d3 x))•eval(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
¡msg d2 (lam(λx. send d3 x))•eval(rcv(d3))•eval(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
¡msg d2 (lam(λx. send d3 x))•comp(await(d3))•eval(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
¡msg d2 (lam(λx. send d3 x))•comp(await(d3))•return(const(unit))•eval(app (lam(λx. const(unit))) (app (rcv(d2)) (const(ack))))
¡msg d2 (lam(λx. send d3 x))•comp(await(d3))•return(const(unit))•comp(app1(app (rcv(d2)) (const(ack))))•eval(lam(λx. const(unit)))
¡msg d2 (lam(λx. send d3 x))•comp(await(d3))•return(const(unit))•comp(app1(app (rcv(d2)) (const(ack))))•return(lam(λx. const(unit)))
¡msg d2 (lam(λx. send d3 x))•comp(await(d3))•return(const(unit))•comp(app2(lam(λx. const(unit))))•eval(app (rcv(d2)) (const(ack)))
¡msg d2 (lam(λx. send d3 x))•comp(await(d3))•return(const(unit))•comp(app2(lam(λx. const(unit))))•comp(app1(const(ack)))•eval(rcv(d2))
¡msg d2 (lam(λx. send d3 x))•comp(await(d3))•return(const(unit))•comp(app2(lam(λx. const(unit))))•comp(app1(const(ack)))•comp(await(d2))
comp(await(d3))•return(const(unit))•comp(app2(lam(λx. const(unit))))•comp(app1(const(ack)))•return(lam(λx. send d3 x))
comp(await(d3))•return(const(unit))•comp(app2(lam(λx. const(unit))))•comp(app2(lam(λx. send d3 x)))•eval(const(ack))
comp(await(d3))•return(const(unit))•comp(app2(lam(λx. const(unit))))•comp(app2(lam(λx. send d3 x)))•return(const(ack))
comp(await(d3))•return(const(unit))•comp(app2(lam(λx. const(unit))))•eval(send d3 (const(ack)))
comp(await(d3))•return(const(unit))•comp(app2(lam(λx. const(unit))))•comp(send1(d3))•eval(const(ack))
comp(await(d3))•return(const(unit))•comp(app2(lam(λx. const(unit))))•comp(send1(d3))•return(const(ack))
¡msg d3 (const(ack))•comp(await(d3))•return(const(unit))•comp(app2(lam(λx. const(unit))))•return(const(ack))
return(const(ack))•return(const(unit))•comp(app2(lam(λx. const(unit))))•return(const(ack))
return(const(ack))•return(const(unit))•eval(const(unit))
return(const(ack))•return(const(unit))•return(const(unit))