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.
### 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.
If the body of a λ-abstraction is a ß-redex, then reduce it and substitute.
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.
(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 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)]))
(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)]))
;(ß-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))))