A little κ-calculus conversation

So, "wan plas wan is doo" in the κ-calculus. Because why? Because if you can prove addition in some calculus, you can prove anything.

Well, prove any primitively-recursive thing in that calculus, and that's good enough for most anything (except Ackermann and some others), which is close enough to a latte at Caribou café for me.

SO! without further ado: 1 + 1 = 2, κ-style.

First of all, some basics. What is the κ-calculus?

κ-calc: application is composition: 

f: A → B is κ x . f : (C x A) → B

and the lifting ('identity') function

C : 1 → C is lift : A → (C x A)

Then, for addition we need the category Nat and the following arrows:

0 : 1 → Nat; and,       (so, 0 ~> 0)

succ : Nat → Nat         (so, succ o succ o 0 ~> "2")

but we also need the iterator function for natural numbers:

(a) it(a, f) o 0 ~> a; and

(b) it(a, f) o succ o n ~> f o it(a, f) o n

from this we can declare the function add in the κ-calculus:

add : Nat x Nat → Nat ≡ (κ x . it(x, succ))

Note how we don't care what the second (snd) argument of the tuple is, we just iterate succ over it, so with add defined above we can now prove 1 + 1 = 2

add o (succ o 0, succ o 0) = (κ x . it(x, succ)) o lift (succ o 0) o succ o 0 (lift distribution)

= it(x, succ)[succ o 0] o succ o 0 (composition)

= it(x [succ o 0/x], succ [succ o 0/x]) o succ o 0 (substitution)

= it(succ o 0, succ) o succ o 0 (substitution)

= succ o (it(succ o 0, succ) o 0) (iteration (b))

= succ o (succ o 0) = 2 (iteration (a))

Q.E.D.

Piece of cake, right? Using categories (for types), we reduce 200 pages of the Principia Mathematica down to a couple of axioms, a couple of types and one function (it), then a few lines of proof and we're done.

Awesomesauce!

But then, my daughters became curious about what the Papa was doing, so this conversation ensued with my 10-year-old.

"But, Papa," Li'l Iz asked with big-big eyes, "what does snd have to do with 2?"

So, I explained.

A tuple is of the form: (a, b)

So for example we have: (3, 4)

So the tupling functions are:

fst (3, 4) ~> 3

snd (3, 4) ~> 4

And therefore for the tuple (1,1)

fst (1, 1) ~> 1

snd (1, 1) ~> 1

So, to prove 1 + 1 = 2 we thence have:

add o (1, 1)

Therefore:

fst (1, 1) o add o snd (1, 1) = 2 

and that's why snd (1, 1) has everything to do with 2. :p

wa, wa, waaaaaaaa (this my daughter wrote)