scheme-test-programs/lambda/t-beta-reduce.scm

;; import lambda/simple-gensym.scm lambda/beta-reduce.scm

(print (beta-reduce '(lambda y ((lambda x (lambda y x)) y))))
(print (beta-reduce '(lambda x ((lambda y x) y)))) ;; y is a free variable here
(print (beta-reduce '(lambda y ((lambda x (lambda y x)) y))))
(print (beta-reduce '(lambda y (lambda y ((lambda x (lambda y x)) y)))))
(print (beta-reduce '(lambda y (lambda x ((lambda x (lambda y x)) y)))))
(define id '(lambda i i))
(print (beta-reduce `(,id ,id)))
(print (beta-reduce `(,id (,id ,id))))
(print (beta-reduce (beta-reduce `(,id (,id ,id)))))
(newline)

(beta-reduce* #t `((,id ,id) ,id))

;; http://www.toves.org/books/lambda/
;; http://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html
;; http://jwodder.freeshell.org/lambda.html

(define y `(lambda f
             ((lambda x (f (x x)))
              (lambda x (f (x x))))))
(define l:TRUE '(lambda x (lambda y x)))
(define l:FALSE '(lambda x (lambda y y)))
(define l:IF '(lambda b (lambda t (lambda f ((b t) f)))))
(define l:AND `(lambda b-1 (lambda b-2 (((,l:IF b-1) b-2) ,l:FALSE))))
(define l:OR `(lambda b-1 (lambda b-2 (((,l:IF b-1) ,l:TRUE) b-2))))
(define l:NOT `(lambda b (((,l:IF b) ,l:FALSE) ,l:TRUE)))

(beta-reduce* #t `(,l:NOT ,l:TRUE))
(beta-reduce* #t `(,l:NOT ,l:FALSE))

(define l:ZERO `(lambda f (lambda x x)))
(define l:ONE `(lambda f (lambda x (f x))))
(define l:ADD '(lambda m (lambda n (lambda f (lambda x ((m f) ((n f) x)))))))
(define l:MUL `(lambda m (lambda n ((m (,l:ADD n)) ,l:ZERO))))

(define l:ISZERO `(lambda n ((n (lambda x ,l:FALSE)) ,l:TRUE)))
(define l:PRED `(lambda n (lambda f (lambda x
				      (((n (lambda g (lambda h
						       (h (g f)))))
					(lambda u x))
				       (lambda u u))))))

;;(beta-reduce* #t `(,l:PRED ,l:ONE))
(beta-reduce* #t `((
		    (,l:PRED ((,l:ADD ,l:ONE) ((,l:ADD ,l:ONE) ,l:ONE)))
		    1+) 0))

(define l:SUB `(lambda m (lambda n ((n ,l:PRED) m))))

(define l:LEQ `(lambda m (lambda n (,l:ISZERO ((,l:SUB m) n)))))

;;(beta-reduce* #t `((,l:LEQ ,l:ONE) ,l:ZERO))
;;(beta-reduce* #t `((,l:LEQ ,l:ZERO) ,l:ONE))

(print
 (beta-reduce* #f `(lambda f
		     (lambda n
			((,l:SUB ((,l:ADD ((,l:ADD ,l:ONE) ,l:ONE)) ((,l:ADD ,l:ONE) ,l:ONE)))
			 ,l:ONE)))))

(define l:FACT^ `(lambda f (lambda n (((,l:IF ((,l:LEQ n) ,l:ONE))
				       ,l:ONE)
				      ((,l:MUL n) ((f f) ((,l:SUB n) ,l:ONE)))))))
(define l:FACT `(,l:FACT^ ,l:FACT^))

;(beta-reduce* #t `(,l:FACT ,l:ONE))
(print
 (beta-reduce* #f `(((,l:FACT ((,l:ADD ((,l:ADD ,l:ONE) ,l:ONE))
			       ((,l:ADD ,l:ONE) ,l:ONE)))
		     1+) 0)))