Modelling Actors with Redex: Part I (eighty-twenty news)

eighty-twenty

about |<br>sitemap

-->

This is the first part of a series of three articles on modelling<br>actor-like systems,1 2 similar to<br>Erlang and to my own work on<br>Syndicate, using PLT<br>Redex, “a domain-specific<br>language designed for specifying and debugging operational<br>semantics.”

Part I: The Functional Fragment: ISWIM in Redex

Part II: The Communicating Fragment: Actors in Redex

Part III: Efficiency vs. Nondeterminism

This post<br>is written as a literate Racket source file, and is licensed CC-BY<br>4.0. You can download it<br>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<br>allows you to interactively explore terms and to use randomized<br>test generation to attempt to falsify properties of your<br>semantics.

In this post, I’ll build a model of a simple “ISWIM”-style,<br>lambda-calculus based functional programming language. In<br>subsequent posts, I’ll extend this little model to build it into<br>an Erlang-style actor system.

Here’s an example program in the language:

((rec loop (lambda (count)<br>(if (= count 0)<br>nil<br>(cons count (loop (- count 1)))))) 3)

And here’s a screenshot of the Redex trace visualizer showing<br>reductions of the program:

Preliminaries

ISWIM is a programming<br>language gedankenexperiment invented by Peter Landin in his<br>famous paper, “The Next 700 Programming Languages”.3 It<br>is essentially a Scheme-like language; a fairly minimal extension<br>of the lambda calculus.

Our model will be an ISWIM-like language supporting S-expressions,<br>numbers, strings, and booleans.

First of all, we need the Racket #lang header:

#lang racket

(provide ISWIM<br>ISWIM-red<br>delta<br>subst-all)

-->

Next, we load Redex.

(require redex)

(require redex/reduction-semantics) ;; to avoid needing to load the GUI stuff, for headless use

-->

Syntax

We begin by declaring the (S-expression-based) syntax we will use<br>for programs written in our language.

(define-language ISWIM

Expressions, Values and Variables

Our first nonterminal is expr, syntax for expressions in our<br>language. An expression can be any of the following options:

(expr x ;; a variable reference<br>value ;; a value (see below)<br>(cons expr expr) ;; the construction of a pair<br>(expr expr ...) ;; a function call<br>(prim expr ...) ;; a primitive operation call<br>(begin expr ...) ;; a sequence of expressions<br>(if expr expr expr) ;; a conditional<br>(rec x expr)) ;; a recursive expression

Notice the lack of imperative constructions. When we get to Part<br>II, we’ll add some imperative commands, like “send message”.

Despite this lack, we still let programs written in this language<br>use begin, because it is more ISWIM-ish than specifically<br>Actors-ish, and it will be useful later.4

Values, value, in our language can be any of the following:

(value (lambda (x ...) expr ...) ;; a literal function<br>number ;; a literal number<br>string ;; a literal string<br>boolean ;; a literal boolean<br>nil ;; the special value `nil`<br>(cons value value)) ;; a constructed pair of values

We’re playing an interesting trick here, letting the cons<br>constructor serve as both an expression and as a value.<br>Once both arguments to cons have been reduced to values,<br>the whole piece of syntax represents the final pair.

We let the syntactic nonterminal x stand for variables in our<br>language:

(x variable-not-otherwise-mentioned)

Evaluation Contexts and Primitive Operators

Our model uses the idea of evaluation contexts invented by<br>Felleisen et al. in 1986.5 6 7<br>An evaluation context is a term with a hole in it. The hole is,<br>roughly, the position in the term where some reduction can happen:<br>where a redex is waiting to be reduced.

This definition of evaluation contexts forces evaluation of<br>function arguments to happen in left-to-right order.

(context hole<br>(value ... context expr ...)<br>(prim value ... context expr ...)<br>(cons context expr)<br>(cons value context)<br>(begin context expr expr ...)<br>(if context expr expr))

We define a small set of primitive operators for manipulating data<br>in our language. Other operators can be added by extending the<br>definition of the prim nonterminal and by adding clauses to the<br>metafunction delta below.

(prim + - = car cdr pair? null?)

Binding structure of the language

I first learned Redex by taking a course based on “Semantics<br>Engineering with PLT Redex”.8 An important part of<br>programming with Redex at the time was implementing substitution<br>functions correctly, respecting the binding structure of the<br>language. This was a difficult, error-prone and annoying part of<br>using the system.

Since then, Paul Stansifer has completed his dissertation<br>work,9 and as a result, Redex programmers can specify<br>a language’s binding structure directly as part of the syntax,<br>meaning that substitution and alpha-equivalence functions can be<br>automatically produced by the system.

We no longer have to write substitution functions by hand!

Here, to make use of Paul’s...