# Introduction

Now that I have the
mathematical definition of
substitution,
I can implement it. For ease of implementation, I will not consider *call by
name* substitution which requires alpha-conversion. I will implement *call by
value*, which is what most familiar programming languages use, such as Python,
Ruby, PHP, C, Perl, and Java to name a few.

# Substitution: Recursive Definition with Alpha Conversion

```
# Replace all free occurrences of x in x with s
[x ↦ s]x = s
# Replace all free occurrences of x in y with s
[x ↦ s]y = y if x ≠ y
# Replace all free occurrences of x in λy.t1 with s
[x ↦ s](λy.t1) = λy.[x ↦ s]t1 if y ≠ x and y ∉ FV(s)
# Replace all free occurrences of x in t1 t2 with s
[x ↦ s](t1 t2) = ([x ↦ s]t1)([x ↦ s]t2)
```

# Strategy

I basically have four things to consider when substituting in *call by value*:
* If the term is in the form `[x ↦ s]x`

, return the *value* `s`

* If the term is in the form `[x ↦ s]y`

, return the *term* `y`

, since `x ≠ y`

* If the term is in the form `[x ↦ s](λy.t1)`

, return the substituted *abstraction* `λy.[x ↦ s]t1`

* If the term is in the form `[x ↦ s](t1 t2)`

, return the application where each term is substituted `([x ↦ s]t1)([x ↦ s]t2)`

There are three parts to every substitution: term, variable, and value.
So I will need them as parameters to my function; I’ll call them `term var value`

.
In mathematical format, you can think of it like this: `[var ↦ value]term`

.

# Implementation in Racket

Using a functional language, like Racket, allows us a more powerful, terse, and
elegant solution to the substitution function. I employ the use of Racket’s
`match`

which gives extremely powerful pattern
matching.

```
(define (subst term var value)
(match term
; [x -> s]y -> y = x ? s : y
[(? symbol?) (if (eq? term var) value term)]
; [x -> s]λx.b -> λx.b
; [x -> s]λy.b -> λy.[x -> s]b
[`(λ (,v) ,body) (if (eq? v var) term `(λ (,v) ,(subst body var value)))]
; [x -> s](t1 t2)
[`(,f ,a) `(,(subst f var value) ,(subst a var value))]))
```

# Tests

```
> (subst `(λ (x) 'y) 'y '1)
'(λ (x) (1))
> (subst `(λ (x) 'y) 'y `(λ (x) 'z))
'(λ (x) ((λ (x) 'z)))
> (subst `((λ (x) y) (λ (y) z)) 'z '2)
'((λ (y) 2))
> (subst `((λ (x) y) (λ (y) z)) 'y '2)
'((λ (y) z))
```