От: | Кодт | ||
Дата: | 02.09.15 11:05 | ||
Оценка: | 10 (1) |
zero f x = x
one f x = f x
two f x = f (f x)
(inc n) f x = n f (f x) -- тут я пишу скобки в объявлении, чтобы сделать карринг более наглядным и подчеркнуть суть:
(plus n m) f x = n f (m f x) -- (inc n), (plus n m), (mult n m) - это нумералы, т.к. они принимают аргументы f и x
(mult n m) f x = n (m f) x -- а (m f) - функция одного аргумента - тут без карринга пришлось бы тащить лямбды
немножко писанины | |
Обычно декремент делается на сдвиге
после чего вычитание
Важный момент: нумералы — по-прежнему изоморфны неотрицательным числам, поэтому декремент нуля не определён. Обычно там делают идемпотентную заглушку:
что приводит к
| |
От: | A13x | ||
Дата: | 03.09.15 00:43 | ||
Оценка: | 15 (1) |
;; Boolean logic
(def l-true (% a (% b a))) ; logical 'true'
(def l-false (% a (% b b))) ; logical 'false'
(def l-and (% p (% q p q p))) ; logical 'and'
(def l-or (% p (% q p p q))) ; logical 'or'
(def l-not (% p p l-false l-true)) ; logical 'not'
(def l-xor (% p (% q p (l-not q) q))) ; logical 'xor'
(def l-if (% p (% a (% b p a b)))) ; if (p) then (a) else (b)
(def l-negative? (% n n (% x l-false) (% y l-true) l-false))
(def l-positive? (% n n (% x l-true) (% y l-false) l-false))
;;
;; Numerals
;;
;; Zero number
(def zero (% s (% p (% z z))))
;;Naive succ def - it won't work - (def succ (% n (% s (% p (% z s (((n s) p) z))))))
;; predecessor (decrement) for positive numbers only
;; PRED := λn.λf.λb.λx.n (λg.λh.h (g f)) b (λu.x) (λu.u)
(def pos-pred (% n (% f (% b (% x n (% g (% h h (g f))) b (% u x) (% u u))))))
;; (numcall (pos-pred (succ one)))
;; successor (increment) for negative numbers only
(def neg-succ (% n (% b (% f (% x n b (% g (% h h (g f))) (% u x) (% u u))))))
;; (numcall (neg-succ (pred zero)))
;; (numcall (neg-succ (pred (pred zero))))
;; Successor operation (increment)
(def succ (% n
(((l-if (l-negative? n)) (neg-succ n))
(% s (% p (% z (s (((n s) p) z))))))))
;; Predecessor operation (decrement)
(def pred (% n
(((l-if (l-positive? n)) (pos-pred n))
(% s (% p (% z (p (((n s) p) z))))))))