Lambda Calculus Interpreter.






Later edit: there is newer, improved version of this interpreter, check
this post and few posts before that.



; Lambda calculus implemented in Newlisp. It would be too ambitious
; to explain what is lambda calculus in this post, so I'll assume
; that reader familiarized himself with notion of lambda calculus
; somewhere else, and I'll provide only code for evaluation ("reduction")
; of lambda-expressions. Instead of lambda symbol, I'll use ^ -
; and it was original symbol used by Church.

; Only beta-reduction (but this is only important one) and normal
; order evaluation (better one, used for Haskell and fexprs) - from
; outside to inside implemented.

(set 'is-variable (lambda(x)(symbol? x)))

(set 'is-function (lambda(L)(and (list? L)
                                 (= (first L) '^)
                                 (= (nth 2 L) '.))))
                                 
(set 'function-variable (lambda(f)(nth 1 f)))
(set 'function-body (lambda(f)(last f)))
                                 
(set 'is-application (lambda(L)(and (list? L)
                                    (= (length L) 2))))

(set 'substitute-free-occurences ; of variable V in E with F
     (lambda(V E F)
     
       (cond ((is-variable E) (if (= E V) F E))

             ((is-function E)
             
                  (if (= (function-variable E) V)
                      
                      E ; V is bounded in E - no substitution
                      
                      (list '^
                            (function-variable E)
                            '.
                            (substitute-free-occurences V
                                   (function-body E)
                                   F))))
                        
              ((is-application E)
               (list (substitute-free-occurences V (first E) F)
                     (substitute-free-occurences V (last E) F))))))
                        

(set 'reduce-once
     (lambda(E)
        (cond ((is-variable E) E)
              ((is-function E) E)      
              ((is-application E)
                (let ((E1 (first E))
                      (E2 (last E)))
                
                (if (is-function E1)
                
                    ;E=((^V._) E2) ==> E10[V:=E2]
                    

                    (substitute-free-occurences (function-variable E1)
                                                (function-body E1)
                                                E2)
                          
                     ;E=(E1 E2) ==>
                     
                     (let ((new-E1 (reduce-once E1)))

                           (if (!= new-E1 E1)
                               (list new-E1 E2)
                               (list E1 (reduce-once E2))))))))))
                                  

(set 'reduce (lambda(new-expression)
                (local(expression)
                  (println "\n--------------\n\n" (string new-expression))
                  (do-while (!= new-expression expression)
                            (setf expression new-expression)
                            (setf new-expression (reduce-once expression))
                            (if (!= new-expression expression)
                                (println " ==> " (string new-expression))
                                (println "\n     Further reductions are impossible."))
                new-expression))))

; The list of reduced expressions

(dolist (i '( x
             (^ x . x)
             ((^ x . x) y)
             ((^ x . a) ((^ y . y) z))  
             ((^ y . (^ z . z)) ((^ x . (x x)) (^ v . (v v))))
             ((((^ v . (^ t . (^ f . ((v t) f)))) (^ x . (^ y . x))) a) b)
             ((((^ v . (^ t . (^ f . ((v t) f)))) (^ x . (^ y . y))) a) b)
             ; (^ f . ((^ x . (f (x x))) (^ x . (f (x x))))) Y-combinator - test it!
             ((^ x . (x x)) (^ x . (x x)))
             ;((^ x . (x (x x))) (^ x . (x (x x))))
             ))
   
   ;(println "\n\n=== " (+ $idx 1) ": "  i "\n\n")
   
   (reduce i))
   
(exit)


                                      OUTPUT
                                   
                                   

--------------

x

     Further reductions are impossible.

--------------

(^ x . x)

     Further reductions are impossible.

--------------

((^ x . x) y)
 ==> y

     Further reductions are impossible.

--------------

((^ x . a) ((^ y . y) z))
 ==> a

     Further reductions are impossible.

--------------

((^ y . (^ z . z)) ((^ x . (x x)) (^ v . (v v))))
 ==> (^ z . z)

     Further reductions are impossible.

--------------

((((^ v . (^ t . (^ f . ((v t) f)))) (^ x . (^ y . x))) a) b)
 ==> (((^ t . (^ f . (((^ x . (^ y . x)) t) f))) a) b)
 ==> ((^ f . (((^ x . (^ y . x)) a) f)) b)
 ==> (((^ x . (^ y . x)) a) b)
 ==> ((^ y . a) b)
 ==> a

     Further reductions are impossible.

--------------

((((^ v . (^ t . (^ f . ((v t) f)))) (^ x . (^ y . y))) a) b)
 ==> (((^ t . (^ f . (((^ x . (^ y . y)) t) f))) a) b)
 ==> ((^ f . (((^ x . (^ y . y)) a) f)) b)
 ==> (((^ x . (^ y . y)) a) b)
 ==> ((^ y . y) b)
 ==> b

     Further reductions are impossible.

--------------

((^ x . (x x)) (^ x . (x x)))

     Further reductions are impossible.











--

No comments:

Post a Comment