owen-d · May 20, 2019 20:22 · May 20, 2019
diff --git a/combinators.ts b/combinators.ts
@@ -0,0 +1,49 @@
+// Y= λf.(λx.f (x x)) (λx.f (x x))
+
+y = f => {
+  const g = x => f(x(x))
+  return g(g)
+}
+
+// seems equivalent to Z for use in applicative order langs
+// Y1= λf.(λx. (λy. f (xx) y))(λx. (λy. f (xx) y))
+y1 = f => {
+  const g = x => y => f(x(x))(y)
+  return g(g)
+}
+
+// z:=λf.(λx.f (λv.((x x) v))) (λx.f (λv.((x x) v)))
+z = f => {
+  let g = x => f((v => x(x)(v)))
+  return g(g)
+}
+
+fact = f => n => n === 0 ? 1 : n * f(n-1)
+
+
+
+// reduction tests
+
+/*
+  Y1= λf.(λx. (λv. f (xx) v))(λx. (λv. f (xx) v))
+  *introduce an arg F
+  [f -> F]
+  (λx. (λv. F (xx) v))(λx. (λv. F (xx) v))
+  [x -> (λx. (λv. F (xx) v))]
+  λv. F ((λx. (λv. F (xx) v)) (λx. (λv. F (xx) v))) v
+  *via subst
+  λv. F (Y1 F) v
+*/
+
+/*
+  Z := λf.(λg.λx.f (g g) x) (λg.λx.f (g g) x)
+  *introduce an arg F
+  [f -> F]
+  (λg.λx.F (g g) x) (λg.λx.F (g g) x)
+  [g -> (λg.λx.F (g g) x)]
+  λx.F ((λg.λx.F (g g) x) (λg.λx.F (g g) x)) x
+  *via substitution:
+  λx.F (Z F) x
+*/
+
+// omg they _are_ equivalent!! lambda calculus is so cool.