Lambda calculus basics

10-17.rkt

#lang racket

;; λ-calculus expressions
(define (expr? e)
  (match e
    [(? symbol? x) #t] ;; variables
    [`(λ (,(? symbol? x)) ,(? expr? e-body)) #t] ;; λ abstractions
    [`(,(? expr? e-f) ,(? expr? e-a)) #t] ;; applications
    [_ #f]))


;; Example λ-calculus terms
(expr? '((λ (x) (x x)) y))
(expr? '(λ (z) (z (y x))))
(expr? '(x z))
(expr? '((x ((λ (x) x) x)) (y (λ (z) z))))

;; Here are three applications, which of the following are
;; β redexes ("i.e., β-reducible expression"):
'(x (λ (y) y)) ;; no
'((x y) (y (λ (z) z))) ;; no
'((λ (x) (x x)) (λ (z) z)) ;; yes
;; E0 is (x x) and E1 is (λ (z) z)
;; Thus, it β-reduces to...
;; →β E0 [ x ↦ E1 ]
;; = (x x) [ x ↦ (λ (z) z) ]
'((λ (z) z) (λ (z) z))


(define (substitute E0 x E1) 'todo)

(define (apply-β e)
  (match e
    [`((lambda (,x) ,E0) ,E1)
     ;; have to define substitute
     (substitute E0 x E1)]))


;; β reduce the following
;; I mean: take the top-level application and perform
;; "one step" of β reduction for the term

;; Example 1
;;'((λ (x) (x (x y))) (λ (z) (z x)))
;; By the definition of β reduction
;;-->β (x (x y)) [ x ↦ (λ (z) (z x)) ]
;; (e1) = ((λ (z) (z x)) ((λ (z) (z x)) y))
;;
;; Now, we have two possibilities for β reduction

;; We will see that when you get to a application, you have of two options
;; - You can either use the "applicative" order and
;; "eagerly" reduce the argument until you can't reduce
;; any more. This is called the "call by value" approach, because it attempts
;; to reduce the arguments of λs down to "values" before the application can
;; proceed.
;; - Alternatively ("normal" order), you could "lazily" defer reduction of the argument and
;; instead apply the function right away. This is the "call by name" approach.
;; 
;; If I take the "normal" order decision, I don't reduce the argument...
;; -->β (z x) [z ↦ ((λ (z) (z x)) y) ]
;; = (((λ (z) (z x)) y) x) (e2)
;; -->β ((y x) x)
;; this is in β normal form (i.e., no more possible β reduction)

;;
;; If instead I take the "applicative" order, I get..
;;  ((λ (z) (z x)) (y x)) (e3)
;; -->β ((y x) x)
;; This is also in β normal form


;; Theorem (Church Rosser): if two expressions are equivalent, they give
;; the same β normal form.
;; If e -->β e' and e -->β e'', then there is some e''' such that
;; e' -->*  e''' and e'' -->* e'''

;; Example 2
((λ (z) (z (z z))) (λ (x) (x x)))

;; Three options:
;; (1) Every way of β reducing the term will lead to nontermination
;; (2) Every way of β reducing the term will lead to termination
;; ** (3) Some ways of β reducing will terminate, others will not...

((λ (x) (λ (y) y))
 ((λ (x) (x x)) (λ (x) (x x))))
;; Normal order evaluation / CBN / lazy evaluation gives us...
(λ (y) y) ;; which immediately terminates


; f(x) = 3