Given that the Curry-Howard Correspondence is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?
$\begingroup$
$\endgroup$
6
-
1$\begingroup$ Seems more suited for cstheory.stackexchange.com $\endgroup$– NeilCommented Feb 28, 2011 at 10:56
-
$\begingroup$ If op would like, @ me in a comment and I can migrate it for you. $\endgroup$– WillCommented Feb 28, 2011 at 13:45
-
2$\begingroup$ John Crossley wrote a paper on this that I happened to see posted somewhere recently: [What is the difference between proofs and programs?][citeseerx.ist.psu.edu/viewdoc/… -- I haven't read it yet, but it came recommended... $\endgroup$– TaraCommented Feb 28, 2011 at 15:05
-
1$\begingroup$ @TJ Ellis, thanks for the link, but after a brief skim, it seems that the paper doesn't answer the question posed in it's title (or the answer is "they are the same"). $\endgroup$– max taldykinCommented Feb 28, 2011 at 16:30
-
$\begingroup$ @TJ Ellis, did you see it post on reddid/r/compsci? I did it, ;) @max, I felt so, that's why I post this question. $\endgroup$– plmdayCommented Feb 28, 2011 at 20:28
|
Show 1 more comment
5 Answers
$\begingroup$
$\endgroup$
5
The programming languages people use day to day don't fit so well into the Curry-Howard correspondence, because their type systems are too weak. To say something interesting using Curry-Howard for imperative programs, one needs to have a more sophisticated type system. The book Adapting Proofs-as-programs pushes this angle with the aim of synthesising imperative programs. With dependent types becoming more and more popular, certainly in research functional languages (Agda, Epigram), the distinction is becoming blurrier. Of course you can do program synthesis/extraction within the Coq theorem prover (and presumably others), which is of course based on Curry-Howard.
The Curry-Howard correspondence can also be used in situations where the proofs do not so clearly correspond to programs (or they are not programs anyone will ever run). One example of this is in Proof-carrying authorization. The propositions correspond to statements about who is authorized to do what. Proofs provide the required evidence that a proposition holds, thus an authorization request is permitted. In order to encode the proofs, proof terms are introduced (via Curry-Howard). Proof terms are sent between parties as representations of proofs of the validity of authorization requests, but they are not considered programs.
answered Mar 1, 2011 at 19:28
-
1$\begingroup$ You should mention dependently typed languages, as in them the line between proofs and propositions gets blurred. $\endgroup$ Commented Mar 1, 2011 at 20:22
-
1$\begingroup$ Indeed. Let's not forget Coq's program synthesis/extraction. $\endgroup$ Commented Mar 1, 2011 at 20:25
-
$\begingroup$ what program would correspond to a non-constructive (classical) proof of the form $\forall k \ T(e,k) \lor \lnot \forall k \ T(e,k)$? (Assume that $T$ is some interesting decidable relation e.g. $e$-th TM halts in $k$ steps.) (I can ask it as a new question if the answer is not very short.) $\endgroup$– KavehCommented Mar 2, 2011 at 7:40
-
1$\begingroup$ @Kaveh: do ask this as a separate question. In a comment you can say "the Godel-Gentzen translation is a continuation-passing transformation" but anything less cryptic won't fit. :) $\endgroup$ Commented Mar 2, 2011 at 8:27
-
$\begingroup$ @Neel, done: cstheory.stackexchange.com/q/5245/186 $\endgroup$– KavehCommented Mar 2, 2011 at 10:48
$\begingroup$
$\endgroup$
In Coq, there are 2 types (Prop and Set), they are used by the programmer to separate what are proofs that won't produce actual code and the part of the proof that will be used to extract running code (your program).
That is a nice solution for the problem you ask about, how to identify what is meant to generate machine code (program) and what is present to complete the proof of the proposition (or type).
AFAIK there is no automatic way to distinguish both. This might be something interesting for research? Or maybe someone is able to point out it's clearly impossible?
With dependent types not only there isn't a clear distinction between proofs and programs but also there isn't a distinction between programs and types! The only distinction will be where the type(or program) appear, making it part of the "program" place or of the "type" place of a given term.
An example will make it clearer i hope:
When you use the identity function with dependent types you need to pass the type your are going to use the function with! The type is being used as a value in your "program"!
Untyped Lambda Calculus:
id = $\lambda{x}.x$
With Dependent Types:
id : (A : Set) -> A -> A
id = $(\lambda{A}.(\lambda{x}.x))$
If you are using this function, then you would do it like this example:
id Naturals 1
Notice that the "type" (in this case the Set of Naturals) being passed as a value is thrown away so it will never be computed, but still it's in the "program" part of the term. That's what also will happen with the "proof" parts, they need to be there for the term to type-check but during computation they will be thrown away.
$\begingroup$
$\endgroup$
3
I will go out on a limb here and say that, if you are willing to squint a bit, proofs and terminating programs can be identified.
Any terminating program is a proof that you can take its input and produce its output. This is a very basic kind of proof of implication.
Of course, to make this implication carry information more meaningful than stating the obvious, you need to be able to show that the program works for any and all instances of input drawn form some class with logical meaning. (And so too for the output.)
From the other direction, any proof with finite inference steps is a symbolic program manipulating objects in some logical system. (If we don't worry too much about what the logical symbols and rules mean computationally.)
Types and propositions can be made to work similarly. Any type T can be assigned the proposition $\exists x : x \vdash T$ with obvious truth conditions. Any proposition can be turned into the type of it's proofs.
This is pretty simplistic, but I think it does suggest the robustness of the idea. (Even if some people are bound not to like it. ;-) )
answered Mar 2, 2011 at 0:02
-
-
$\begingroup$ One should assume, of course, that you mean finite proofs and terminating programs. Some classes of non-terminating programs work just fine as infinite proofs. It's the non-productive non-terminating programs you need to watch out for. $\endgroup$ Commented Mar 5, 2011 at 2:32
-
$\begingroup$ I think this is a bit tricky, depending on how you are defining finite and infinite with respect to proofs. In general, all proofs that we accept are finite, because they have to convince a human in a small finite amount of time. A proof that relies on an induction scheme (i.e. most "infinite" proofs) are by this measure still finite, they just have symbolic steps that represent an infinite but regular computation. A truly infinite proof, that I think most of us would reject as a valid proof, would be one where you literally had to consider an infinite number of distinct facts to validate. $\endgroup$ Commented Mar 5, 2011 at 15:36
$\begingroup$
$\endgroup$
Proof irrelevance?
When you write some program, you are interested in its performance, memory consumption etc.
E.g it's better to use some clever sorting algorithm instead of bubble sort, even if their implementations have same types (even in dependent type setting).
But when you prove some theorem it is only existence of a proof you are interested in.
Of course, from aesthetic point of view, some proofs are more simple/beautiful/inspiring/etc (e.g. proofs from The Book).
$\begingroup$
$\endgroup$
If you accept the Curry–Howard correspondence then the question is mainly a philosophical one. "Are proofs and programs different? Of course. How? Well, we call proofs 'proofs' and we call programs 'programs'."
Or to put it less flippantly, if there's an isomorphism between proofs and programs —which it seems clearly there is— then your question is asking whether there is any oracle capable of distinguishing the two. Humans categorize them as being different (for the most part), so it's certainly arguable that such an oracle exists. The important question then becomes whether there is any meaningful difference between them, which is up for philosophical debate. What is a "proof"? There is no formal definition of what constitutes a proof; it's a term of art, much like the notion of "effectively calculable" in the Church–Turing thesis. For that matter, "program" has no formal definition either.
These are words of natural language used to categorize different fields of mathematical enquiry. What Curry and Howard observed is that these two different fields where in fact studying the same thing. Noticing this connection is important because it says that these different researchers should be talking to one another. But on another level, to notice the connection is to belie the difference between them. When tackling a problem, sometimes it is more beneficial to think of it as a programming problem, whereas other times it is more beneficial to think of it as a logical problem. This difference in perspective is, I think, the important difference between them. But whether a difference of perspective constitutes a difference of identity is a deep philosophical question which has been explored at least as far back as Frege's Ueber Sinn und Bedeutung.
