wip: use de Bruijn indices representation

provide sample complex terms to evaluate

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)))