3.13 Problem: Threads
Add process forking and channel-based communication to a
call-by-value functional language. Here is the proposed grammar:
(define-language Lambda (e ::= x (lambda (x_!_ ...) e) (e e ...) n (+ e e) (if0 e e e) (spawn e) (put c e) (get c) (void)) (n ::= number) (c ::= variable-not-otherwise-mentioned) (x ::= variable-not-otherwise-mentioned))
A (spawn e) expression creates a new thread from the given
sub-expression, while put and get expressions allow
these threads to communicate. Specifically, when one thread evaluates
(put c v) and another evaluates (get c) for the same
c, the get thread receives value v while the
put thread’s expression evaluates to (void).
Hints Instead of a single expression, your reductions must deal with a set of expressions, one per thread. Reducing (spawn e) in one of these expressions thus adds an e to that set; use (void) as the result of this action. When any one thread has (get c) as its redex and another has (put c v), the two redexes are simultaneously replaced with their contractions.
In Redex, sets are currently realized with sequences. The key difference is that sets are unordered and sequences are ordered. Keep this in mind when you formulate reduction relations for put-get communications.