;;; Time-stamp: <2006-02-02 23:28:44 mgellis>

;;; Here is a normal order evaluator.  It may not be fast
(define eval-exp
  (lambda (expr)
    (let ([reduc (find-reduction expr)])
      (cond
        [(null? reduc) expr]
        [else (let ([redex (car reduc)]
                    [context (cdr reduc)])
                (eval-exp (context (apply subst redex))))]))))

(define subst
  (lambda (var val expr)
    (match expr
      [,v (guard (equal? v var)) val]
      [,v (guard (symbol? v)) v]
      [(,[e1] ,[e2]) `(,e1 ,e2)]
      [(lambda (,f) ,body)
       (cond
         [(equal? var f) `(lambda (,f) ,body)]
         [(not (occur-free f val))
          `(lambda (,f) ,(subst var val body))]
         [else (let ([z (gensym "z")])
                 `(lambda (,z)
                    ,(subst var val (subst f z body))))])])))

(define occur-free
  (lambda (var expr)
    (match expr
      [,x (guard (equal? var x)) #t]
      [,x (guard (symbol? x)) #f]
      [(,[e1] ,[e2]) (or e1 e2)]
      [(lambda (,f) ,body) (guard (equal? var f)) #f]
      [(lambda (,f) ,[body]) body])))


(define find-reduction
  (lambda (expr)
    (call/cc
     (lambda (hop) ;; So we can hop out once we find a redex
       (letrec
           ([find-reduction
             (lambda (expr context)
               (match expr
                 [((lambda (,f) ,body) ,rand)
                  (hop `((,f ,rand, body) . ,context))]
                 [(,e1 ,e2)
                  (find-reduction e1 (lambda (x)
                                       (context `(,x ,e2))))
                  (find-reduction e2 (lambda (x)
                                       (context `(,e1 ,x))))]
                 [(lambda (,f) ,b)
                  (find-reduction b
                                  (lambda (x)
                                    (context `(lambda (,f) ,x))))]
                 [,v (guard (symbol? v)) '()]))])
         (find-reduction expr (lambda (x) x)))))))

;;; Here's is an implementation of the abstraction algorithm:

(define lambda->ski
  (lambda (expr)
    (match expr
      [,v (guard (symbol? v)) v]
      [(lambda (,f) ,[b]) (replace f b)]
      [(,[e1] ,[e2]) `(,e1 ,e2)])))

(define replace
  (lambda (k expr)
    (match expr
      [,v (guard (and (symbol? v) (eq? v k))) 'I]
      [,v (guard (symbol? v)) `(K ,v)]
      [(,[e1] ,[e2]) `((S ,e1) ,e2)])))


;;; Here is X in terms of S and K
(define X
  `(lambda (q)
     (((q K) S) K)))

;;; You should note that (X (X X)) = S and ((X X) X) = K

;;; If we abstract X:

(lambda->ski X)

;;; We get: ((s ((s ((s i) (k k))) (k s))) (k k))

;;; Note that since we can express S and K in terms of X, we can also
;;; express I in terms of X.  Using S and K we can define I as ((S K) K)
;;; but recall that the second K is just filler, ((S K) S) is also I.
;;; Infact we can put anything we want there.  So ((S K) X) is also I.

;;; Hence we can write I as: (((X (X X)) ((X X) X)) X)

;;; Now we can have some fun!

;;; Here's a program that takes something in SKI and converts it to just
;;; using X

(define ski->X
  (lambda (expr)
    (match expr
      [I '(((X (X X)) ((X X) X)) X)]
      [K '((X X) X)]
      [S '(X (X X))]
      [(,[e1] ,[e2]) `(,e1 ,e2)])))

;;; And we can do:

(ski->X '((s ((s ((s i) (k k))) (k s))) (k k)))

;;; And we get:

;;; (((x (x x))
;;;   (((x (x x))
;;;     (((x (x x)) (((x (x x)) ((x x) x)) x))
;;;      (((x x) x) ((x x) x))))
;;;    (((x x) x) (x (x x)))))
;;;  (((x x) x) ((x x) x)))

;;; We can write a program to take an expression like the above and convert
;;; it into The Lambda Calculus, using the definition of X that we know

;;; Here we use a nicer gensym, since Scheme's gensym is hard to read...
(define parse-X
  (lambda (expr)
    (let ([counts (list (cons 'x 0) (cons 'y 0) (cons 'z 0) (cons 'q 0))])
      (let ([gensym (lambda (v)
                      (let* ([a (assq v counts)]
                             [n (cdr a)])
                        (set-cdr! a (add1 n))
                        (string->symbol (string-append (symbol->string v) "."
                                                       (number->string n)))))])
        (match expr
          [X (let ([x.0 (gensym 'x)]
                   [x.1 (gensym 'x)]
                   [x.2 (gensym 'x)]
                   [y.0 (gensym 'y)]
                   [y.1 (gensym 'y)]
                   [y.2 (gensym 'y)]
                   [z.0 (gensym 'z)]
                   [q.0 (gensym 'q)])
               `(lambda (,q.0)
                  (((,q.0 (lambda (,x.0) (lambda (,y.0) ,x.0)))
                    (lambda (,x.1)
                      (lambda (,y.1) (lambda (,z.0) ((,x.1 ,z.0)
                                                     (,y.1 ,z.0))))))
                   (lambda (,x.2) (lambda (,y.2) ,x.2)))))]
          [(,[e1] ,[e2]) `(,e1 ,e2)])))))

;;; Now we can do this:

(eval-exp (parse-x '(((x (x x))
                      (((x (x x))
                        (((x (x x)) (((x (x x)) ((x x) x)) x))
                         (((x x) x) ((x x) x))))
                       (((x x) x) (x (x x)))))
                     (((x x) x) ((x x) x)))))

;;; And we get back:

;;; (lambda (z.33)
;;;   (((z.33 (lambda (x.44) (lambda (y.44) x.44)))
;;;     (lambda (x.25)
;;;       (lambda (y.25) (lambda (z.8) ((x.25 z.8) (y.25 z.8))))))
;;;    (lambda (x.8) (lambda (y.8) x.8))))

;;; Which is just:

;;; (lambda (q)
;;;   (((q k)
;;;     s)
;;;    k))

;;; So we have written an expression using only X that evaluates to itself.