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.

HOAS vs. Nominal Logic

I don't yet have a deep understanding in the debate between higher-order abstract syntax and nominal logic, but this is an interesting summary from Karl Crary and Bob Harper in a short article in the Logic Column for SIGACT News:

“The real contrast between HOAS and nominal logic lies in their philosophy toward binding structure. Both HOAS and nominal logic provide a sophisticated treatment of binding structure not enjoyed by first-order accounts, but ones of very different character. The philosophy of LF is that binding and alpha-conversion are fundamental concepts, and thus builds them in at the lowest level. Consequently, name management in LF is ordinarily a non-issue. In contrast, nominal logic promotes name management as an object of study. It makes binding into a sophisticated artifact, rather than a primitive concept as in LF.”