Curry-Howard Correspondence: Linking Computer Science and Mathematical Logic

Sunday - October 15 2023, 09:13 UTC - 1 year ago

The Curry-Howard correspondence links computer science and mathematical logic by showing that two concepts from computer science, types and programs, are equivalent respectively to propositions and proofs from logic. It is a profound discovery that has many applications such as proof assistants, formal verification systems, and computer algebra systems.

Some scientific discoveries matter because they reveal something new — the double helical structure of DNA, for example, or the existence of black holes. However, some revelations are profound because they show that two old concepts, once thought distinct, are in fact the same. Take James Clerk Maxwell’s equations showing that electricity and magnetism are two aspects of a single phenomenon, or general relativity’s linking of gravity with a curved space-time.

The Curry-Howard correspondence does the same but on a larger scale, linking not just separate concepts within one field, but entire disciplines: computer science and mathematical logic. Also known as the Curry-Howard isomorphism (a term meaning there exists some kind of one-to-one correspondence between two things), it establishes a link between mathematical proofs and computer programs.

Simply stated, the Curry-Howard correspondence posits that two concepts from computer science (types and programs) are equivalent, respectively, to propositions and proofs — concepts from logic.

One ramification of this correspondence is that programming — often seen as a personal craft — is elevated to the idealized level of mathematics. Writing a program is not just "coding," it becomes an act of proving a theorem. This formalizes the act of programming and provides ways to reason mathematically about the correctness of programs.

The correspondence is named for the two researchers who independently discovered it. In 1934, the mathematician and logician Haskell Curry noticed a similarity between functions in mathematics and the implication relationship in logic, which takes the form of "if-then" statements between two propositions.Inspired by Curry’s observation, the mathematical logician William Alvin Howard discovered a deeper link between computation and logic in 1969, showing that running a computer program is a lot like simplifying a logical proof. When a computer program runs, each line is "evaluated" to yield a single output. Similarly, in a proof, you start with complex statements that you can simplify (by eliminating redundant steps, for example, or substituting complex expressions with simpler ones) until you arrive at a conclusion — a more condensed and succinct statement derived from many interim statements.

While this description conveys a general sense of the correspondence, to fully understand it we need to learn a bit more about what computer scientists call "type theory." .

Let’s start with a famous paradox: In a village there lives a barber who shaves all the men who do not shave themselves, and only them. Does the barber shave himself? If the answer is yes, then he must not shave himself (because he only shaves men who don’t shave themselves). If the answer is no, then he must shave himself (because he shaves all the men who don’t shave themselves). This is an informal version of a paradox Bertrand Russell discovered while trying to establish the foundations of mathematics using a concept called sets. That is, it’s impossible to define a set that contains all sets that do not contain themselves without encountering contradictions.

To avoid this paradox, an alternative approach has been taken to define sets, which is called type theory. In type theory, sets are defined as types and the barber paradox can be sidestepped by saying that a man who shaves himself is of two types simultaneously — "male" and "not male." Plus, this approach results in a lighthearted application of types — humor and satire.

The Curry-Howard correspondence is a profound discovery linking two enormous concepts in computer science and mathematics. It elevates programming to the level of proof, adds ability for mathematical reasoning about program correctness, and allows for further applications such as proof assistants, formal verification systems, and computer algebra systems.