ISWIM Call by Name

README.md

Call-by-Name ISWIM

Implement call-by-name evaluation for ISWIM using Redex.

Specifically:

The syntax of expressions is the same as basic ISWIM.

Evaluation of function application uses β instead of βᵥ. Evaluation of primitive operations is the same as basic ISWIM.

You must define

• the nonterminal En for call-by-name evaluation contexts
• the notion of reduction beta
• the standard reduction relation :-->n

You are not required to adapt any of the abstract machines.

Example:

(((λ unused (λ x (* (+ 1 x) (+ 2 x))))
  ((λ x (x x)) (λ x (x x))))
 (+ 3 4))
:-->>n 72

iswim-cbn.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)]

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


  [(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)]

  [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)]

  [EN hole (EN N) (B EN) (X EN) (Op1 EN) (Op2 EN N) (Op2 V EN) (if0 EN N_1 N_2)]
  ;;              we won't go into lambda's argument
)

;; ----------------------------------------
;; 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_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))]

  [(free-in X M)
   ---------------------------------------- "free-in-if0-condition"
   (free-in X (if0 M N_1 N_2))]

  [(free-in X N_1)
   ---------------------------------------- "free-in-if0-then"
   (free-in X (if0 M N_1 N_2))]

  [(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 (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
  (reduction-relation
   ISWIM
   (--> ((λ X M) N)
        (subst X N M))))

(define beta-v
  (reduction-relation
   ISWIM
   (--> ((λ X M) V)
        (subst X V 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))

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



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

(define :-->n (context-closure reduce ISWIM EN))

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


;; ----------------------------------------


(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 y-comb (term
                (λ f (
                      (λ x (f (x x)))
                      (λ x (f (x x)))))))

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

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

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

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

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

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


(module+ test
  (test-equal (car (apply-reduction-relation* :-->n fact-0))
              (term 1))
  (test-equal (car (apply-reduction-relation* :-->n fact-1))
              (term 1))
  (test-equal (car (apply-reduction-relation* :-->n fact-2))
              (term 2))
  (test-equal (car (apply-reduction-relation* :-->n fact-5))
              (term 120)))

;; ------------------------------------------