zero = \s.\z.z
succ = \a.\s.\z.a s (s z)
mul = \a.\b.a (add b) zero
pow = \a.\b.a (mul b) (succ zero)

true = \a.\b.a
false = \a.\b.b
if = \c.\t.\f.c t f
not = \a.a false true
and = \a.\b.a b false
or = \a.\b.a true b
xor = \a.\b.a (not b) b

pair = \a.\b.\c.c a b
fst = \p.p true
snd = \p.p false
const = true

iszero = \n.n (const false) true
pred = (\pack.\packpred.\n.snd (n packpred (pack n))) (\n.pair zero n) (\n.iszero (fst n) (pair (succ zero) (snd n)) (pair (succ zero) (pred (snd n)))
sub = \a.\b.b pred a

eq = \a.\b.and (iszero (sub a b)) (iszero (sub b a))
ne=\a.\b.not (eq a b)
lt = \a.\b.and (iszero (sub a b)) (not (iszero (sub b a)))
le = \a.\b.or (eq a b) (lt a b)
gt = \a.\b.not (le a b)
ge = \a.\b.not (lt a b)

div = (\init.\step.\a.\b.add (fst (a step (init a b))) (fst (b step (init b a)))) (\a.\b.pair zero (pair a b)) (\i.(ge fst(snd i)) (snd (snd i))) (pair (succ (fst i)) (sub (fst (snd i)) (snd (snd i))) (snd (snd i))) i)

empty = pair zero zero
cons = \a.\b.pair (succ zero) (pair a b)
isempty = \l.iszero (fst l)
tail = \l.snd (snd l)

Y=\f.(\t.f (t t))(\t.f (t t))
foldr = Y (\self.\f.\e.\l.(isempty l) e (f (head l) (self f e (tail l))))
length = \l.foldr (true succ) zero l
sum = \l.foldr add zero l
product - \l.foldr mul (succ zero) l
append = \h.\l.foldr cons l h
reverse = \l.foldr (\a.\b.append b (const a empty)) empty l
map = \f.\l.foldr (\a.\b.cons (f a) b) l
zip = Y (\self.\a.\b.(or (isempty a) (isempty b)) empty (cons (pair (head a) (head b)) (self (tail a) (tail b))))
flatten = \l.map append l
posted on 2009-12-24 08:55 陈梓瀚(vczh) 阅读(2464) 评论(4)  编辑 收藏 引用 所属分类: 其他

# re: Lambda Calculus 2009-12-25 00:34 | 空明流转

。  回复  更多评论

# re: Lambda Calculus 2009-12-25 01:09 | 陈梓瀚(vczh)
@空明流转

# re: Lambda Calculus 2009-12-28 01:21 | radar

# re: Lambda Calculus 2010-01-08 01:14 | 太垃圾了

 只有注册用户登录后才能发表评论。 相关文章: