# 正確實作 substitution 有多難

lambda calculus 有所謂的 substitution，具體來說就是 `((lambda (x) x) y)` 會變成 =y=，但正確實作這個行為到底有多麻煩呢?為什麼我寫這篇廢文: 因為我寫錯了…

```(define (utlc t)
(match t
[`(λ (,x) ,m)
`(λ (,x) ,m)]
[`(,f ,a)
`(,f ,a)]
[`,e `,e]))
```

```(define (utlc t)
(match t
[`(λ (,x) ,m)
`(λ (,x) ,(utlc m))]
[`(,f ,a)
(match (utlc f)
[`(λ (,x) ,m)
(utlc (subst m x a))]
[f1
`(,f1 ,a)])]
[`,e `,e]))
```

```(define (subst t x s)
t)
```

substitute variable v: if v is x, return s, else return v，根據這些已經能寫出來了:

```(define (subst t x s)
(match t
[`,e
(if (equal? `,e `,x)
s
e)]))
```

```(define (subst t x s)
(match t
[`(,e1 ,e2)
`(,(subst e1 x s) ,(subst e2 x s))]
; ...
```

lambda 就是問題的根源，先想想簡單的辦法: 對 lambda 而言，substitution 就是替換其 body:

```(define (subst t x s)
(match t
[`(λ (,i) ,b)
`(λ (,i)
,(subst b x s))]
; ...
```

```(define (subst t x s)
(match t
[`(λ (,i) ,b)
(cond
[(equal? `,i `,x) `,t]
[#t
`(λ (,i)
,(subst b x s))])]
; ...
```

```(define (subst t x s)
(match t
[`(λ (,i) ,b)
(cond
[(equal? `,i `,x) `,t]
[(equal? `,i `,s)
(define fi (gensym `,i))
(define fb (subst b i fi))
`(λ (,fi) ,(subst fb x s))]
; ...
```

Date: 2020-06-04 Thu 00:00