eighty-twenty

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

• Part I: The Functional Fragment: ISWIM in Redex
• Part II: The Communicating Fragment: Actors in Redex
• Part III: Efficiency vs. Nondeterminism

This post is written as a literate Racket source file, and is licensed CC-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 is a programming language gedankenexperiment invented by Peter Landin in his famous paper, “The Next 700 Programming Languages”.³ 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.⁴

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 6 7 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”.⁸ 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,⁹ 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.

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 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 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, 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, 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, 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 as a side-condition 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″.

References and Footnotes