 Use of "reduce^" from Newlisp REPL (setf [println.supressed] true [print.supressed] true) (load "http://instprog.com/Instprog.default-library.lsp" ) (setf [println.supressed] nil [print.supressed] nil) ;--------------------------------------------------------------- ; Interpreter for lambda-calculus, described in recent posts is now ; integrated in my library for Newlisp, as function "reduce^". ; ; Here is example demonstrating how it works. If you want to see ; implementatition details, check the library. Check the previous ; posts also. (println (reduce^ '((^ x . (x (x x))) (^ y . (y (y y)))) ;lambda-expression 10 ;maximal number of reductions, ;useful for non-terminating lambda-expressions true ;true if you want reduction steps are printed on screen ;nil if you want "silent" interpretation )) (println (reduce^ '((^ x . x) (^ x . x)) 10 true )) (println (reduce^ '((^ x . (x x)) (^ x . (x x))) 10 true )) (exit) ; OUTPUT: ; ; 1. ==[ start ]==> ((^x.(x (x x)))(^y.(y (y y)))) ; 2. ==[ beta ]==> ((^y.(y (y y)))((^y.(y (y y)))(^y.(y (y y))))) ; 3. ==[ alpha ]==> ((^x.(x (x x)))((^y.(y (y y)))(^z.(z (z z))))) ; ... ; ; UNREDUCED: maximal number of reductions reached. ; ; (unreduced ((((^ y . (y (y y))) ((^ y . (y (y y))) (^ y . (y (y y))))) (((^ z . ( ; z ; (z z))) ; (^ x1 . (x1 (x1 x1)))) ; ((^ y1 . (y1 (y1 y1))) (^ z1 . (z1 (z1 z1)))))) ; (((^ x2 . (x2 (x2 x2))) (^ y2 . (y2 (y2 y2)))) ((^ z2 . (z2 (z2 z2))) (^ x3 . ( ; x3 ; (x3 x3)))))) 10) ; ; 1. ==[ start ]==> ((^x.x)(^x.x)) ; 2. ==[ alpha ]==> ((^x.x)(^y.y)) ; 3. ==[ beta ]==> (^y.y) ; 4. ==[ alpha ]==> (^x.x) ; ; REDUCED to normal form. ; ; (reduced (^ x . x) 4) ; ; 1. ==[ start ]==> ((^x.(x x))(^x.(x x))) ; 2. ==[ alpha ]==> ((^x.(x x))(^y.(y y))) ; 3. ==[ beta ]==> ((^y.(y y))(^y.(y y))) ; 4. ==[ alpha ]==> ((^x.(x x))(^y.(y y))) ; ; IRREDUCIBLE: cycle. ; ; (irreducible ((^ x . (x x)) (^ y . (y y))) 4) ; ; ; |
If you like this post, you'll probably like
| Almost two hundred thousand reduced lambda-expressions. |
--
No comments:
Post a Comment