The OO dream?

Signed message-passing! Multi-language, multi-implementation services! Actor-based distributed computation! Is this the OO dream?

[A] portable implementation of Termite is underway. ... The implementation will also support signed message passing... [A] system will only be able to receive messages from trusted sources... Will this be a way to re-unite the Scheme community? Is it a better approach than providing a common package infrastructure?

From Dominique Boucher. Heady stuff. The mind reels at the possibilities. We'll see.

Capture-avoiding substitution in PLT Redex, Part 2

Following up on yesterday's post, there's another way to specify capture-avoiding substitution that has a convenient representation in Scheme. In the last decade, Pitts and Gabbay have built a research program on reasoning about binding using an algebra of names with name-swapping as their fundamental operation. The notation

(a b) ⋅ x

means roughly "swap occurrences of names a and b in the term x". This is very easy to code in a general way using S-expressions:

(define-metafunction swap
  lambda-calculus
  [(x_1 x_2 x_1) x_2]
  [(x_1 x_2 x_2) x_1]
  [(x_1 x_2 (any_1 ...)) ((swap (x_1 x_2 any_1)) ...)]
  [(x_1 x_2 any_1) any_1])

The new definition of subst is very similar to the one I posted yesterday, except instead of using change-variable it uses swap:

(define-metafunction subst
  lambda-calculus
  [(x_1 e_1 (lambda (x_1) e_2))
   (lambda (x_1) e_2)]
  [(x_1 e_1 (lambda (x_2) e_2))
   ,(term-let ([x_new (variable-not-in (term e_1) (term x_2))])
      (term
       (lambda (x_new)
         (subst (x_1 e_1 (swap (x_2 x_new e_2)))))))]
  [(x_1 e_1 x_1) e_1]
  [(x_1 e_1 x_2) x_2]
  [(x_1 e_1 (e_2 e_3))
   ((subst (x_1 e_1 e_2)) (subst (x_1 e_1 e_3)))])

This corresponds to Pitts and Gabbay's definition of capture-avoiding substitution.

The cool thing about swap is that its definition doesn't have to change as you add new expression forms to your language; it's completely oblivious to the binding structure of the expression, and in a sense to any of the structure of the expression. All it needs is the ability to visit every node in the tree. So S-expressions as a term representation and swap as a variable-freshening operation fit together very nicely to form a convenient implementation of capture-avoiding substitution in PLT Redex.

Capture-avoiding substitution in PLT Redex

There are lots of ways to implement substitution in PLT Redex (an embedded DSL in PLT Scheme for defining operational semantics with rewrite rules and evaluation contexts). I'll demonstrate with the lambda calculus, of course:

(define lambda-calculus
  (language
   [e (e e) x v]
   [v (lambda (x) e)]
   [x (variable-except lambda)]))

Since the early days, Redex has come with a library for building capture-avoiding substitution functions called subst. It's a little awkward to work with, though. Here's a definition of substitution using subst:

