I do not know how to solve this incredibly difficult question. The complexity rivals those of the millennial problems. Instead, I’ll let reddit user u/sellopou speak his words.
Take a computational approach to the problem. Specifically, consider the encoding of natural numbers in the simply-typed lambda calculus called Church numerals. In this encoding, the number 2 is represented by a function that looks like this:
2 ≡ λf.λx.f (f x)
In other words, the number two is a function that takes a function and some value (let's assume that we're comfortable with currying here), and applies the function twice to the value. In general, a number n is represented by a function that takes a function and some value and applies f to the value n times.
Using the Church encoding, you can define operations on the numbers as well. In this case, you're interested in plus, which takes two numbers and returns a number
plus ≡ λm.λn.λf.λx.???
So what's in the body? Well, the body has to be n + m applications of f to the value x. If we pass f and x to n, we get n applications–call that r, and if we apply m to f and r, that'll be m + n applications of f:
plus ≡ λm.λn.λf.λx.m f (n f x)
So the expression 2 + 2 using this encoding is:
plus 2 2 ≡ (λm.λn.λf.λx.m f (n f x)) (λf.λx.f (f x)) (λf.λx.f (f x))
Now β-reduce until you get the result:
plus 2 2 ≡ (λm.λn.λf.λx.m f (n f x)) (λf.λx.f (f x)) (λf.λx.f (f x))
↦ (λn.λf.λx.(λf.λx.f (f x)) f (n f x)) (λf.λx.f (f x))
↦ (λf.λx.(λf.λx.f (f x)) f ((λf.λx.f (f x)) f x))
↦ (λf.λx.(λx.f (f x)) ((λf.λx.f (f x)) f x))
↦ (λf.λx.(λx.f (f x)) ((λx.f (f x)) x))
↦ (λf.λx.(λx.f (f x)) (f (f x)))
↦ (λf.λx.f (f (f (f x
≡ 4.
But now, let's bust out of this theoretical prison and say we have a number 0 in some representation that we can actually work with, as well as a function add1 that knows how to increment a number in that representation. Well, then we can get a useable representation out of our church numeral, by applying to the numeral to add1 and the value:
4 add1 0 = 4
