ISWIM with f-expressions.

README.md

Small experiment with ISWIM. I tried to add something like f-expressions, resp. $wau functions.

iswim-wau.rkt

#lang racket
(require redex)

;; ----------------------------------------
;; ISWIM

(define-language ISWIM
  [(M N) B X (λ X M) (M N) (Op1 M) (Op2 M N)
         (if0 M N_1 N_2) (let ([X N]) M) ($wau X M)] ;; Exercise 1

  [B integer]
  [(X Y Z) variable-not-otherwise-mentioned]
  [Op Op1 Op2]
  [Op1 add1 sub1 iszero]
  [Op2 + *]

  [(VN WN) B X (λ X M) ($wau X M)]
  
  [(V W) B X (λ X M)]

  [C hole (λ X C) (C N) (M C) (Op1 C) (Op2 C N) (Op2 M C)
     (if0 C N_1 N_2) (if0 M C N) (if0 M N C) ;; Exercise 1: if0
     ($wau X C) ]

  [Answer B function]

  ;; Standard reduction:
  [E hole (E N) (V E) (Op1 E) (Op2 E N) (Op2 V E) (if0 E N_1 N_2)] ;; Exercise 1: if0

  [EN hole (EN N) (VN EN) (Op1 EN) (Op2 EN N) (Op2 VN EN) (if0 EN N_1 N_2)] ;; Call by name context

  ;; CC machine:
  [CC-config (cc M E)]

  ;; SCC machine:
  [SCC-config (scc M E)]

  ;; CK machine:
  [CK-config (ck M Kck)]
  [Kck mt (fn VN Kck) (ar N Kck) (op Op (VN ...) (N ...) Kck) (if0 N_1 N_2 Kck)] ;; Exercise 1: if0

  ;; CEK machine:
  [CEK-config (cek CM Kcek)]
  [(CM CN) (closure M Env) (closure (thunk* M) Env)]
  [(CV CW) (closure B Env) (closure (λ X M) Env) (closure ($wau X M) Env) (closure (thunk* M) Env)]
  [Env empty (extend Env X CN)] ;; changed CV -> CN because we can close $wau functions
  [Kcek mt (fn CV Kcek) (ar CN Kcek) (op Op (CV ...) (CN ...) Kcek) (if0 N_1 N_2 Env Kcek)]) ;; Exercise 1: if0
;;                                                                  ^ I don't need to close both branches, I can keep the Env for them and close it later

;; ----------------------------------------
;; Free variables and substitution

(define-judgment-form ISWIM
  #:mode (free-in I I)
  #:contract (free-in X M)

  [---------------------------------------- "free-in-var"
   (free-in X X)]

  [(free-in X M)
   (side-condition ,(not (equal? (term X) (term Y))))
   ---------------------------------------- "free-in-λ"
   (free-in X (λ Y M))]

  [(free-in X M)
   (side-condition ,(not (equal? (term X) (term Y))))
   ---------------------------------------- "free-in-$wau"
   (free-in X ($wau Y M))]

  [(free-in X M_1)
   ---------------------------------------- "free-in-app1"
   (free-in X (M_1 M_2))]

  [(free-in X M_2)
   ---------------------------------------- "free-in-app2"
   (free-in X (M_1 M_2))]

  [(free-in X M)
   ---------------------------------------- "free-in-op1"
   (free-in X (Op1 M))]

  [(free-in X M_1)
   ---------------------------------------- "free-in-op2-1"
   (free-in X (Op2 M_1 M_2))]

  [(free-in X M_2)
   ---------------------------------------- "free-in-op2-2"
   (free-in X (Op2 M_1 M_2))]

  ;; Exercise 1: if0
  [(free-in X M)
   ---------------------------------------- "free-in-if0-condition"
   (free-in X (if0 M N_1 N_2))]

  ;; Exercise 1: if0
  [(free-in X N_1)
   ---------------------------------------- "free-in-if0-then"
   (free-in X (if0 M N_1 N_2))]

  ;; Exercise 1: if0
  [(free-in X N_2)
   ---------------------------------------- "free-in-if0-else"
   (free-in X (if0 M N_1 N_2))]
  )

