The deep connection between mathematical logic and computer program code: mirror images of each other

Some scientific discoveries are given great significance because they reveal something new, such as the double helix structure of DNA or the existence of black holes. But these revelations have a deeper meaning, because they show that two old concepts that previously seemed very different are actually the same. For example, the system of equations discovered by James Clerk Maxwell showed that electricity and magnetism are two different aspects of the same phenomenon, while general relativity linked gravity to the curved space-time.

The same is true for Curry-Howard correspondence, and it relates not just two different concepts in one field, but two complete disciplines: Computer Science and Mathematical Logic. This correspondence is also known as Curry-Howard isomorphism (isomorphism refers to a certain one-to-one correspondence between two things), which establishes a certain connection between mathematical proofs and computer programs. .

Simply put, Curry-Howard believes that two concepts in computer science (type and program) are equivalent to two concepts in logic (proposition and proof). ).

One result of this correspondence is that program development has been elevated to an idealized mathematical level, whereas before people usually thought that program development was just a manual job. Program development is not just about "writing code", it has become the act of proving theorems. This formalizes the behavior of program development and provides a way to mathematically reason about program correctness.

The name of this correspondence comes from two researchers, who independently discovered this correspondence. In 1934, mathematician and logician Haskell Curry noticed the similarity between functions in mathematics and the implication relationship in logic. The form of an implication relation is an "if-then" statement between two propositions.

Inspired by Currie's observations, mathematical logician William Alvin Howard discovered in 1969 that there was a deeper connection between computation and logic. correlation; his research showed that running a computer program is much like simplifying logical proofs. When you run a computer program, each line of code is "evaluated" to produce an output. Similarly, when working on a proof, you start with a complex statement and then simplify it (for example, by eliminating redundant steps or replacing complex expressions with simpler ones) until you reach some conclusion - from many A transitional statement leads to a more concise statement.

While this description gives a rough idea of ​​what this correspondence means, fully understanding it requires learning more about what computer scientists call "type theory." .

Let us start with a famous paradox: There was a barber in a village who shaved and only shaved all those who did not shave themselves. So does this barber shave himself? If the answer is yes, then he must not shave himself (because he only shaves for people who do not shave himself). If the answer is no, then he must shave himself (because he shaves everyone who does not shave himself). This is an informal version of a paradox discovered by Bertrand Russell when he was trying to form the basis of mathematics using a concept called sets. That is to say: it is impossible to define a set that contains all sets that do not contain itself, and contradictions will inevitably occur in this process.

Russell's research shows that in order to avoid this paradox, we can use types. Roughly speaking, types are categories whose concrete values ​​are called objects. For example, if there is a type Nat representing natural numbers, then its objects are 1, 2, 3, and so on. Researchers often use colons to indicate the type of object. For example, for the integer type value 7, it can be written as "7: Integer". We can use a function to convert an object of type A into an object of type B, or we can use a function to combine two objects of types A and B into a new object of type "A×B".

So, one way to resolve this paradox is to layer these types so that they only contain elements one level below themselves. Then a type cannot contain itself, which avoids the self-reference that creates the above paradox.

In the world of type theory, the process of proving a statement to be true may differ from what we are used to. If we want to prove that the integer 8 is even, then the key to the problem is to prove that 8 is actually an object of the "even" type, and the rule of this type defines that the elements are divisible by 2. After verifying that 8 is divisible by 2, we can conclude that 8 is a "resident" of the "even" type.

Currie and Howard proved that types are fundamentally equivalent to logical propositions. When a function "inhabit" a certain type, that is, when the function is an object of that type, we can effectively prove that the corresponding proposition is true. Therefore, a function that takes an object of type A as input and an object of type B as output (denoted as type A → B) must correspond to an implication: "If A, then B." For example, suppose there is the proposition "If If it rains, then the ground is wet." In type theory, this proposition would be modeled as a function of the type "rain → ground is wet". These two representations look different, but are mathematically the same.

Although this connection may seem abstract, it not only changes the way practitioners of mathematics and computer science think about their work, but also brings some insights to both fields. Practical applications. In computer science, this connection provides a theoretical foundation for software verification, the process of ensuring software correctness. By describing desired behavior in terms of logical propositions, program developers can mathematically prove whether a program behaves as expected. And this connection also provides a solid theoretical foundation for designing more powerful functional programming languages.

In the field of mathematics, this correspondence has given rise to the proof assistant tool, also known as the interactive theorem prover. These software tools can assist in building formal proofs, examples include Coq and Lean. In Coq, each proof step is essentially a program, and the validity of the proof is checked through a type checking algorithm. Mathematicians have also been using proof assistants (especially Lean theorem provers) to formalize mathematics, which involves representing mathematical concepts, theorems, and proofs in a rigorous format that can be verified by a computer. This allows sometimes informal mathematical language to be tested by computers.

Researchers are also exploring the potential outcomes of this connection between mathematics and programming. The original Curry-Howard correspondence united program development with a type of logic called intuitionistic logic, but it turns out that there are many more types of logic that can be unified.

Cornell University computer scientist Michael Clarkson said: "In the century since Currie derived his insights, we have continued to discover more and more 'logical systems An instance of System Y." Researchers have also linked programming to other types of logic, such as linear logic, which involves the concept of "resources," and modal logic, which involves the concepts of possibility and necessity.

And although this correspondence bears the name of Currie and Howard, they are by no means the only discoverers of this correspondence. This demonstrates a fundamental nature of this correspondence: people notice it over and over again. Clarkson said: "The deep connection between computing and logic does not seem to be accidental."

The above is the detailed content of The deep connection between mathematical logic and computer program code: mirror images of each other. For more information, please follow other related articles on the PHP Chinese website!