y,z combinators, ts edition

combinators.ts

// 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.