$blog→errstr

do not commit

Reduction

| Comments

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