Curry–Howard correspondence(en.wikipedia.org)
en.wikipedia.org
Curry–Howard correspondence
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
22 comments
I've always been intrigued by, but never delved deeply enough into the depths of the more mathematical sides of programming. I've always wondered is there a good mathematical representation of an algorithm that is useful for algebraic manipulation? For example:
Take an ugly equation like: x^2 + 3x+y+2+(−x)^2 = 3+(−x)^2 . It can be transformed to either (x+1)(x+2)-3 = y or y=−x^2−3x+1 fairly cleanly and usefully with just a few algebraic theorems. I remove redundancy among other things.
Can I take "bubble sort" work my way in steps to produce a "quick sort" or a "merge sort"? Sure you could prove they produce identical results but it doesn't feel like you're bridging that gap. Maybe this is too vague a question.
Take an ugly equation like: x^2 + 3x+y+2+(−x)^2 = 3+(−x)^2 . It can be transformed to either (x+1)(x+2)-3 = y or y=−x^2−3x+1 fairly cleanly and usefully with just a few algebraic theorems. I remove redundancy among other things.
Can I take "bubble sort" work my way in steps to produce a "quick sort" or a "merge sort"? Sure you could prove they produce identical results but it doesn't feel like you're bridging that gap. Maybe this is too vague a question.
The answer is surprisingly yes!
It's usually called equational reasoning or Bird–Meertens formalism.
Transforming an insertion sort into merge sort is covered in Section 5 of "FUNCTIONAL PEARLS The Third Homomorphism Theorem":
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45....
It's usually called equational reasoning or Bird–Meertens formalism.
Transforming an insertion sort into merge sort is covered in Section 5 of "FUNCTIONAL PEARLS The Third Homomorphism Theorem":
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45....
I can't begin to explain how excited I am to delve into this! Thank you for the lead.
You can have a look at Richard Bird's book _Pearls of Functional Algorithm Design_. It's much more accessible than his earlier influential book _Algebra of Programming_.
In this book, many well-known algorithms, e.g. KMP pattern matching, are derived from naive implementations by step-by-step applications of algebraic rules of (functional) programs.
In this book, many well-known algorithms, e.g. KMP pattern matching, are derived from naive implementations by step-by-step applications of algebraic rules of (functional) programs.
Thanks!
Related to your last question, I was always puzzled by the following: when is a program an implementation of an (abstract) algorithm?
For example, can a program decide, given a sorting function implemented in language X, and an algorithm Y, whether or not the sorting function is an implementation of algorithm Y? Part of the question is how to represent algorithms (is "formal" pseudo-code the best way?)
Also, can you decide whether or not two functions written in different programming languages are implementations of the same algorithm?
For example, can a program decide, given a sorting function implemented in language X, and an algorithm Y, whether or not the sorting function is an implementation of algorithm Y? Part of the question is how to represent algorithms (is "formal" pseudo-code the best way?)
Also, can you decide whether or not two functions written in different programming languages are implementations of the same algorithm?
> For example, can a program decide, given a sorting function implemented in language X, and an algorithm Y, whether or not the sorting function is an implementation of algorithm Y?
Assuming the usual things (e.g. that an algorithm Y can be specified in some useful, say, very high level language) then this problem is Halting-hard (e.g. at least as hard as the halting problem), because it would be showing the equivalence of two programs. A similar case applies to your latter question.
I'm not sure there's a good way of specifying abstract algorithms without running into this problem, but I'd be interested in defining a bit further what you might be thinking about.
Assuming the usual things (e.g. that an algorithm Y can be specified in some useful, say, very high level language) then this problem is Halting-hard (e.g. at least as hard as the halting problem), because it would be showing the equivalence of two programs. A similar case applies to your latter question.
I'm not sure there's a good way of specifying abstract algorithms without running into this problem, but I'd be interested in defining a bit further what you might be thinking about.
Yes, in general it is obviously undecidable.
I should have been clearer, but I'm mostly interested in structure (traversal) algorithms, most of which could be coded in a language with bounded loops.
An easier question is the one of determining the complexity of an algorithm. I think there's a ton of work in this area, for example in techniques that use typing systems (types may for example specify how many times a parameter is used, thus allowing the program to infer the complexity).
(easier because the equivalence relation of "implementing the same algorithm" is strictly finer than "having the same complexity")
I should have been clearer, but I'm mostly interested in structure (traversal) algorithms, most of which could be coded in a language with bounded loops.
An easier question is the one of determining the complexity of an algorithm. I think there's a ton of work in this area, for example in techniques that use typing systems (types may for example specify how many times a parameter is used, thus allowing the program to infer the complexity).
(easier because the equivalence relation of "implementing the same algorithm" is strictly finer than "having the same complexity")
No you can't really, not that this has much to do with Curry-Howard.
Bubble sort and Quicksort only resemble each other in so much as the result is sorted. All of the other steps are completely different, meaning the abstract shapes of the intermediate computations are very different.
Bubble sort and Quicksort only resemble each other in so much as the result is sorted. All of the other steps are completely different, meaning the abstract shapes of the intermediate computations are very different.
Professor Philip Wadler has a fantastic talk titled "Propositions as Types" that introduces the Curry-Howard correspondence, some history behind it and ideas following it.
In fact it's one of my favorite talks. Well worth a watch if you haven't seen it: https://www.youtube.com/watch?v=IOiZatlZtGU&t=1s
In fact it's one of my favorite talks. Well worth a watch if you haven't seen it: https://www.youtube.com/watch?v=IOiZatlZtGU&t=1s
So proofs and programs are isomorphic. We know there are programs which never halt and we know there are programs for which we can not algorithmically decide whether they halt or not. What is the equivalent thing in proofs? Are there proofs which never halt?
Is a proof really isomorphic with a program as written in source-code, or is it isomorphic with the EXECUTION of a program with a given input?
A program and its execution are not the same thing are they? But with proofs I find it hard to think about the difference between the "source-code" of a proof and the "execution" of a proof. Is there such a thing as distinction between the execution of a proof and the "source-code" of it?
Is a proof really isomorphic with a program as written in source-code, or is it isomorphic with the EXECUTION of a program with a given input?
A program and its execution are not the same thing are they? But with proofs I find it hard to think about the difference between the "source-code" of a proof and the "execution" of a proof. Is there such a thing as distinction between the execution of a proof and the "source-code" of it?
General recursion in programs (that makes termination undecidable) requires a fix-point operator of type (a -> a) -> a
The logical equivalent of this is an axiom (P -> P) -> P which lets you prove anything. So non-termination in a programming language corresponds to being able to prove anything - including False - in the logic.
The logical equivalent of this is an axiom (P -> P) -> P which lets you prove anything. So non-termination in a programming language corresponds to being able to prove anything - including False - in the logic.
> So proofs and programs are isomorphic. We know there are programs which never halt and we know there are programs for which we can not algorithmically decide whether they halt or not. What is the equivalent thing in proofs? Are there proofs which never halt?
Yes; a "proof which never halts" is an invalid attempt at a proof (so not really a proof).
To a first approximation, the Curry–Howard correspondence says that programming and proving are the same. This is literally true if "programming" and "proving" are restricted to mean more specific things. (There are many variants of the Curry–Howard correspondence. The simplest one relates "simply-typed lambda calculus" with "propositional intuitionistic logic". Simply-typed lambda calculus is basically what you get when you take Python, strip everything away except for the keyword "lambda", and add types. Intuitionistic propositional logic is basically what you get when you take ordinary logical reasoning, strip away quantifiers ("for all", "there exists") and force yourself to never use proof by contradiction. There are also variants for more powerful programming languages and more powerful logics. The case of classical logic, where we can use proof by contradiction, is particularly interesting, since the translations of such proofs make use of continuations. See https://rawgit.com/iblech/talk-constructive-mathematics/mast...) But in a wider sense it's false: Invalid proves aren't very much worthwhile, while non-terminating programs can be. Thus a better approximation is "programming strictly encompasses proving".
> Is a proof really isomorphic with a program as written in source-code, or is it isomorphic with the EXECUTION of a program with a given input?
The former.
> A program and its execution are not the same thing are they?
Correct. A program is a piece of a text. Its execution is (for me, in this context) the final value computed by the program. (The Curry–Howard correspondence is easiest to understand when we restrict to programs in a purely-functional programming language like Haskell.)
> But with proofs I find it hard to think about the difference between the "source-code" of a proof and the "execution" of a proof. Is there such a thing as distinction between the execution of a proof and the "source-code" of it?
I'm with you; the reason the difference is hard to see is because while we run programs all the time, we almost never run proofs. However, yes, indeed, you can run proofs. The result will be a "proof certificate", something like a proof with all intermediate definitions unrolled and then maximally simplified.
Quite different-looking proofs (texts) can yield the same "proof certificate" when ran, exactly as different-looking source codes can yield the same final value when ran.
Here is an example. Consider the following proof (due to Euclid) of the fact that there is a prime number greater than 6: "Like any positive natural number, the number N = 1⋅2⋅3⋅4⋅5⋅6 + 1 is a product of prime numbers. However, no number between 2 and 6 is a factor of N, since dividing N by any such number will always leave a remainder of one. Hence all the prime factors of N, for definiteness pick the smallest one, are prime numbers greater than 6." The proof certificate obtained by running this proof will be the pair (7,...), where "..." is a certificate that the number 7 is indeed prime. The reason the number 7 appears here is because 1⋅2⋅3⋅4⋅5⋅6 + 1 = 721 = 7 * 103. If the proof picked the largest factor instead of the smallest, the result of the proof would be the pair (103,...) (with a different primality certificate).
Running proofs is becoming a more important thing nowadays, thanks to the development of good proof assistants and homotopy type theory. (While in principle it's possible run proofs manually, like in the previous paragraph, it's only fun when a computer does it for you.) For instance, a mathematician might prove that some particular structure of interest only contains finitely many elements, without having a clue how many values there are. If she runs the proof, the computer will tell her the answer. The catch is that with current (mathematical) technology, she might have to wait quite a bit for the answer. (The in my circles famous "Brunerie two" comes to mind: This is a proof where we know the answer to be the number 2, and made much progress in pimping the Curry–Howard correspondence, but aren't quite there yet. See https://guillaumebrunerie.github.io/pdf/cubicalexperiments.p...)
Yes; a "proof which never halts" is an invalid attempt at a proof (so not really a proof).
To a first approximation, the Curry–Howard correspondence says that programming and proving are the same. This is literally true if "programming" and "proving" are restricted to mean more specific things. (There are many variants of the Curry–Howard correspondence. The simplest one relates "simply-typed lambda calculus" with "propositional intuitionistic logic". Simply-typed lambda calculus is basically what you get when you take Python, strip everything away except for the keyword "lambda", and add types. Intuitionistic propositional logic is basically what you get when you take ordinary logical reasoning, strip away quantifiers ("for all", "there exists") and force yourself to never use proof by contradiction. There are also variants for more powerful programming languages and more powerful logics. The case of classical logic, where we can use proof by contradiction, is particularly interesting, since the translations of such proofs make use of continuations. See https://rawgit.com/iblech/talk-constructive-mathematics/mast...) But in a wider sense it's false: Invalid proves aren't very much worthwhile, while non-terminating programs can be. Thus a better approximation is "programming strictly encompasses proving".
> Is a proof really isomorphic with a program as written in source-code, or is it isomorphic with the EXECUTION of a program with a given input?
The former.
> A program and its execution are not the same thing are they?
Correct. A program is a piece of a text. Its execution is (for me, in this context) the final value computed by the program. (The Curry–Howard correspondence is easiest to understand when we restrict to programs in a purely-functional programming language like Haskell.)
> But with proofs I find it hard to think about the difference between the "source-code" of a proof and the "execution" of a proof. Is there such a thing as distinction between the execution of a proof and the "source-code" of it?
I'm with you; the reason the difference is hard to see is because while we run programs all the time, we almost never run proofs. However, yes, indeed, you can run proofs. The result will be a "proof certificate", something like a proof with all intermediate definitions unrolled and then maximally simplified.
Quite different-looking proofs (texts) can yield the same "proof certificate" when ran, exactly as different-looking source codes can yield the same final value when ran.
Here is an example. Consider the following proof (due to Euclid) of the fact that there is a prime number greater than 6: "Like any positive natural number, the number N = 1⋅2⋅3⋅4⋅5⋅6 + 1 is a product of prime numbers. However, no number between 2 and 6 is a factor of N, since dividing N by any such number will always leave a remainder of one. Hence all the prime factors of N, for definiteness pick the smallest one, are prime numbers greater than 6." The proof certificate obtained by running this proof will be the pair (7,...), where "..." is a certificate that the number 7 is indeed prime. The reason the number 7 appears here is because 1⋅2⋅3⋅4⋅5⋅6 + 1 = 721 = 7 * 103. If the proof picked the largest factor instead of the smallest, the result of the proof would be the pair (103,...) (with a different primality certificate).
Running proofs is becoming a more important thing nowadays, thanks to the development of good proof assistants and homotopy type theory. (While in principle it's possible run proofs manually, like in the previous paragraph, it's only fun when a computer does it for you.) For instance, a mathematician might prove that some particular structure of interest only contains finitely many elements, without having a clue how many values there are. If she runs the proof, the computer will tell her the answer. The catch is that with current (mathematical) technology, she might have to wait quite a bit for the answer. (The in my circles famous "Brunerie two" comes to mind: This is a proof where we know the answer to be the number 2, and made much progress in pimping the Curry–Howard correspondence, but aren't quite there yet. See https://guillaumebrunerie.github.io/pdf/cubicalexperiments.p...)
Thanks for great explanation.
> A program is a piece of a text.
But, a program is more than a text, it is a structure, parsed from text with the rules of the language .
Still I think I'm beginning to see the correspondence.
Execution of the program is when we give it some input and run it. So there would be similarly an input to proofs. Proof would need to be "proven correct" for EVERY valid input, that is what compiler does for programs, proving the result of the program must be of its declared result-type.
But a proof which proves anything is not really a proof as said by someone, it corresponds to a non-halting program. So in this sense doesn't a proof ALWAYS require that we "run" it, to prove that it terminates, and thus is a valid proof actually?
Does this require some meta-logic? Proving that a proof terminates? :-)
> A program is a piece of a text.
But, a program is more than a text, it is a structure, parsed from text with the rules of the language .
Still I think I'm beginning to see the correspondence.
Execution of the program is when we give it some input and run it. So there would be similarly an input to proofs. Proof would need to be "proven correct" for EVERY valid input, that is what compiler does for programs, proving the result of the program must be of its declared result-type.
But a proof which proves anything is not really a proof as said by someone, it corresponds to a non-halting program. So in this sense doesn't a proof ALWAYS require that we "run" it, to prove that it terminates, and thus is a valid proof actually?
Does this require some meta-logic? Proving that a proof terminates? :-)
> > A program is a piece of a text.
> But, a program is more than a text, it is a structure, parsed from text with the rules of the language .
Yes, you are right. By "text" I actually meant "term" or "abstract syntax tree".
> Execution of the program is when we give it some input and run it. So there would be similarly an input to proofs. Proof would need to be "proven correct" for EVERY valid input, that is what compiler does for programs, proving the result of the program must be of its declared result-type.
Not necessarily, not all programs require input and similarly not all proofs require input. But yes, for most cases you're right: Just as the program "output a prime number larger than <>" requires an input, so does a proof of the statement "there is a prime number larger than <>".
> But a proof which proves anything is not really a proof as said by someone, it corresponds to a non-halting program. So in this sense doesn't a proof ALWAYS require that we "run" it, to prove that it terminates, and thus is a valid proof actually?
Indeed, in general, running a proof and observing that it terminates is one way to ensure that it's a valid proof. However, all the proof systems (logics) used in mathematical practice correspond, under Curry–Howard correspondence, to programming languages in which any well-typed program terminates. (These programming languages are therefore in some sense quite impoverished; they are definitely not Turing-complete. However they are still rich enough to interpret all of mathematics!) Thus to ensure that a proof is valid it suffices to ensure that the corresponding program is well-typed. For the traditional proof systems used in mathematics (e.g. Zermelo–Fraenkel set theory), this is decidable, that is, it's easy to write a proof checker. For newer proof systems (e.g. homotopy type theory) the same holds, but type inference might not be decidable; therefore we declare that in order to give a full proof one also has to give all the types.
> Does this require some meta-logic? Proving that a proof terminates? :-)
Indeed! One possible choice for the meta-logic is "common human reasoning". Of course this is not formal, so the usual problems with informal reasoning apply. A popular alternative is PRA, "primitive-recursive arithmetic". All standard results you'll find in logics textbooks, such as Gödel's incompleteness phenomena or the Curry–Howard correspondence, can be formalized and proven within PRA. The reason why PRA is well-suited to study logical systems is because PRA itself is very weak, that is, easy to trust. In contrast, the usual logical systems used in mathematics are quite powerful, therefore conceivably (though extremely unlikely) inconsistent.
In case you'd like me to upgrade "extremely unlikely" to "provably", then I have bad news for you: PRA proves that if (PRA is able to prove that any of the standard systems is consistent), then (PRA is inconsistent). So there are just two options: Either PRA itself cannot be trusted, in which case all hell breaks lose (http://spikedmath.com/183.html); or PRA is trustworthy, in which case PRA is not inconsistent, in which case we know that PRA is not able to verify the consistency of any of the usual proof systems. (In this analysis, I'm assuming the law of excluded middle. Without it, it's not clear that these two options are the only ones.)
If you enjoyed the movie Inception, then you'll appreciate that we need a meta-meta-logic in order to talk about correctness of proofs formulated in PRA. This meta-meta-logic is almost always taken to be "common human reasoning". It could be substituted for a more formal version, for instance PRA again, but at some meta level you have to stop anyway and fall back to informality, so most logicians stop already at the meta-meta-level. (There are diminishing returns of further formalization.)
Welcome to the wondrous world of mathematical logic! :-) In case you want to learn the glory details, have a lot of time at your hands and can understand German, you can watch a series of lectures I gave a couple months ago: https://www.youtube.com/playlist?list=PLR-3Jx6BfhkgjagoGM3Z1...
> But, a program is more than a text, it is a structure, parsed from text with the rules of the language .
Yes, you are right. By "text" I actually meant "term" or "abstract syntax tree".
> Execution of the program is when we give it some input and run it. So there would be similarly an input to proofs. Proof would need to be "proven correct" for EVERY valid input, that is what compiler does for programs, proving the result of the program must be of its declared result-type.
Not necessarily, not all programs require input and similarly not all proofs require input. But yes, for most cases you're right: Just as the program "output a prime number larger than <>" requires an input, so does a proof of the statement "there is a prime number larger than <>".
> But a proof which proves anything is not really a proof as said by someone, it corresponds to a non-halting program. So in this sense doesn't a proof ALWAYS require that we "run" it, to prove that it terminates, and thus is a valid proof actually?
Indeed, in general, running a proof and observing that it terminates is one way to ensure that it's a valid proof. However, all the proof systems (logics) used in mathematical practice correspond, under Curry–Howard correspondence, to programming languages in which any well-typed program terminates. (These programming languages are therefore in some sense quite impoverished; they are definitely not Turing-complete. However they are still rich enough to interpret all of mathematics!) Thus to ensure that a proof is valid it suffices to ensure that the corresponding program is well-typed. For the traditional proof systems used in mathematics (e.g. Zermelo–Fraenkel set theory), this is decidable, that is, it's easy to write a proof checker. For newer proof systems (e.g. homotopy type theory) the same holds, but type inference might not be decidable; therefore we declare that in order to give a full proof one also has to give all the types.
> Does this require some meta-logic? Proving that a proof terminates? :-)
Indeed! One possible choice for the meta-logic is "common human reasoning". Of course this is not formal, so the usual problems with informal reasoning apply. A popular alternative is PRA, "primitive-recursive arithmetic". All standard results you'll find in logics textbooks, such as Gödel's incompleteness phenomena or the Curry–Howard correspondence, can be formalized and proven within PRA. The reason why PRA is well-suited to study logical systems is because PRA itself is very weak, that is, easy to trust. In contrast, the usual logical systems used in mathematics are quite powerful, therefore conceivably (though extremely unlikely) inconsistent.
In case you'd like me to upgrade "extremely unlikely" to "provably", then I have bad news for you: PRA proves that if (PRA is able to prove that any of the standard systems is consistent), then (PRA is inconsistent). So there are just two options: Either PRA itself cannot be trusted, in which case all hell breaks lose (http://spikedmath.com/183.html); or PRA is trustworthy, in which case PRA is not inconsistent, in which case we know that PRA is not able to verify the consistency of any of the usual proof systems. (In this analysis, I'm assuming the law of excluded middle. Without it, it's not clear that these two options are the only ones.)
If you enjoyed the movie Inception, then you'll appreciate that we need a meta-meta-logic in order to talk about correctness of proofs formulated in PRA. This meta-meta-logic is almost always taken to be "common human reasoning". It could be substituted for a more formal version, for instance PRA again, but at some meta level you have to stop anyway and fall back to informality, so most logicians stop already at the meta-meta-level. (There are diminishing returns of further formalization.)
Welcome to the wondrous world of mathematical logic! :-) In case you want to learn the glory details, have a lot of time at your hands and can understand German, you can watch a series of lectures I gave a couple months ago: https://www.youtube.com/playlist?list=PLR-3Jx6BfhkgjagoGM3Z1...
Thanks for the very informative but thankfully informal answer. I especially like "PRA proves that if (PRA is able to prove that any of the standard systems is consistent), then (PRA is inconsistent)." :-)
There is a nice blog with a lot of resources on this topic
http://therisingsea.org/post/seminar-ch/
http://therisingsea.org/post/seminar-ch/
A beautiful truth of the universe :)
There’s an older gentleman who frequents a Panera in Chicago my wife works at. He is known and loved by all the employees and is staple of the store around closing time.
At some point, I made a comment about the paper he was reading (he always brings in the daily paper) and we sat for a bit and talked politics and news. He had introduced himself as Bill, and over the course of the conversation I came to found out that he was William Howard. I’ve sat down and chatted with him a few times since, and he’s always happy to help explain type theory to my feeble web dev mind :).
I was really impressed by how well versed he was, not only in his field of math, but also in his expertise of (what he considers a tangential field) programming, aerospace, ecenomics, etc. He’s got an air of humble greatness about him, and meeting him really left me a better and more educated person.