Originally Posted by Takyon

2+2 is 5.4 - 2

Originally Posted by ryuu

You forget to ignore friction

Originally Posted by ymir

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

Originally Posted by Jumping22

Me and the Boys ordering a milkshake from Femboy Hooters;

Originally Posted by ymir

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