'K' is for Kappa-calculus

'K' is for κ-calculus

This is an epic story of epic epicness!

No, really.

So, way back when, this guy named Church (Alonzo was his Christian name, and he liked going to churches)

(Actually, that's just conjecture on my part.)

Okay, everybody, stop everything and go to this wikipedia link on the Frege-Church ontology, right now.

Have you read it?

Well, what are you waiting for, read the post, for goodness sake!

I'M WAITING!

...

Okay.

So, I read the post, and I was all like skyr, you know? No whey!

Like, totally! Like. I mean, like, wikipedia, wrote that?

So, I quizzed my girls:

"Girls!" I shouted excitedly, "What's the farthest planet from the Sun?"

They were like, "Whaaaaa?"

Then they asked, like, "Papa!" with arched eyebrows, "why do you want to know what's the farthest plant from the Sun?"

Hm. I, like, have to work on my, like, diction.

(We'll get to the reason behind the paroxysms of 'like's momentarily.)

So, I clarified, "Planet, planet!" I shouted, "What's the farthest planet from the Sun!"

EM, the older, and therefore smarter one (she has to be, you see), said, "Pluto. No, wait. Pluto's not a planet. Neptune, then!"

"HAAAAAA!" I screamed.

Elena Marie looked at me like her Papa had finally gone off the deep end.

Well, finally off the deep end, but this time, never to return, gone-off-the-deep kind-of-way.

But before I could explain my victorious berserker scream ...

(Berserker, n.: etymology: íslandic, "Bear Skinned")

(Question: what is the etymology of the word 'etymology'?)

(Did you know Icelandic is an insular Nordic language? They can read the poetic and prose eddas straight off, just like that. Could you read a 1,000 year old document? No, you can't, unless your an Icelander. So there.)

(But I digress.)

(As always.)

(The neat thing here, is this is a digression, from a digression! And it's not even leading us back to the topic, but further away) (just as this digressionary turn discussing my digressionary habits).

(Digressions within digressions within digressions.) (Move over, Frank Herbert, you dead old guy, you're not the only one who can write 'Wheels within wheels within wheels' and have a really bad movie with a Sting cameo made out of your book!)

BUT BEFORE I COULD EXPLAIN my berserker-scream, Li'l Iz piped right up.

"How can you know what's the farthest planet of the Sun, huh, Papa? There're other planets in this galaxy, and what about other galaxies, huh?"

She had me there. But never confuse the point you're trying to make with facts.

WHEN I REREAD what I wrote to my girls, they sighed, appreciatively, EM said, "How ironic can that be?" and walked off to her room to read another book before her ballet recital in forty-five minutes.

I asked Li'l Iz, "Was that, like, ironic?"

She rolled her eyes and deigned not to answer, returning to her own book.

SO, the POINT of all this is:

Pluto is not a planet!

Whew!

I'm so glad that the ravings of a madman in Borderlands 2 would actually have significance to mathematical logic theory. The things one learns by reading blogposts by the geophfmeister.

(That is moi-self) (That is French) (No, it's not.)

Ooh! Digression!

When I was working with some Ph.D.'s and cognitive scientists, I worked with this flaming-red-haired dude (cognitive scientist) named Bill. He would always say 'Gratzi' to people answering his questions, I would always respond: "That is French."

He always gave me weird looks, but he never got the nerve to correct me.

Until one day, he said 'Gratzi' to one of our analysts, and I said, 'That is French.'

She looked me dead in the eye and snarled a disdainful, "Who cares?" before stalking off.

Bill was on the floor, suffering a paroxysm of laugher.

I think that was the best day of his life.

ANYWAY!

Pluto, not planet ... It's not even a plant.

Besides which, Eris is more massive than Pluto, anyway. So there.

Hail, Eris!

SO!

The Lambda calculus ('L' is for Lambda calculus) addressed a certain set of concerns, which I'll get to in Monday's post, but it, like mathematics in general, has its own set of problems, that is, you can write a function that never terminates and so it is undecidable.

So, along came this little kid by the name of Masahito Hasegawa (dunno, maybe he's Italian?) and he noticed something, and that was this: the problem of the lambda calculus is that it's actually two calculi intertwined. And when you disentangle them, you have two distinct calculi, neither of which are undecidable.

The first of the calculi, the one we focus on here, is the κ-calculus, or contextual calculus.

The κ-calculus is this.

The types are pairs of unit types:

τ : 1|τ x τ|...

So, you see from the types that it's either nothing (the 1, or unit type) or it's a (crossed, or cartesian product) of types.

The functions only take these types, NOT functional types, so we're safe in that we're only working with unit types.

The primary operation is the lifting function, which takes an instance and lifts it into the type of concern.

liftτ x -> (a, x) where a is of type τ

Then the κ-abstraction that when acting with an instance carries it along:

κ x . (some function (τ1, τ2) -> τ3) : τ3

Tying lift and the κ-abstraction together gives us our function 'application' where actually no application happens, it's all just composing (in this case) tuples.