Modelling Actors with Redex: Part I

# Modelling Actors with Redex: Part I (eighty-twenty news) Source: [https://eighty-twenty.org/2016/08/18/redex-iswim](https://eighty-twenty.org/2016/08/18/redex-iswim) This is the first part of a series of three articles on modelling*actor\-like systems*,[1](https://eighty-twenty.org/2016/08/18/redex-iswim#fn:Hewitt73)[2](https://eighty-twenty.org/2016/08/18/redex-iswim#fn:DeKoster16)similar to[Erlang](http://erlang.org/)and to my own work on[Syndicate](http://syndicate-lang.org/), using[PLT Redex](https://redex.racket-lang.org/), “a domain\-specific language designed for specifying and debugging operational semantics\.” - [Part I: The Functional Fragment: ISWIM in Redex](https://eighty-twenty.org/2016/08/18/redex-iswim) - [Part II: The Communicating Fragment: Actors in Redex](https://eighty-twenty.org/2016/08/18/redex-iswim-with-actors) - [Part III: Efficiency vs\. Nondeterminism](https://eighty-twenty.org/2026/08/03/redex-iswim-actors-efficient) [](http://creativecommons.org/licenses/by/4.0/)This post is written as a[literate Racket source file](https://eighty-twenty.org/files/redex/redex-iswim.rkt), and is licensed[CC\-BY 4\.0](http://creativecommons.org/licenses/by/4.0/)\. You can download it and run it yourself\. ## The Functional Fragment: ISWIM in Redex The Redex webpage promises: > Write down a grammar and the reduction rules, and PLT Redex allows you to interactively explore terms and to use randomized test generation to attempt to falsify properties of your semantics\. In this post, I’ll build a model of a simple “ISWIM”\-style, lambda\-calculus based functional programming language\. In subsequent posts, I’ll extend this little model to build it into an Erlang\-style actor system\. Here’s an example program in the language: ``` ((rec loop (lambda (count) (if (= count 0) nil (cons count (loop (- count 1)))))) 3) ``` And here’s a screenshot of the Redex trace visualizer showing reductions of the program:  ## Preliminaries [ISWIM](https://en.wikipedia.org/wiki/ISWIM)is a programming language*gedankenexperiment*invented by Peter Landin in his famous paper, “The Next 700 Programming Languages”\.[3](https://eighty-twenty.org/2016/08/18/redex-iswim#fn:Landin66)It is essentially a Scheme\-like language; a fairly minimal extension of the lambda calculus\. Our model will be an ISWIM\-like language supporting S\-expressions, numbers, strings, and booleans\. First of all, we need the Racket`\#lang`header: ``` #lang racket ``` Next, we load Redex\. ``` (require redex) ``` ## Syntax We begin by declaring the \(S\-expression\-based\) syntax we will use for programs written in our language\. ``` (define-language ISWIM ``` ### Expressions, Values and Variables Our first nonterminal is`expr`, syntax for expressions in our language\. An expression can be any of the following options: ``` (expr x ;; a variable reference value ;; a value (see below) (cons expr expr) ;; the construction of a pair (expr expr ...) ;; a function call (prim expr ...) ;; a primitive operation call (begin expr ...) ;; a sequence of expressions (if expr expr expr) ;; a conditional (rec x expr)) ;; a recursive expression ``` Notice the lack of imperative constructions\. When we get to Part II, we’ll add some imperative commands, like “send message”\. Despite this lack, we still let programs written in this language use`begin`, because it is more ISWIM\-ish than specifically Actors\-ish, and it will be useful later\.[4](https://eighty-twenty.org/2016/08/18/redex-iswim#fn:begin-with-no-expressions) Values,`value`, in our language can be any of the following: ``` (value (lambda (x ...) expr ...) ;; a literal function number ;; a literal number string ;; a literal string boolean ;; a literal boolean nil ;; the special value `nil` (cons value value)) ;; a constructed pair of values ``` We’re playing an interesting trick here, letting the`cons`constructor serve as both an expression and as a value\. Once both arguments to`cons`have been reduced to values, the whole piece of syntax represents the final pair\. We let the syntactic nonterminal`x`stand for variables in our language: ``` (x variable-not-otherwise-mentioned) ``` ### Evaluation Contexts and Primitive Operators Our model uses the idea of*evaluation contexts*invented by Felleisen et al\. in 1986\.[5](https://eighty-twenty.org/2016/08/18/redex-iswim#fn:onContexts)[6](https://eighty-twenty.org/2016/08/18/redex-iswim#fn:Felleisen86)[7](https://eighty-twenty.org/2016/08/18/redex-iswim#fn:Felleisen87)An evaluation context is a term with a hole in it\. The hole is, roughly, the position in the term where some reduction can happen: where a*redex*is waiting to be reduced\. This definition of evaluation contexts forces evaluation of function arguments to happen in left\-to\-right order\. ``` (context hole (value ... context expr ...) (prim value ... context expr ...) (cons context expr) (cons value context) (begin context expr expr ...) (if context expr expr)) ``` We define a small set of primitive operators for manipulating data in our language\. Other operators can be added by extending the definition of the`prim`nonterminal and by adding clauses to the metafunction`delta`below\. ``` (prim + - = car cdr pair? null?) ``` ### Binding structure of the language I first learned Redex by taking a course based on “Semantics Engineering with PLT Redex”\.[8](https://eighty-twenty.org/2016/08/18/redex-iswim#fn:Felleisen09)An important part of programming with Redex at the time was implementing*substitution functions*correctly, respecting the binding structure of the language\. This was a difficult, error\-prone and annoying part of using the system\. Since then, Paul Stansifer has completed his dissertation work,[9](https://eighty-twenty.org/2016/08/18/redex-iswim#fn:Stansifer16)and as a result, Redex programmers can specify a language’s binding structure directly as part of the syntax, meaning that substitution and alpha\-equivalence functions can be automatically produced by the system\. We no longer have to write substitution functions by hand\! Here, to make use of Paul’s work, we specify the binding structure for`lambda`and`rec`forms: the formal parameters to a function are bound in the function body, and the recursively\-bound identifier is bound in the contained expression, respectively\. ``` #:binding-forms (lambda (x ...) expr #:refers-to (shadow x ...) ...) (rec x expr #:refers-to x)) ``` The documentation for this neat feature is available[here](https://docs.racket-lang.org/redex/Languages.html#(part._.Binding_.Forms))\. ## Operational Semantics ### Reduction Rules Our reduction relation will combine a*notion of reduction*, capturing the essence of each reduction rule, with use of the*evaluation contexts*we defined earlier\. Roughly speaking, the way we use evaluation contexts makes a notion of reduction in every potentially\-reducible position in a complex term, even though the notion of reduction is specified in terms of a particular redex and reduct isolated from their context\. ``` (define ISWIM-red (reduction-relation ISWIM ``` The first notion of reduction is the beta rule, for function calls\. We will see the definition of the`subst\-all`metafunction below\. ``` (==> ((lambda (x ...) expr ...) value ...) (begin (subst-all expr (x ...) (value ...)) ...) beta) ``` Primitive operators are interpreted by delegating to the`delta`metafunction, also defined below\. ``` (==> (prim value ...) (delta prim (value ...)) delta) ``` When only one expression remains in a`begin`expression, we should replace the`begin`with the expression\. ``` (==> (begin expr) expr begin-one) ``` If the first expression in a`begin`has been completely reduced \(to a`value`\), then discard the value, and move on to reducing the remaining expressions in the`begin`\. ``` (==> (begin value expr_0 expr ...) (begin expr_0 expr ...) begin-many) ``` If the test position in an`if`has reduced to`\#t`\(Scheme notation for “true”\), then replace the whole`if`with just the “then”\-part\. ``` (==> (if #t expr_0 expr_1) expr_0 if-true) ``` Likewise with the “else” part, in case the test position reduced to`\#f`\(“false”\)\. ``` (==> (if #f expr_0 expr_1) expr_1 if-false) ``` Recursive values, usually functions, are handled by*unfolding*them: replacing uses of the recursively\-bound variable in the body with a copy of the whole recursive value itself\. ``` (==> (rec x expr) (substitute expr x (rec x expr)) unfold) ``` This is the first use we’ve seen of the generic[`substitute`](https://docs.racket-lang.org/redex/Languages.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._substitute%29%29)metafunction that Redex provides for us when we specify binding structure in the way we did above\. Finally, we bring together the notions of reduction with the contexts, by introducing what Redex calls a*shortcut*\. This little snippet of syntax gives meaning to the`==\>`arrow used above for the notions of reduction by relating it to an overall reduction arrow`\-\-\>`by placing the arguments to`==\>`in a particular context\. ``` with [(--> (in-hole context A) (in-hole context B)) (==> A B)])) ``` ### Metafunctions Our primitive operators are given meaning by the`delta`metafunction, which uses Redex’s ability to reach out to the host language, Racket, to actually perform computations on base data like numbers and strings\. Pairs and`nil`aren’t treated quite the same as numbers and strings, since instead of being underlying Racket values, our pairs are “stuck” terms with the`cons`constructor at the head of the term\. ``` (define-metafunction ISWIM delta : prim (value ...) -> value [(delta + (number_0 number_1)) ,(+ (term number_0) (term number_1))] [(delta - (number_0 number_1)) ,(- (term number_0) (term number_1))] [(delta = (value_0 value_1)) ,(equal? (term value_0) (term value_1))] [(delta car ((cons value_0 value_1))) value_0] [(delta cdr ((cons value_0 value_1))) value_1] [(delta pair? ((cons value_0 value_1))) #t] [(delta pair? (value)) #f (side-condition (or (not (pair? (term value))) (not (eq? (car (term value)) 'cons))))] [(delta null? (nil)) #t] [(delta null? (value)) #f (side-condition (not (eq? (term value) 'nil)))]) ``` Substitution is taken care of us by the[`substitute`](https://docs.racket-lang.org/redex/Languages.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._substitute%29%29)metafunction, but we define`subst\-all`here to perform many substitutions at once\. ``` (define-metafunction ISWIM subst-all : expr (x ...) (value ...) -> expr [(subst-all expr () ()) expr] [(subst-all expr (x x_0 ...) (value value_0 ...)) (subst-all (substitute expr x value) (x_0 ...) (value_0 ...))]) ``` Finally, we build a kind of*macro*for our little language: the`let`form expands into a use of`lambda`\. ``` (define-metafunction ISWIM let : ((x expr) ...) expr ... -> expr [(let ((x_0 expr_0) ...) expr_1 ...) ((lambda (x_0 ...) expr_1 ...) expr_0 ...)]) ``` ## Examples and Tests At last, we have all the pieces we need to try out our language\! If you’re following along in[DrRacket](https://docs.racket-lang.org/drracket/), or have a graphical environment available, try the following expression in your REPL or IDE\. It should open a window that lets you explore the reduction of the term that we saw at the beginning of this article: ``` (traces ISWIM-red (term ((rec loop (lambda (count) (if (= count 0) nil (cons count (loop (- count 1)))))) 3))) ``` For noninteractive use such as test cases, Redex’s`test\-\-\>\>`function takes a term, reduces it as far as it will go, and compares the result to another term\. Here we put a few simple unit tests in a`test`[submodule](http://docs.racket-lang.org/guide/Module_Syntax.html?q=test%20submodule#%28part._main-and-test%29), so that they can be run by either DrRacket or by`raco test`on the command\-line\. ``` (module+ test (test-equal (term (delta null? (nil))) (term #t)) (test-->> ISWIM-red (term ((lambda (x) (+ x 1)) 123)) (term 124)) (test-->> ISWIM-red (term (let ((x 123)) (+ x 1))) (term 124)) (test-equal (term (delta = (1 2))) (term #f)) (test-equal (term (delta + (1 2))) (term 3)) (test-->> ISWIM-red (term (car (cons 1 (cons 2 nil)))) (term 1)) (test-->> ISWIM-red (term ((rec loop (lambda (count) (if (= count 0) nil (cons count (loop (- count 1)))))) 3)) (term (cons 3 (cons 2 (cons 1 nil))))) ) ``` ## Conclusion We have built a model of a simple lambda\-calculus based programming language\. We used the idea of evaluation contexts to specify the evaluation order of arguments to a function and of subterms of a`begin`expression\. In[Part II](https://eighty-twenty.org/2016/08/18/redex-iswim-with-actors), we’ll extend this language with some imperative actions, turning it into a model of Actors\. ## Exercises 1. \(Trivial\.\) Add a new primitive operator,`string\-append`, to the language\. 2. \(Easy\.\) By altering the definition of contexts, make the evaluation order of this language right\-to\-left instead of left\-to\-right\. 3. \(Medium\-Hard\.\) What happens if we try to reduce a function call to a function with duplicate names for its formal parameters, such as`\(\(lambda \(x x\) x\) 1 2\)`? Why does this happen? Alter the model so that such terms become “stuck”\. **Hint:**This is “Medium\-Hard” rather than just “Medium” because you have to dig into exactly how Redex’s built\-in substitution machinery works: the naive fix of a call to Racket’s[`check\-duplicates`](https://docs.racket-lang.org/reference/pairs.html#%28def._%28%28lib._racket%2Flist..rkt%29._check-duplicates%29%29)as a[`side\-condition`](https://docs.racket-lang.org/redex/Reduction_Relations.html#(idx._(gentag._25._(lib._redex/redex..scrbl))))doesn’t immediately work\. 4. \(Easy\.\)Prove that this model is deterministic \(confluent\): For all expressions`e`,`e′`, and`e″`, if`e→e′`and`e→e″`then`e′=e″`\.