Skip to content

Instantly share code, notes, and snippets.

@TeWu
Last active September 2, 2024 18:34
Show Gist options
  • Save TeWu/96cc5a49fce3fa0c6defcf5c50bdf309 to your computer and use it in GitHub Desktop.
Save TeWu/96cc5a49fce3fa0c6defcf5c50bdf309 to your computer and use it in GitHub Desktop.
Factorial function in lambda calculus - implemented in 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
//
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment