Proposition as Types informs our view of the universality of certain
programming languages.
The Pioneer spaceship contains a plaque designed to communicate with aliens, if any should ever intercept it. They
may find some parts of it easier to interpret than others. A radial diagram shows the distance of fourteen pulsars and the centre of the
galaxy from Sol. Aliens are likely to determine that the length of
each line is proportional to the distances to each body. Another diagram shows humans in front of a silhouette of Pioneer. If Star Trek
gives an accurate conception of alien species, they may respond
“They look just like us, except they lack pubic hair.” However, if
the aliens’s perceptual system differs greatly from our own, they
may be unable to decipher these squiggles.
What would happen if we tried to communicate with aliens by
transmitting a computer program? In the movie Independence Day,
the heroes destroy the invading alien mother ship by infecting it
with a computer virus. Close inspection of the transmitted program
shows it contains curly braces—it is written in a dialect of C! It
is unlikely that alien species would program in C, and unclear that
aliens could decipher a program written in C if presented with one.
What about lambda calculus? Propositions as Types tell us that
lambda calculus is isomorphic to natural deduction. It seems difficult to conceive of alien beings that do not know the fundamentals
of logic, and we might expect the problem of deciphering a program written in lambda calculus to be closer to the problem of understanding the radial diagram of pulsars than that of understanding
the image of a man and a woman on the Pioneer plaque.
We might be tempted to conclude that lambda calculus is universal, but first let’s ponder the suitability of the word ‘universal’.
These days the multiple worlds interpretation of quantum physics
is widely accepted. Scientists imagine that in different universes
one might encounter different fundamental constants, such as the
strength of gravity or the Planck constant. But easy as it may be to
imagine a universe where gravity differs, it is difficult to conceive
of a universe where fundamental rules of logic fail to apply. Natural
deduction, and hence lambda calculus, should not only be known
by aliens throughout our universe, but also throughout others. So
we may conclude it would be a mistake to characterise lambda calculus as a universal language, because calling it universal would be
too limiting.