;; lc-subst : variable × expression × expression → expression
(define lc-subst
  (subst
   [`(lambda (,x) ,body)
    (all-vars (list x))
    (build (lambda (vars body) `(lambda ,vars ,body)))
    (subterm (list x) body)]
   [(? symbol?) (variable)]
   [`(,e1 ,e2)
    (all-vars '())
    (build (lambda (vars e1 e2) `(,e1 ,e2)))
    (subterm '() e1)
    (subterm '() e2)]))

The subst special form relies on the subform all-vars to list the bound variables of an expression. The build subform reconstructs an expression from its pieces, including the variables (potentially automatically freshened to avoid capture) and the subexpressions. Then the subterm subform identifies each subexpression and lists the bound variables in scope for the subexpression.

This requires a fair amount of work for the client to coax subst into automatically substituting or freshening bound variables. These days, the authors recommend directly implementing capture-avoiding substitution. The example on the Redex web site gives a definition of capture-avoiding substitution as a metafunction:

;; subst : variable × expression × expression → expression
(define-metafunction subst
  lambda-calculus
  ;; 1. x_1 bound, so don't continue in lambda body
  [(x_1 e_1 (lambda (x_1) e_2))
   (lambda (x_1) e_2)]
  ;; 2. in this case, we know that no capture can occur,
  ;; so it is safe to recur normally.
  [(x_1 e_1 (lambda (x_2) e_2))
   (lambda (x_2) (subst (x_1 e_1 e_2)))
   (side-condition
    (equal? (variable-not-in (term e_1) (term x_2))
            (term x_2)))]
  ;; 3. general purpose capture avoiding case
  [(x_1 e_1 (lambda (x_2) e_2))
   ,(term-let ([x_new (variable-not-in (term (x_1 e_1 e_2))
                                       (term x_2))])
              (term
               (lambda (x_new)
                 (subst (x_1 e_1 (subst (x_2 x_new e_2)))))))]
  ;; 4. replace x_1 with e_1
  [(x_1 e_1 x_1) e_1]
  ;; 5. x_1 and x_2 are different, so don't replace
  [(x_1 e_1 x_2) x_2]
  ;; 6. ordinary recursive case
  [(x_1 e_1 (e_2 e_3))
   ((subst (x_1 e_1 e_2)) (subst (x_1 e_1 e_3)))])

This implements capture-avoiding substitution with Redex's new define-metafunction form. Redex's term macro is a quasiquote-like data constructor that produces S-expressions; define-metafunction defines implicitly unquoted functions that can be invoked within a term form. The subst metafunction substitutes an expression e_1 for a variable x_1 within an expression e_2 by applying

(subst (x_1 e_1 e_2))

within a term form.

This metafunction is correct, but I find its definition a little subtle. I think it's clearer to separate concerns a little more and divide its definition into two pieces. Following Gunter's definition of capture-avoiding substitution we define a separate "change of variable" function:

;; change-variable : variable × variable × expression → expression
(define-metafunction change-variable
  lambda-calculus
  [(x_1 x_2 x_1) x_2]
  [(x_1 x_2 x_3) x_3]
  [(x_1 x_2 (lambda (x_1) e_1))
   (lambda (x_1) e_1)]
  [(x_1 x_2 (lambda (x_3) e_1))
   (lambda (x_3) (change-variable (x_1 x_2 e_1)))]
  [(x_1 x_2 (e_1 e_2))
   ((change-variable (x_1 x_2 e_1)) (change-variable (x_1 x_2 e_2)))])

This function replaces a variable name x_1 with a new name x_2 within an expression e_1. The subst metafunction uses change-variable for renaming a bound variable with a fresh name.

;; subst : variable × expression × expression → expression
(define-metafunction subst
  lambda-calculus
  [(x_1 e_1 (lambda (x_1) e_2))
   (lambda (x_1) e_2)]
  [(x_1 e_1 (lambda (x_2) e_2))
   ,(term-let ([x_new (variable-not-in (term e_1) (term x_2))])
      (term
       (lambda (x_new)
         (subst (x_1 e_1 (change-variable (x_2 x_new e_2)))))))]
  [(x_1 e_1 x_1) e_1]
  [(x_1 e_1 x_2) x_2]
  [(x_1 e_1 (e_2 e_3))
   ((subst (x_1 e_1 e_2)) (subst (x_1 e_1 e_3)))])

I prefer this definition of capture-avoiding substitution for several reasons. First, it corresponds directly to Gunter's definition. Furthermore, its runtime efficiency is a little clearer. The first definition of the metafunction recursively calls itself twice on the same subexpression in case #3; the reason why this doesn't cause exponential growth is because its behavior in one of the two cases is equivalent to change-variable (because it substitutes a variable) and consequently more efficient. But this took me a while to figure out. Finally, the types are a little tighter. For example, if we were just defining call-by-value substitution, subst could take a value for its second argument, rather than arbitrary expressions.

Food for thought from Robert O'Callahan

Robert O'Callahan, former CMUer and current Mozilla hacker extraordinaire, has a couple thoughts on research directions for PL:

I also suggested that the worst code is not necessarily buggy code, but code that is unnecessarily complex. Detecting that would be an interesting new direction for program analysis.

And also:

...[T]he state of parallel programming models, languages and tools remains pathetic for general-purpose single-user programs and no breakthrough should be expected. My position is that for regular desktop software to scale to 32 cores by 2011 (as roadmaps predict) we'd have to rewrite everything above the kernel, starting today, using some parallel programming model that doesn't suck. Since that model doesn't exist, it's already too late. Probably we will scale out to a handful of cores, with some opportunistic task or data parallelism, and then hit Amdahl's law, hard. It is probably therefore more fruitful to focus on new kinds of applications which we think we have reasonable ideas for parallelizing. I think virtual worlds (which are not just "games", people!) are a prime candidate. That's a direction I think the PL/software engineering research community should be pushing in.