exercises.rkt

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

;; A "reduction sequence" is a sequence of λ-calculus terms,
;; each of which follows from the previous via a reduction (either
;; α, β, or η).
;;
;; Write the "call-by-value" reduction sequence for the following
;; expression:
;; 
;; ((λ (x) y) ((λ (z) z) (λ (a) a)))
;; -->β ((λ (x) y) (λ (a) a))
;; -->β y
;;
;; Write the "call-by-name" reduction sequence for the above expression:
;;
;; ((λ (x) y) ((λ (z) z) (λ (a) a)))
;; -->β y [ x -> ((λ (z) z) (λ (a) a)) ] = y

;; Write the call-by-value and call-by-name reduction sequences for the following

(((λ (x) x) (λ (y) y))
 ((λ (z) z) (λ (a) a)))

;; Exercise 5: Call-By-Value reduction sequence for above expr

;;(((λ (x) x) (λ (y) y))
;; ((λ (z) z) (λ (a) a)))
;;-->β
;; ((λ (y) y)
;; ((λ (z) z) (λ (a) a)))
;;-->β
;;((λ (y) y)
;; (λ (a) a))
;;-->β
;;(λ (a) a)

;; Exercise 6: write the call-by-name reduction sequence (to WHNF) for this:
;; ((λ (y) (λ (z) z)) ((λ (x) (x x)) (λ (x) (x x))))
;; -->β (λ (z) z)

;; This term cannot be reduced via CBV, but can trivially be reduced using
;; CBN
;; ((λ (y) (λ (z) z)) ((λ (x) (x x)) (λ (x) (x x))))
;; -->β ((λ (y) (λ (z) z)) ((λ (x) (x x)) (λ (x) (x x))))
;; -->β ((λ (y) (λ (z) z)) ((λ (x) (x x)) (λ (x) (x x))))
;; -->β ((λ (y) (λ (z) z)) ((λ (x) (x x)) (λ (x) (x x))))
;; -->β ...