I am familiar with defining the ADD function on top of the SUCC function, such as in the following:

const ONE = f => a => f(a);   
const SUCC = n => f => a => f(n(f)(a));        // SUCC = λnfa.f(nfa)
const ADD = n1 => n2 => n1(SUCC)(n2);          // ADD  = λnk.n SUCC k 
console.log(ADD(ONE)(ONE)(x => x 1)(0));
// 2

However, how would I define add if there wasn't a successor function already defined? I tried using substitution to get the following, but I'm not sure why it's not working. What do I have screwed up here?

const ONE = f => a => f(a);
const ADD = n1 => n2 => f => a => n1(f(n1(f)(a)))(n2);
console.log(ADD(ONE)(ONE)(x => x 1)(0));
// TypeError: f is not a function

CodePudding user response：

const ADD = n1 => n2 => n1(n => f => a => f(n(f)(a)))(n2)
// ADD = λnk.n (λnfa.f (n f a)) k

This can also be eta-reduced to

const ADD = n1 => n1(n => f => a => f(n(f)(a)))
// ADD = λn.n (λnfa.f (n f a))

When doing substitution, you simply replace the term to be substituted with its definition:

• n1 => n2 => n1(SUCC)(n2)
• definition of SUCC: n => f => a => f(n(f)(a))
• replace SUCC with the above definition: n1 => n2 => n1(n => f => a => f(n(f)(a)))(n2)

Another way you could define ADD is like this:

const ADD = m => n => f => x => m(f)(n(f)(x))
// ADD = λmnfx.m f (n f x)

The Church numerals m and n can be seen as functions that take a function f and produce another function that applies f a particular number of times. In other words, n(f) can be seen as ‘repeat f n times’.

Therefore, ADD(m)(n) should return a function that repeats a function m n times.

const ADD =
  m => // first number
  n => // second number
  f => // function to be repeated
  x => // value
  (
    m(f) // 2. then apply f m times
    (n(f)(x)) // 1. apply f n times
  )

ADD(ONE) is also equivalent to SUCC (as you would expect):

• ADD(ONE)
• (m => n => f => x => m(f)(n(f)(x)))(ONE) (definition of ADD)
• n => f => x => ONE(f)(n(f)(x)) (beta-reduction)
• n => f => x => (f => a => f(a))(f)(n(f)(x)) (definition of ONE)
• n => f => x => (a => f(a))(n(f)(x)) (beta-reduction)
• n => f => x => f(n(f)(x)) (beta-reduction)
• SUCC (definition of SUCC)

For more information, see ‘Church encoding’ on Wikipedia.