(module+ test
  (test-judgment-holds (free-in x (λ y (y x))))
  (test-equal (judgment-holds (free-in x (λ x x))) #f))

(define-metafunction ISWIM
  subst : X N M -> M ;; M[X <- N]

  [(subst X N B) B]

  [(subst X N X) N]
  [(subst X N Y) Y] ;; X ≠ Y, otherwise previous case matches

  [(subst X N (λ X M))
   (λ X M)]

  ;; ** Do we still need the following case? **
  [(subst X N (λ Y M)) ;; X ≠ Y, otherwise previous case matches
   (λ Z (subst X N (subst Y Z M)))
   (judgment-holds (free-in Y N))
   (where Z ,(variable-not-in (term (X N)) (term Y)))]

  [(subst X N (λ Y M)) ;; X ≠ Y, Y ∉ FV(N), otherwise previous case matches
   (λ Y (subst X N M))]

  [(subst X N ($wau X M))
   ($wau X M)]

  ;; ** Do we still need the following case? **
  [(subst X N ($wau Y M)) ;; X ≠ Y, otherwise previous case matches
   ($wau Z (subst X N (subst Y Z M)))
   (judgment-holds (free-in Y N))
   (where Z ,(variable-not-in (term (X N)) (term Y)))]

  [(subst X N ($wau Y M)) ;; X ≠ Y, Y ∉ FV(N), otherwise previous case matches
   ($wau Y (subst X N M))]

  [(subst X N (M_1 M_2))
   ((subst X N M_1) (subst X N M_2))]

  [(subst X N (Op1 M))
   (Op1 (subst X N M))]

  [(subst X N (Op2 M_1 M_2))
   (Op2 (subst X N M_1) (subst X N M_2))]

  ;; Exercise 1: if0
  [(subst X N (if0 M N_1 N_2))
   (if0 (subst X N M) (subst X N N_1) (subst X N N_2))]
  )

(module+ test
  (test-equal (term (subst x y x))
              (term y))
  (test-equal (term (subst x (λ y y) (λ z (x z))))
              (term (λ z ((λ y y) z))))
  (test-equal (term (subst x 5 (add1 (+ x (* 2 y)))))
              (term (add1 (+ 5 (* 2 y)))))
  ;; The following test depends on how variable-not-in picks the fresh
  ;; variable name (z1 in this example):
  (test-equal (term (subst x (y z) (λ z (x z))))
              (term (λ z1 ((y z) z1)))))

;; ----------------------------------------
;; Reduction

(define beta-v
  (reduction-relation
   ISWIM
   (--> ((λ X M) V)
        (subst X V M))))

(define beta-wau
  (reduction-relation
   ISWIM
   (--> (($wau X M) N)
        (subst X N M))))

(define delta
  (reduction-relation
   ISWIM
   (--> (add1 B) ,(add1 (term B)))
   (--> (sub1 B) ,(sub1 (term B)))
   (--> (iszero 0) (λ x (λ y x)))
   (--> (iszero B) (λ x (λ y y)) (side-condition (not (zero? (term B)))))
   (--> (+ B_1 B_2) ,(+ (term B_1) (term B_2)))
   (--> (* B_1 B_2) ,(* (term B_1) (term B_2)))))

(define delta-if
  (reduction-relation
   ISWIM
   (--> (if0 0 N_1 N_2) N_1) ;; Exercise 1
   (--> (if0 B N_1 N_2) N_2 (side-condition (not (zero? (term B))))))) ;; Exercise 1
   

(define v-reduce (union-reduction-relations beta-v delta delta-if beta-wau))

(define :-->v (context-closure v-reduce ISWIM E))

(module+ test
  (test--> :-->v (term (* (+ 1 2) (+ 2 3)))
           (term (* 3 (+ 2 3))))
  (test--> :-->v (term ((λ x (+ 2 x)) (+ 3 4)))
           (term ((λ x (+ 2 x)) 7)))
  (test--> :-->v (term ((λ x (+ 2 x)) 7))
           (term (+ 2 7)))
  (test--> :-->v (term (if0 0 23 7))
           (term 23))

  (test--> :-->v (term (($wau x x) (+ 2 3)))
           (term (+ 2 3)))
  )

;; ----------------------------------------
;; Example term

(define the-term (term ((λ a (+ 1 (* (+ 2 a) 3))) (+ 4 5))))

(define wow-term (term (($wau x (+ x 3)) (+ 2 3))))

;; ----------------------------------------
;; CC machine

(define-metafunction ISWIM
  is-value? : M -> boolean
  [(is-value? VN) #t]
  [(is-value? _) #f])

(define-metafunction ISWIM
  not-wau? : M -> boolean
  [(not-wau? ($wau X M)) #f]
  [(not-wau? _) #t])


#;(define :-->ccvau
  (reduction-relation
   ISWIM
   #:domain CC-config

   (--> (cc (($wau X M) N) E)
        (cc (subst X N M) E))
   ;; FEXPR
   ))

(define :-->cc
  (reduction-relation
   ISWIM
   #:domain CC-config
   (--> (cc (M N) E)
        (cc M (in-hole E (hole N)))
        (where #f (is-value? M)))

   (--> (cc (VN N) E)
        (cc N (in-hole E (VN hole)))
        (where #f (is-value? N))
        (where #t (not-wau? VN)))
   (--> (cc ((λ X M) VN) E)
        (cc (subst X VN M) E))

   (--> (cc (($wau X M) N) E)
        (cc (subst X N M) E))
   ;; FEXPR

   (--> (cc (Op1 M) E)
        (cc M (in-hole E (Op1 hole)))
        (where #f (is-value? M)))
   (--> (cc (Op1 B) E)
        (cc VN E)
        (where (VN) ,(apply-reduction-relation delta (term (Op1 B)))))

   (--> (cc (Op2 M N) E)
        (cc M (in-hole E (Op2 hole N)))
        (where #f (is-value? M)))
   (--> (cc (Op2 VN N) E)
        (cc N (in-hole E (Op2 VN hole)))
        (where #f (is-value? N)))
   (--> (cc (Op2 B_1 B_2) E)
        (cc VN E)
        (where (VN) ,(apply-reduction-relation delta (term (Op2 B_1 B_2)))))

   ;; Exercise 1: if0
   (--> (cc (if0 M N_1 N_2) E)
        (cc M (in-hole E (if0 hole N_1 N_2)))
        (where #f (is-value? M)))
   (--> (cc (if0 B N_1 N_2) E)
        (cc N E)
        (where (N) ,(apply-reduction-relation delta-if (term (if0 B N_1 N_2)))))

   (--> (cc VN (in-hole E (hole N)))
        (cc (VN N) E))
   (--> (cc VN (in-hole E (WN hole)))
        (cc (WN VN) E))
   (--> (cc VN (in-hole E (Op1 hole)))
        (cc (Op1 VN) E))
   (--> (cc VN (in-hole E (Op2 hole N)))
        (cc (Op2 VN N) E))
   (--> (cc VN (in-hole E (Op2 WN hole)))
        (cc (Op2 WN VN) E))
   (--> (cc VN (in-hole E (if0 hole N_1 N_2)))
        (cc (if0 VN N_1 N_2) E))))

(module+ test
  (test--> :-->cc (term (cc (* (+ 1 2) (+ 2 3)) hole))
           (term (cc (+ 1 2) (* hole (+ 2 3)))))
  (test--> :-->cc (term (cc (+ 1 2) (* hole (+ 2 3))))
           (term (cc 3 (* hole (+ 2 3)))))
  (test--> :-->cc (term (cc ((λ x (+ 2 x)) 7) hole))
           (term (cc (+ 2 7) hole)))

  (test--> :-->cc (term (cc (($wau x (+ 2 x)) (+ 2 3)) hole))
           (term (cc (+ 2 (+ 2 3)) hole)))

)

;; ----------------------------------------
;; SCC machine

(define :-->scc
  (reduction-relation
   ISWIM
   #:domain SCC-config
   (--> (scc (M N) E)
        (scc M (in-hole E (hole N))))

   (--> (scc ($wau X M) (in-hole E (hole N)))
        (scc (subst X N M) E))

   (--> (scc VN (in-hole E (hole N)))
        (scc N (in-hole E (VN hole)))
        (where #t (not-wau? VN)))
   (--> (scc VN (in-hole E ((λ X M) hole)))
        (scc (subst X VN M) E))

   (--> (scc (Op1 M) E)
        (scc M (in-hole E (Op1 hole))))
   (--> (scc B (in-hole E (Op1 hole)))
        (scc VN E)
        (where (VN) ,(apply-reduction-relation delta (term (Op1 B)))))

   (--> (scc (Op2 M N) E)
        (scc M (in-hole E (Op2 hole N))))
   (--> (scc VN (in-hole E (Op2 hole N)))
        (scc N (in-hole E (Op2 VN hole))))
   (--> (scc B_2 (in-hole E (Op2 B_1 hole)))
        (scc VN E)
        (where (VN) ,(apply-reduction-relation delta (term (Op2 B_1 B_2)))))

   ;; Exercise 1: if0
   (--> (scc (if0 M N_1 N_2) E)
        (scc M (in-hole E (if0 hole N_1 N_2))))
   (--> (scc B (in-hole E (if0 hole N_1 N_2)))
        (scc N E)
        (where (N) ,(apply-reduction-relation delta-if (term (if0 B N_1 N_2)))))))

(module+ test
  (test--> :-->scc (term (scc (* (+ 1 2) (+ 2 3)) hole))
           (term (scc (+ 1 2) (* hole (+ 2 3)))))
  (test--> :-->scc (term (scc (+ 1 2) (* hole (+ 2 3))))
           (term (scc 1 (* (+ hole 2) (+ 2 3)))))
  (test--> :-->scc (term (scc 2 (* (+ 1 hole) (+ 2 3))))
           (term (scc 3 (* hole (+ 2 3)))))
  (test--> :-->scc (term (scc (($wau x (+ 2 x)) (+ 2 3)) hole))
           (term (scc ($wau x (+ 2 x)) (hole (+ 2 3)))))
  (test--> :-->scc (term (scc ($wau x (+ 2 x)) (hole (+ 2 3))))
           (term (scc (+ 2 (+ 2 3)) hole)))
  )

;; ----------------------------------------
;; CK machine

(define :-->ck
  (reduction-relation
   ISWIM
   #:domain CK-config
   (--> (ck (M N) Kck)
        (ck M (ar N Kck)))

   (--> (ck ($wau X M) (ar N Kck))
        (ck (subst X N M) Kck))
   
   (--> (ck VN (ar N Kck))
        (ck N (fn VN Kck))
        (where #t (not-wau? VN)))
   (--> (ck VN (fn (λ X M) Kck))
        (ck (subst X VN M) Kck))

   (--> (ck (Op1 M) Kck)
        (ck M (op Op1 () () Kck)))
   (--> (ck B (op Op1 () () Kck))
        (ck VN Kck)
        (where (VN) ,(apply-reduction-relation delta (term (Op1 B)))))

   (--> (ck (Op2 M N) Kck)
        (ck M (op Op2 () (N) Kck)))
   (--> (ck VN (op Op2 () (N) Kck))
        (ck N (op Op2 (VN) () Kck)))
   (--> (ck B_2 (op Op2 (B_1) () Kck))
        (ck VN Kck)
        (where (VN) ,(apply-reduction-relation delta (term (Op2 B_1 B_2)))))

   ;; Exercise 1: if0
   (--> (ck (if0 M N_1 N_2) Kck)
        (ck M (if0 N_1 N_2 Kck)))
   (--> (ck B (if0 N_1 N_2 Kck))
        (ck N Kck)
        (where (N) ,(apply-reduction-relation delta-if (term (if0 B N_1 N_2)))))))

(module+ test
  (test--> :-->ck (term (ck (* (+ 1 2) (+ 2 3)) mt))
           (term (ck (+ 1 2) (op * () ((+ 2 3)) mt))))
  (test--> :-->ck (term (ck (+ 1 2) (op * () ((+ 2 3)) mt)))
           (term (ck 1 (op + () (2) (op * () ((+ 2 3)) mt)))))
  (test--> :-->ck (term (ck 2 (op + (1) () (op * () ((+ 2 3)) mt))))
           (term (ck 3 (op * () ((+ 2 3)) mt))))
  (test--> :-->ck (term (ck (($wau x (+ x 2)) (+ 2 3)) mt))
           (term (ck ($wau x (+ x 2)) (ar (+ 2 3) mt))))
  (test--> :-->ck (term (ck ($wau x (+ x 2)) (ar (+ 2 3) mt)))
           (term (ck (+ (+ 2 3) 2) mt)))
  )

;; ----------------------------------------
;; CEK machine

(define-metafunction ISWIM
  lookup : Env X -> CV ;; CV -> CV :: FEXPR
  [(lookup (extend Env X CV) X) CV] ;; CV -> CV :: FEXPR
  [(lookup (extend Env X CV) Y) (lookup Env Y)]) ;; CV -> CV :: FEXPR

(define-metafunction ISWIM
  not-closed-wau? : CM -> boolean
  [(not-closed-wau? (closure ($wau X M) Env)) #f]
  [(not-closed-wau? _) #t])

(define-metafunction ISWIM
  not-closed-thunk* : CM -> boolean
  [(not-closed-thunk* (closure (thunk* M) Env)) #f]
  [(not-closed-thunk* _) #t])

(define :-->cek
  (reduction-relation
   ISWIM
   #:domain CEK-config
   ; APP
   (--> (cek (closure (M N) Env) Kcek)
        (cek (closure M Env) (ar (closure N Env) Kcek)))

   ; ($WAU ARG)
   (--> (cek (closure ($wau X M) Env_1) (ar (closure N Env_2) Kcek))
        (cek (closure M (extend Env_1 X (closure (thunk* N) Env_2))) Kcek))

   ; (CV ARG)
   (--> (cek (closure (λ X M) Env) (ar CN Kcek))
        (cek CN (fn (closure (λ X M) Env) Kcek))
        ;(where #t (not-closed-wau? CV))
        )
   (--> (cek CV (fn (closure (λ X M) Env) Kcek))
        (cek (closure M (extend Env X CV)) Kcek))

   ; (OP1 ...)
   (--> (cek (closure (Op1 M) Env) Kcek)
        (cek (closure M Env) (op Op1 () () Kcek)))
   (--> (cek (closure B Env) (op Op1 () () Kcek))
        (cek (closure VN empty) Kcek)
        (where (VN) ,(apply-reduction-relation delta (term (Op1 B)))))

   ; (OP2 ... ...)
   (--> (cek (closure (Op2 M N) Env) Kcek)
        (cek (closure M Env) (op Op2 () ((closure N Env)) Kcek)))
   (--> (cek CV (op Op2 () (CN) Kcek))
        (cek CN (op Op2 (CV) () Kcek))
        (where #t (not-closed-thunk* CV)))
   (--> (cek (closure B_2 Env_2) (op Op2 ((closure B_1 Env_1)) () Kcek))
        (cek (closure VN empty) Kcek)
        (where (VN) ,(apply-reduction-relation delta (term (Op2 B_1 B_2)))))

   ;; Exercise 1: if0
   (--> (cek (closure (if0 M N_1 N_2) Env) Kcek)
        (cek (closure M Env) (if0 N_1 N_2 Env Kcek)))
   (--> (cek (closure B Env_0) (if0 N_1 N_2 Env Kcek))
        (cek (closure N Env) Kcek)
        (where (N) ,(apply-reduction-relation delta-if (term (if0 B N_1 N_2)))))

   ;;(->> (cek (closure X Env) Kcek)
   ;;     (cek CM Kcek)
   ;;     (where (thunk* CM) (lookup Env X)))
   
   (--> (cek (closure X Env) Kcek)
        (cek CV Kcek)
        (where CV (lookup Env X))) ;; changed CV to CM because of $wau

   (--> (cek (closure (thunk* M) Env) Kcek)
        (cek (closure M Env) Kcek))

   )) 

;; ============================================================

;; Exercise 1
;; Somewhere in the depths of this file.

(define the-term-2
  (term (if0 (+ 2 -2) 23 42)))

(define the-term-3
  (term (if0 1 23 42)))



(module+ test
 
  ;; (stepper :-->cek (term (cek (closure ,the-term empty) mt)))
  (test-equal
   (car (apply-reduction-relation* :-->cek (term (cek (closure ,the-term empty) mt))))
   (term (cek (closure 34 empty) mt)))

  ;; (stepper :-->cek (term (cek (closure ,the-term-2 empty) mt)))
  (test-equal
   (car (apply-reduction-relation* :-->cek (term (cek (closure ,the-term-2 empty) mt))))
   (term (cek (closure 23 empty) mt)))

  ;; (stepper :-->cc (term (cc ,the-term-2 hole)))
  (test-equal
   (car (apply-reduction-relation* :-->cc (term (cc ,the-term-2 hole))))
   (term (cc 23 hole)))

  ;; (stepper :-->scc (term (scc ,the-term-2 hole)))
  (test-equal
   (car (apply-reduction-relation* :-->scc (term (scc ,the-term-2 hole))))
   (term (scc 23 hole)))

  ;; (stepper :-->ck (term (ck ,the-term-2 mt)))
  (test-equal
   (car (apply-reduction-relation* :-->ck (term (ck ,the-term-2 mt))))
   (term (ck 23 mt)))

;; (stepper :-->cek (term (cek (closure (if0 (+ 1 -1) 9 ((λ x (x x)) (λ x (x x)))) empty) mt)))
)

;; Exercise 2
(define-metafunction ISWIM
  desugar : M -> M ;; (add1 n) -> (+ n 1) ...

  [(desugar B) B]

  [(desugar X) X]

  [(desugar (λ X M)) (λ X (desugar M))]

  [(desugar ($wau X M)) ($wau X (desugar M))]

  [(desugar (M N)) ((desugar M) (desugar N))]

  [(desugar (add1 M)) (+ (desugar M) 1)]

  [(desugar (sub1 M)) (+ (desugar M) -1)]
  
  [(desugar (Op1 M)) (Op1 (desugar M))]

  [(desugar (Op2 M N)) (Op2 (desugar M) (desugar N))]

  [(desugar (if0 M N_1 N_2)) (if0 (desugar M) (desugar N_1) (desugar N_2))]

  [(desugar (let ([X N]) M)) ((λ X (desugar M)) (desugar N))]

  [(desugar (iszero M)) (if0 (desugar M) (λ t (λ f t)) (λ t (λ f f)))]
  )

(define with-let (term
                  (desugar
                   (let
                       ([x (+ 2 3)])
                     (let
                         ([y (+ 4 2)])
                          (+ x y))))))

;; (stepper :-->cek (term (cek (closure ,with-let empty) mt)))

(define with-iszero (term
                     (desugar
                      (iszero (+ 23 -23)))))

;; Exercise 3

(define y-comb (term
                ($wau f (
                         ($wau x (f (x x)))
                         ($wau x (f (x x)))))))

(define fix (term
             (λ f
               (λ x ((
                      (λ g (f (λ v ((g g) v))))
                      (λ g (f (λ v ((g g) v))))) x)))))

(define fact (term
              (desugar
               (λ f (λ n (if0 n 1 (* n (f (sub1 n)))))))))

(define fact-lazy (term
                   (desugar
                    ($wau f ($wau n (if0 n 1 (* n (f (sub1 n)))))))))

(define fact-term-lazy (term
                        (desugar (,y-comb ,fact-lazy))))

(define fact-term (term
                   (desugar (,fix ,fact))))

(define fact-0 (term (,fact-term 0)))
(define fact-0-lazy (term (,fact-term-lazy 0)))

(define fact-1 (term (,fact-term 1)))
(define fact-1-lazy (term (,fact-term-lazy 1)))

(define fact-2 (term (,fact-term 2)))
(define fact-2-lazy (term (,fact-term-lazy 2)))

(define fact-5 (term (,fact-term 5)))
(define fact-5-lazy (term (,fact-term-lazy 5)))

(define fact-20 (term (,fact-term 20)))
(define fact-20-lazy (term (,fact-term-lazy 20)))

(module+ test
  (test-equal
   (car (apply-reduction-relation* :-->cc (term (cc ,fact-20 hole))))
   (term (cc 2432902008176640000 hole)))
  (test-equal
   (car (apply-reduction-relation* :-->cc (term (cc ,fact-20-lazy hole))))
   (term (cc 2432902008176640000 hole)))

  (test-equal
   (car (apply-reduction-relation* :-->scc (term (scc ,fact-20 hole))))
   (term (scc 2432902008176640000 hole)))
  (test-equal
   (car (apply-reduction-relation* :-->scc (term (scc ,fact-20-lazy hole))))
   (term (scc 2432902008176640000 hole)))

  (test-equal
   (car (apply-reduction-relation* :-->ck (term (ck ,fact-20 mt))))
   (term (ck 2432902008176640000 mt)))
  (test-equal
   (car (apply-reduction-relation* :-->ck (term (ck ,fact-20-lazy mt))))
   (term (ck 2432902008176640000 mt)))
  
  (test-equal
   (car (apply-reduction-relation* :-->cek (term (cek (closure ,fact-20 empty) mt))))
   (term (cek (closure 2432902008176640000 empty) mt)))
  #;(test-equal
   (car (apply-reduction-relation* :-->cek (term (cek (closure ,fact-20-lazy empty) mt))))
   (term (cek (closure 2432902008176640000 Env) mt)))
  ;; too big, too slow... Aint no body got time for that!

  (test-equal
   (car (apply-reduction-relation* :-->cek (term (cek (closure ,fact-5 empty) mt))))
   (term (cek (closure 120 empty) mt)))
  (test-equal
   (car (apply-reduction-relation* :-->cek (term (cek (closure ,fact-5-lazy empty) mt))))
   (term (cek (closure 120 empty) mt)))

)

;; Exercise 4

(define unchurch-term (term (λ n ((n (λ x (add1 x))) 0))))

(define church-0 (term (λ s (λ z z))))

(define church-2 (term (λ s (λ z (s (s z))))))

(define un-test-0 (term (,unchurch-term ,church-0)))
(define un-test-2 (term (,unchurch-term ,church-2)))

(module+ test
  (test-equal
   #t
   (redex-match?
    ISWIM
    (cek (closure 0 Env) mt)
    (car (apply-reduction-relation* :-->cek (term (cek (closure ,un-test-0 empty) mt))))))

  (test-equal
   #t
   (redex-match?
    ISWIM
    (cek (closure 2 Env) mt)
    (car (apply-reduction-relation* :-->cek (term (cek (closure ,un-test-2 empty) mt)))))))

;; I will maybe do optional stuff later. As well as desugaring the op1.
;; Right now I just want to submit little bit early before the deadline.
;; I had a lot of fun though!