; numbers
;; zero = λf.λx.x
(define zero
(lambda (f) (lambda (x) x)))
;; λf.λx.f x
(define one
(lambda (f) (lambda (x) (f x))))
;; λf.λx. f (f x)
(define two
(lambda (f) (lambda (x) (f (f x)))))
(define three (add-1 two))
(define four (add-1 three))
; operations
;; add-1 n = n+1 = λf.λy.f ((n f) y)
(define (add-1 n)
(lambda (f) (lambda (x) (f ((n f) x)))))
;; a+b
(define (add a b)
(lambda (f) (lambda (x) ((a f) ((b f) x)))))
;; mult = m*n = λm.λn.λf. n (m f)
(define (mult m n)
(lambda (f) (n (m f))))
; predicates
;; zero? ≡ λn. n (λx.F) T
(define zero?
(lambda (n) ((n (lambda (x) #f)) #t)))
;;; n-1 = λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)
(define (n-1 n)
(lambda (f) (lambda (x) (((n (lambda (g) (lambda (h) (h (g f)))))
(lambda (u) x))
(lambda (u) u)))))
; converting
;; get-number - convert Church numbers to Scheme numbers
(define (get-number n)
(if (zero? n)
0
(1+ (get-number (n-1 n)))))
; test
(zero? zero)
(zero? one)
(zero? (n-1 (add-1 zero)))
(get-number zero)
(get-number one)
(get-number three)
(get-number (add two three))
(get-number (mult one one))
(get-number (mult zero one))
(get-number (mult one three))
(define five (add two three))
(define six (mult two three))
(get-number (mult six five))
(zero? two)
(zero? (n-1 two))
(zero? (n-1 (n-1 two)))
; β-reduction example of (n-1 two)
;; (λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)) (λfx.f (f x))
;; λf.λx. (λfx.f (f x)) (λg.λh. h (g f)) (λu. x) (λu. u))
;; λf.λx. (λx.(λg.λh. h (g f)) ((λg.λh. h (g f)) x)) (λu. x) (λu. u))
;; λf.λx. ((λg.λh. h (g f)) ((λg.λh. h (g f)) (λu. x))) (λu. u))
;; λf.λx. (λh. h (((λg.λh. h (g f)) (λu. x)) f)) (λu. u)
;; λf.λx. (λu. u) (((λg.λh. h (g f)) (λu. x)) f))
;; λf.λx. (((λg.λh. h (g f)) (λu. x)) f)
;; λf.λx. ((λh. h ((λu. x) f)) f)
;; λf.λx. f x
P.S. решил что проще поменять цветовую схему блога под настройки в емаксе, чем наоборот) а уж воевать с htmlize - эт точно на долго бы затянулось..
Комментариев нет:
Отправить комментарий