## Introduction

Two of the most common forms of reduction are *Call-By-Name* (CBN) and
*Call-By-Value* (CBV), with the latter being the most ubiquitous. In this post,
I give implement both in Racket.

## Mathematical Definitions

### Non Deterministic Full ß-reduction
This is a *non-deterministic*, full ß-reduction definition. Notice that there is
no *value* term definition, that is because a value cannot be a ß-redex. The way
to read the following rules are, the definition on top of the line is the
conditional, on the bottom is what happens if that is true.

###Application In application, there are two scenarios that need to be handled: the left hand and/or right hand terms are ß-redexes.

### Abstraction

If the body of a λ-abstraction is a ß-redex, then reduce it and substitute.

### Application-Abstraction

If we have an abstraction and a term, substitute the term into the body of the abstraction if the free variables in the body match the term.

## ß-reduction Implementation

###Substitution You can see the implementation and theory posts on substitution to get more background. Here is the implementation in Racket:

```
(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) -> [x -> s]t1 [x -> s]t2
[`(,f ,a) `(,(subst f var value) ,(subst a var value))]))
```

### Beta-reduction

Beta-reduction is not *full* beta reduction. We only have one rule to implement,
*abstraction*

```
; (t1 t2)
(define (ß-reduce term)
(match term
[`((λ (,v1) ,b1), (and rhs `(λ (,v2) ,b2))) (subst b1 v1 rhs)]))
```

### Full ß-reduction

```
(define (full-ß-reduce term)
(match term
; value
[(? symbol?) (error "Cannot reduce value" term )]
; identity
[`(λ (,v) ,v) (term)]
; abstraction
[`((λ (,v1) ,b1)(λ (,v2) ,b2)) (ß-reduce term)]
; application
[`((λ (,v1) ,b1), e) (full-ß-reduce e)]
; application-abstraction
[`(,f ,e) (full-ß-reduce f)]))
```

## Tests

###Beta-Reduce Tests

```
;(ß-reduce `((λ(x) (x x))(λ(z) u)))
;'(((λ (z) u)) ((λ (z) u)))
;(ß-reduce `((λ(x)(λ(y) (y x)))(λ(z)u)))
;'(λ (y) (y ((λ (z) u))))
```

### Full ß-reduce Tests

```
;> (full-ß-reduce `((λ(y) (y a))((λ(x)x)(λ(z)((λ(u)u)z)))))
;'((λ (z) ((λ (u) u) z)))
;> (full-ß-reduce `((λ(x)(x x))(λ(x)(x x))))
;'(((λ (x) (x x))) ((λ (x) (x x))))
```