10-19.rkt

#lang racket

;; omega term = 
;; ((lambda (x) (x x)) (lambda (x) (x x)))
;; (x x) [ x ↦ (lambda (x) (x x)) ] =
;; ((lambda (x) (x x)) (lambda (x) (x x)))

;; there are two options
'((lambda (x) (lambda (y) y)) ((lambda (x) (x x)) (lambda (x) (x x))))

;; A few examples for β reeduction

;; Perform every possible "one-step" β reduction for the following:
;; this term has two "β redexes" (reducible expression...)
;; ((λ (x) (x y)) ((λ (z) z) (λ (x) k)))
;; the "outer" one
;; ⟶β 
;; (x y) [ x ↦ ((λ (z) z) (λ (x) k)) ]
;; = (((λ (z) z) (λ (x) k)) y)
;; if I keep reducing..
;; ⟶β ((λ (x) k) y)
;; ⟶β k

;; The "inner" one
;; ⟶β
;; ((λ (x) (x y)) (λ (x) k))
;; ⟶β
;; ((λ (x) k) y)
;; ⟶β
;; k

;; A "reduction sequence" is a sequence of reductions, each which follows from
;; the previous one...

;; Let's say I have the λ-calculus expression

((λ (add1) (add1 5)) (λ (x) x)) ;; 5

;; What are the free variables for this expression
'((λ (x) (λ (y) (z (x y)))) x)
;; { x, z }

;; Translate the math from the slides into racket
(define (free-vars e)
  (match e
    [(? symbol? x) (set x)]
    [`(λ (,x) ,e) (set-remove (free-vars e) x)] ;; use set-remove
    [`(,e0 ,e1) (set-union (free-vars e0) (free-vars e1))]))


(define f add1)
(define f (lambda (x) (add1 x)))

;; X (lambda (x) (lambda (y) (z))) -- NO -- not a λ calculus term
;; O ((lambda (z) (z (lambda (y) (y k)))) (lambda (x) x)) -- OK 
;; X (lambda (x) (lambda (y) (x y y))) -- NO -- (x y y) not in λcalculus

;; ((λ (x) (x x)) (λ (z) (λ (y) y)))
;; ⟶β
;; ((λ (z) (λ (y) y)) (λ (z) (λ (y) y)))
;; ⟶β
;; (λ (y) y)
;; we're done 

;; after α-conversion of first x to y
((λ (y) (y y)) (λ (z) (λ (y) y)))