; 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