;;;lambda calculus
;;;booleans
true = x.y.x
false = x.y.y
if = v. .f. v t f
;;;ex
if true M N = M
--->(v. .f. v t f) (x.y.x) M N
--->(x.y.x) M N
--->M
;;;Pairs
;fst(mkpair M N) = M
;snd(mkpair M N) = N
makpair = x.y.f. f x y
fst =p.p true
snd =p.p false
;;;Church number
;;;a lambda function stand for natrual number
;;;encoded by a function of two arguments, f and x
;;;where the function applies f to x n tims (number n)
0 = f.x.x
1 = f.x.f x
2 = f.x.f (f x)
3 = f.x.f (f (f x))
...
n = f.x.f...ntimes...(f x)
add1 = .f.x f (n f x) ;apply f n+1 times
add = m. . m add1 n ;m haapens to be a function that will take add1 and apply it m times
iszero = . n (x.false) true
;;;减法,主要就是要减少一次f的调用
;;;把n的f全部替换为warp f,x替换成<true,x>
;;;其中这个true主要是用来表示是否为第一次执行f,如果是那么就是x,如果不是那么就继续保持f x
;;;很简单,带入展开就知道了
sub1 =
.f.x. snd(n (warp f) <true,x>)
warp = f.p.<false , if (fst p) (snd p) (f (snd p))>
---未完---