(a b) ⋅ xmeans 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:

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 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])

This corresponds to Pitts and Gabbay's definition of capture-avoiding substitution.(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)))])

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:

Post a Comment