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.