diff options
Diffstat (limited to 'lambda-calcul/haskell/fac.lisp')
| -rw-r--r-- | lambda-calcul/haskell/fac.lisp | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/lambda-calcul/haskell/fac.lisp b/lambda-calcul/haskell/fac.lisp new file mode 100644 index 0000000..549334b --- /dev/null +++ b/lambda-calcul/haskell/fac.lisp @@ -0,0 +1,39 @@ +(let ((False (lam (f t) f)) + (True (lam (f t) t)) + (If (lam (b x y) (b x y))) + (Zero (lam (z s) z)) + (Succ (lam (n z s) (s n))) + (One (Succ Zero)) + (Two (Succ One)) + (Three (Succ Two)) + (IsZero (lam (n) (n True (lam (m) False)))) + (const (lam (x y) x)) + (Pair (lam (a b p) (p a b))) + (fst (lam (pair) (pair (lam (a b) a)))) + (snd (lam (pair) (pair (lam (a b) b)))) + (fix (lam (f) + ((lam (x) (f (x x))) + (lam (x) (f (x x)))))) + (add (fix (lam (radd x y) + (x y (lam (n) (Succ (radd n y))))))) + (mul (fix (lam (rmul x y) + (x Zero (lam (n) (add y (rmul n y))))))) + (fac (fix (lam (rfac x) + (x + One + (lam (n) (mul x (rfac n))))))) + (eqnat (fix (lam (reqnat x y) + (x (y True (const False)) + (lam (x1) (y False (lam (y1) (reqnat x1 y1)))))))) + (sumto (fix (lam (rsumto n) + (n Zero + (lam (m) (add n (rsumto m))))))) + (n5 (add Two Three)) + (n6 (mul Two Three)) + (n17 (add n6 (add n6 n5))) + (n37 (Succ (mul n6 n6))) + (n703 (sumto n37)) + (n704 (Succ (sumto n37))) + (n720 (fac n6)) + ) + (eqnat n720 (add n704 n17))) |