Sunday, May 20, 2007

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
[(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
[(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))])
(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.

No comments: