lambda-exercises.txt

#lang racket

;; λ Calculus Exercises
;; Tue, Oct 25, 2022
;; CIS 352

;; Exercise 1:
;; ((λ (x) x) (λ (y) y))
;; Perform beta reduction on this term
;; For credit: the substitution must be made explicit
;; E0 [ x -> E1 ] for some E0, x, and E1
;; ((λ (x) E0) E1) how to match against the term ^^?
;; x = x
;; E0 = x
;; E1 = (λ (y) y)
;; x [ x -> (λ (y) y) ]
;; =
;; (λ (y) y)

;; Exercise 2:
;; ((λ (x) x) ((λ (z) z) y))
;; Identify two possible β reductions for the above term.
;; x [ x -> ((λ (z) z) y) ]
;; ((λ (z) z) y) #1
;; ((λ (x) x) y) #2

;; Examples of free variables...
;;(λ (x) x) ;; FV( (λ (x) x) ) = {} 
;; (λ (x) (x y)) ;; FV ( (λ (x) (x y)) ) = {y} 
;; y ;; FV ( y ) = {y}
;; (z (λ (z) z)) ;; FV ( (z (λ (z) z)) ) = {z}

;; Exercise 3:
;; - Which variables are free in the following term
;; {z, x}
;; - Which variables are bound somewhere in the term:
;; {x, y}
;; ((λ (x) (x x)) ((λ (y) (λ (x) (x z))) x))

(define (freevars expr)
  (match expr
    [(? symbol? x) (set x)]
    [`(λ (,x) ,e-body) (set-remove (freevars e-body) x)]
    [`(,e0 ,e1) (set-union (freevars e0) (freevars e1))]))

;; ((λ (x) (z x)) (λ (x) ((λ (z) (λ (y) (y z))) z)))

;; Terms like (λ (x) x)
;; are kind of "equivalent" to terms like (λ (y) y), (λ (z) z), ....

(λ (x) (λ (x) x)) ;; when you substitute x inside of this expression,
                  ;; careful not to redefine x

;; Exercise 4
;; β reduce the following expression using capture-avoiding substitution
;;
;; ((λ (y) 
;;    ((λ (z) (λ (y) (z y))) y)) 
;;  (λ (x) x))
;; -->β 
;; ((λ (z) (λ (y) (z y))) (λ (x) x))

;; Exercise 5
;; Give an example of a lambda term for which β-reduction
;; could not occur because it would capture