Originally, I was going to use this writeup to describe what I thought were two unrelated meanings of the letter K in mathematics. However, after more research, I realised that the two meanings are in fact deeply and inextricably linked. More on that later; first, here are the two meanings.
In the early- to mid-20th century, mathematicians, for the first time, started to analyze the expressiveness and power of maths itself. In order to do this, they needed a model of computation which could then be used to reason about the very language it was expressed in. There were a number of different approaches, Alan Turing with his machines, Marvin Minsky with his machines, Andrei Markov with his algorithms but most importantly to us, Alonzo Church's Lambda calculus. Lambda calculus is basically a convenient way to express and apply functions. It was used to reason about computation where we only had functions available to us in our mathematical vocabulary.
Combinators are used as a set of basic functions in the lambda calculus, taken as given, so that more complex expressions can be written in terms of atomic building blocks. K is one of these combinators. Intuitively it accepts two arguments, ignores the second one and returns the first one. A few more formal descriptions:
or in
lambda calculus:
or in
ML:
fun K x y = x;
I have reservations giving C-style code due to the lack of type polymorphism.
Although this combinator seems incredibly simple and weedy, when used in conjunction with other combinators, such as S, and function application, it becomes very powerful.
In propositional logic, K is a standard axiom which a lot of proofs rely on.
Where → signifies inference.
This axiom can be shown to be valid from the truth table of the statements.
A | B | A → (B → A)
---+---+-------------
t | t | t
t | f | t
f | t | t
f | f | t
Again, this axiom seems obvious and useless. However, when combined with other axioms and Modus Ponens, K becomes an essential part of intuitionistic logic.
The Connection
The similarity between the two Ks became apparent when I was putting the ML code fragment into an interpreter. The type it gave for fun K x y was
val K = fn : 'a -> 'b -> 'a
The similarity between this and the logic axiom is striking
It turns out that this is no coincidence. A very deep result known as the Curry-Howard Isomorphism establishes direct correspondence between such seeminly diverse fields as second-order logic and polymorphic types, and importantly to us, minimal propositional logic and lambda calculus.
As the ML fragment given above is simply-typed lambda calculus in essence, it should be no surprise that there is such a direct connection between the K axiom and its related combinator's type.
NB, this does not mean that propositional logic is Turing complete, as lambda calculus is. It is the types of lambda expressions that are relevant, not the programmes themselves.