Factorial function in lambda calculus - implemented in JS

lambda_factorial.js

///
///  Factorial function in lambda calculus - implemented in JS
///

//// Lambda calculus
// zero = λs.λz.z
// succ = λn.λs.λz.s (n s z)
// mult = λn.λm.λs.m (n s)
// pred = λn.λf.λx.n(λg.λh.h (g f))(λu.x)(λu.u)
// minus = λn.λm.m pred n
// true = λt.λf.t
// false = λt.λf.f
// not = λp.p false true
// and = λp.λq.p q p
// is_zero = λn.n (λx.false) true
// leq = λn.λm.is_zero (minus n m)
// Z = λf.( λx.(x x) λx.f(λy.x x y) )
// factorial = Z (λf.λn.( (leq n zero) (succ zero)  (λy.(mult n (f (pred n))) y) ))


//// Lambda JavaScript - Only lambda definition and application allowed (recursion is not allowed - "const"s used for clarity, but every expression should be inlinable)
const zero = s=>z=>z
const succ = n=>s=>z=>s(n(s)(z))
const mult = n=>m=>s=>m(n(s))
const pred = n=>f=>x=>n(g=>h=>h(g(f)))(u=>x)(u=>u)
const minus = n=>m=>m(pred)(n)
const bTrue = t=>f=>t
const bFalse = t=>f=>f
const and = p=>q=>p(q)(p)
const isZero = n=>n(x=>bFalse)(bTrue)
const leq = n=>m=>isZero(minus(n)(m))
const Z = f=>(x=>x(x))(x=>f(y=>x(x)(y)))

const factorial = Z(f=>n=>
  leq(n)(zero)(
    succ(zero)
  )(
    (y =>
      mult(n)(f(pred(n)))(y)
    )
  )  
)

const factorial_inlined = (f=>(x=>x(x))(x=>f(y=>x(x)(y))))(f=>n=>
  (n=>m=>(n=>n(x=>t=>f=>f)(t=>f=>t))((n=>m=>m(n=>f=>x=>n(g=>h=>h(g(f)))(u=>x)(u=>u))(n))(n)(m)))(n)(s=>z=>z)(
    (n=>s=>z=>s(n(s)(z)))(s=>z=>z)
  )(
    (y=>
      (n=>m=>s=>m(n(s)))(n)(f((n=>f=>x=>n(g=>h=>h(g(f)))(u=>x)(u=>u))(n)))(y)
    )
  )  
)

const factorial_inlined_minified = (f=>(x=>x(x))(x=>f(y=>x(x)(y))))(f=>n=>(n=>m=>(n=>n(x=>t=>f=>f)(t=>f=>t))((n=>m=>m(n=>f=>x=>n(g=>h=>h(g(f)))(u=>x)(u=>u))(n))(n)(m)))(n)(s=>z=>z)((n=>s=>z=>s(n(s)(z)))(s=>z=>z))((y=>(n=>m=>s=>m(n(s)))(n)(f((n=>f=>x=>n(g=>h=>h(g(f)))(u=>x)(u=>u))(n)))(y))))


//// JavaScript
const to_church_int = n => n <= 0 ? zero : succ(to_church_int(n-1))
const unchurch_int = n => n(m => m + 1)(0)

console.log( unchurch_int(factorial_inlined_minified(to_church_int(5))) )  //=> 120

// As ONE big lambda
console.log((n=>(n=>n(m=>m+1)(0))((f=>(x=>x(x))(x=>f(y=>x(x)(y))))(f=>n=>(n=>m=>(n=>n(x=>t=>f=>f)(t=>f=>t))((n=>m=>m(n=>f=>x=>n(g=>h=>h(g(f)))(u=>x)(u=>u))(n))(n)(m)))(n)(s=>z=>z)((n=>s=>z=>s(n(s)(z)))(s=>z=>z))((y=>(n=>m=>s=>m(n(s)))(n)(f((n=>f=>x=>n(g=>h=>h(g(f)))(u=>x)(u=>u))(n)))(y))))((f=>(x=>x(x))(x=>f(y=>x(x)(y))))(f=>n=>n<=0?s=>z=>z:(n=>s=>z=>s(n(s)(z)))(f(n-1)))(n))))(5))


// Sources / See also:
//               Church encoding @ Wikipedia:  https://en.wikipedia.org/wiki/Church_encoding
//    Programming with Nothing by Tom Stuart:  https://youtu.be/VUhlNx_-wYk
//    Y Not- Adventures in Functional Programming by Jim Weirich:  https://youtu.be/FITJMJjASUs   
//