-1

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
David542
  • 104,438
  • 178
  • 489
  • 842
  • 2
    `const ADD = n1 => n2 => n1(n => f => a => f(n(f)(a)))(n2)`? (can be eta reduced to `const ADD = n1 => n1(n => f => a => f(n(f)(a)))`) – Lauren Yim Apr 02 '22 at 01:34
  • 2
    [cs.se] would probably be a better place for lambda calculus questions. Translating them into JS doesn't really change the nature of the question much. – Barmar Apr 02 '22 at 01:36
  • @cherryblossom I see, man that gets pretty abstract so quickly. Thanks for pointing that out. – David542 Apr 02 '22 at 01:37
  • @cherryblossom so does the lambda expression become `ADD = λnk.n ( λnfa.f(nfa) ) k` ? – David542 Apr 02 '22 at 01:39

1 Answers1

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

Lauren Yim
  • 12,700
  • 2
  • 32
  • 59
  • thanks so much for taking the time here. Could you explain a bit about how you got to the second definition of add? – David542 Apr 02 '22 at 01:59
  • I see how you can move this part over -- https://gyazo.com/d1bbc8a55441ce19e0b418a26e18d8e1 -- but why does it then become `n1(f)(...)` and not `n1(f(...))` ? Would you want to show how that beta reduction works? – David542 Apr 02 '22 at 02:02
  • 1
    @David542 I’m not sure how to reduce the first definition of `ADD` into the second one, but I’ve added some explanation to my answer for how the second one is derived. – Lauren Yim Apr 02 '22 at 03:26