untyped normalization by evaluation

unbe.scm

(use r7rs)

(define uniq
  (let ((n 0))
    (lambda ()
      (set! n (+ n 1))
      (string->symbol (string-append "$" (number->string n))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; - Operational aspects of untyped normalization by evaluation, K. Aehlig et al, MSCS 2003.
;;; - Normalization by evaluation, Sam Lindley, http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; object language
;; e ::= x
;;     | c
;;     | (lambda (x) e)
;;     | (e e)

;; meta language
;; E ::= (NE . e)
;;     | (ABS . f)

; e -> E
(define (reflect e)
  `(NE . ,e))

; E -> e
(define (reify e)
  (let ((tag (car e)) (e (cdr e)))
    (case tag
      ((ABS) (let ((x (uniq)))
	       `(lambda (,x) ,(reify (e (reflect x))))))
      ((NE) e))))

; E * E -> E
(define (app f x)
  (let ((tag (car f)) (f (cdr f)))
    (case tag
      ((ABS) (f x))
      ((NE) (reflect `(,f ,(reify x)))))))

; (E -> E) -> E
(define (lam f)
  `(ABS . ,f))

; e -> E
(define (interpret e env)
  (cond
   ((symbol? e)
    (let ((v (assq e env)))
      (if v (cdr v) (reflect e))))
   ((not (pair? e))
    (reflect e))
   ((eq? 'lambda (car e))
    (let ((v (caadr e)) (e (caddr e)))
      (lam (lambda (x) (interpret e `((,v . ,x) . ,env))))))
   (else
    (let ((f (interpret (car e) env))
	  (x (interpret (cadr e) env)))
      (app f x)))))

(define (nbe e env)
  (reify (interpret e env)))

(nbe '((lambda (y) y) x) '())		; => x

(nbe '(lambda (x) ((lambda (z) z) x)) '()) ; => (lambda ($2) $2)

(nbe '(lambda (x) (lambda (y) (x y))) '()) ; => (lambda ($3) (lambda ($4) ($3 $4)))

(nbe '((lambda (x) ((lambda (z) z) x)) y) `((y . ,(reflect 1)))) ; => 1

(nbe '((+ 1) 2)
     `((+ . ,(lam (lambda (x)
		    (lam (lambda (y)
			   (reflect (+ (reify x) (reify y)))))))))) ; => 3

; w/ side effects
(nbe '(lambda (x) (print 42))
     `((print . ,(lam (lambda (x)
			(display (reify x))
			(newline)
			(reflect #f))))))	; => (lambda ($5) #f)  console: 42

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; One-pass CPS transformation is just a normalization-by-evaluation interpreter.
;;; - Ordinary and one-pass CPS transformation, Oleg Kiselyov, http://okmij.org/ftp/tagless-final/cookbook.html#CPS
;;; - Representing control: a study of the CPS transformation, O. Danvy, A. Filinski, MSCS'92.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; [x] --> \k.k@x
;; [\x.M] --> \k.k@\x.[M]
;; [M@N] --> \k.[M]@\m.[N]@\n.(m@n)@k

; E -> E
(define (cps-var x)
  (lam (lambda (k) (app k x))))

; (E -> E) -> E
(define (cps-lam f)
  (lam (lambda (k)
         (app k (lam f)))))

; E * E -> E
(define (cps-app f x)
  (lam (lambda (k)
         (app f (lam (lambda (m)
                       (app x (lam (lambda (n)
                                     (app (app m n) k))))))))))

; e -> E
(define (cps-interpret e env)
  (cond
   ((symbol? e)
    (cps-var (cdr (assq e env))))
   ((eq? 'lambda (car e))
    (let ((v (caadr e)) (e (caddr e)))
      (cps-lam (lambda (x) (cps-interpret e `((,v . ,x) . ,env))))))
   (else
    (let ((f (cps-interpret (car e) env))
          (x (cps-interpret (cadr e) env)))
      (cps-app f x)))))

(define (cps-nbe e env)
  (reify (cps-interpret e env)))

(cps-nbe '(lambda (x) x) '())

(cps-nbe '(lambda (f)
	    (lambda (x)
	      (lambda (y)
		((f y) x))))
	 '())
;; =>
;; (lambda ($15)
;;   ($15 (lambda ($16)
;; 	 (lambda ($17)
;; 	   ($17 (lambda ($18)
;; 		  (lambda ($19)
;; 		    ($19 (lambda ($20)
;; 			   (lambda ($21)
;; 			     (($16 $20) (lambda ($22)
;; 					  (($22 $18) $21)))))))))))))

(cps-nbe '(call/cc (lambda (f)
		     ((f x) y)))
	 `((call/cc . ,(lam (lambda (f)
			      (lam (lambda (k)
				     (app (app f (lam (lambda (x)
						    (lam (lambda (m)
							   (app k x))))))
					  k))))))
	   (x . ,(reflect 'x))
	   (y . ,(reflect 'y))))