суббота, 1 мая 2010 г.

Числа Чёрча

Должен был рассказывать в универе про лямбда-исчисление.. набросал такой примерчик(все честно спизжено с wiki и переписано на схему):


; 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 - эт точно на долго бы затянулось..

Комментариев нет:

Отправить комментарий