./Church Encoding in JavaScript

posted by cli on

Church Encoding in JavaScript

// References:
// https://en.wikipedia.org/wiki/Church_encoding
// http://matt.might.net/articles/js-church/

const I = x => x

// boolean
const TRUE = p => q => p(I);
const FALSE = p => q => q(I);

// operators
const AND = p => q => p (q) (p)
const OR = p => q => p (p) (q)
const NOT = p => p (FALSE) (TRUE)
const IF = pred => onTrue => onFalse => pred(onTrue)(onFalse)
const boolify = b => IF (b) (() => true) (() => false)

// numberals
const ZERO = f => z => z;
const ONE = f => z => f (z);

// cheat, convert number n to a church number
const numberal = n => f => z => n === 0 ? z : numberal(n - 1)(f)(f(z))

// arithmetic
const PLUS = m => n => f => z => m (f) (n (f) (z)) // fm+n (x) = fm(fn(x))
const SUCC = n => f => z => f (n (f) (z))
const MULT = m => n => f => z => m (n (f)) (z) // fmn (x) = (fn)m(x)
const EXP = m => n => n (m) // n f x = fn (x) -> n m f = mn f
// NOTE:
// m < n -> m - n = 0
// PRED(0) = 0

// predecessor function
// Wrap the value in a container and skip the first application of f
//
// value = v => h => h (v)
// extract = k => u => k (u)
// inc = g => h => h(g(f))
// init = h => h (x)
// const = u => x
// const PRED = n => f => x => extract(n inc const)
const PRED = n => f => z => (n (g => h => h(g(f))) (u => z)) (u => u)
const MINUS = m => n => (n (PRED)) (m) // fm-n = f(-1)n fm
// DIV is much more complicated...
// divide = (\n.((\f.(\x.x x) (\x.f (x x))) (\c.\n.\m.\f.\x.(\d.(\n.n (\x.(\a.\b.b)) (\a.\b.a)) d ((\f.\x.x) f x) (f (c d m f x))) ((\m.\n.n (\n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)) m) n m))) ((\n.\f.\x. f (n f x)) n))

const numerify = n => n (x => x + 1) (0)

// predicates
const ZEROP = n => n (() => FALSE) (TRUE)
const LE = m => n => ZEROP (MINUS (m) (n))
const EQ = m => n => AND (LE (m) (n)) (LE (n) (m))

// A combinator is a particular type of higher-order function that may be used in defining functions without using variables. The combinators may be combined to direct values to their correct places in the expression without ever naming them as variables.
// http://okmij.org/ftp/Computation/fixed-point-combinators.html
// U combinator
const U = f => f(f)
// U(U) will run forever

// const fact_u = U (f) = U (h => n => (n <= 1) ? 1 : fact_u(n - 1) * n)
// substitute fact_u with h(h), fact_u = U (h => n => (n <= 1) ? 1 : h(h)(n - 1) * n)

/**
 * x = f(x)
 * => x -> Y(f)
 * Y(f) = f(Y(f))
 */
// let Y = F => F(Y(F))
// => eta-expansion
// Y = F => F(Y(x => Y(F)(x)))
// => eliminate Y recursion with U
const Y = U (f => F => F(x => f(f)(F)(x)))
// => expand U
// Y = (f => F => F(x => f(f)(F)(x))) (f => F => F(x => f(f)(F)(x)))

// const fact_y = Y(fact => n => n <= 1 ? 1 : n * fact(n - 1))

// const factorial = fact => n => n <= 1 ? 1 : n * fact(n - 1)

// const trace = f => (...args) => {
//   console.log(`called with args:`, args);
//   return f(...args);
// }

// // This version only supports one argument
// const cache = new Map();
// const memoize = f => (arg) => {
//   if (cache.has(arg)) {
//     return cache.get(arg);
//   }

//   const v = f(arg);
//   cache.set(arg, v);
//   return v;
// }

// const compose = (...fn) => x => fn.reduceRight((rv, f) => f(rv), x)

// const fact = Y(compose(trace, memoize, factorial));


// Pair and List
const CONS = car => cdr => z => z (car) (cdr)
const CAR = cons => cons (car => cdr => car)
const CDR = cons => cons (car => cdr => cdr)
const NIL = FALSE
const NILP = cons => cons (car => cdr => z => TRUE) (FALSE)

// Computes factorial with only function definition and function application!
const church_factorial = Y(fact => n => IF (LE (n) (ONE)) (() => ONE) (() => MULT (fact (PRED (n))) (n)))


// signed number howto: let's consider integers for now. A number can be expresses a the difference between two numbers
// x = m - n, so we can use a pair to represent a signed number
// rational numbers can be expresses as a pair of signed numbers
//
// Real numbers are a little bit complex
// Real numbers may be encoded by a limiting process that guarantees that the difference from the real value differs by
// a number which may be made as small as we need
//
// Once we have real numbers, complex numbers can be expressed as a pair of real numbers.