4 ms·

I was working on learning proofs, rather than programs, but I think there are a lot of similarities. I'm just a mathematician, and my mind has obviously been w

I was working on learning proofs, rather than programs, but I think there are a lot of similarities. I'm just a mathematician, and my mind has obviously been warped by continua and the Axiom of Choice but aren't they the same thing? http://en.wikipedia.org/wiki/Curry-Howard_correspondence http://en.wikipedia.org/wiki/Curry-Howard_correspondence Actually, I've gotten interested in learning more about theoretical CS lately, but my everyone in my department is too old/applied/Russian to care, and my university's CS people only seem to care about operating systems and e-commerce. Can you recommend a logical starting place?

sdp 18y ago
The equivalence seems to hold only when the program is complete. Thus, while all proofs can be expressed as programs, not all programs can be expressed as proofs.
- sdp 18y ago
  Programs are equivalent to proofs given their correctness, rather. Additionally, according to the wikipedia article, extracting a proof from a program requires a very richly typed programming language.
- 13ren 18y ago
  Can't you restrict the domain, and so that the program is complete (for that restricted domain)?
  - sdp 18y ago
    I meant correct, not complete. I refer to the article on wikipedia which states: "A converse direction is to use a program to extract a proof, given its correctness. This is only feasible if the programming language the program is written for is very richly typed: the development of such type systems has been partly motivated by the wish to make the Curry-Howard correspondence practically relevant."
ntoshev 18y ago
The notation you'd use to represent the program/proof is very important.
jderick 18y ago
One interesting difference is that if you are learning a proof, then you know when you are successful. At least for my research, I generated a bunch of small cases of the theorem I was trying to prove, then tried to learn the general case. If I was successful, I would have a proof of the original conjecture. When learning programs from some data, you can always test your program against the data but never can be sure that you are generalizing the data properly.

sdp 18y ago

The equivalence seems to hold only when the program is complete. Thus, while all proofs can be expressed as programs, not all programs can be expressed as proofs.

sdp 18y ago
Programs are equivalent to proofs given their correctness, rather. Additionally, according to the wikipedia article, extracting a proof from a program requires a very richly typed programming language.
13ren 18y ago
Can't you restrict the domain, and so that the program is complete (for that restricted domain)?
- sdp 18y ago
  I meant correct, not complete. I refer to the article on wikipedia which states: "A converse direction is to use a program to extract a proof, given its correctness. This is only feasible if the programming language the program is written for is very richly typed: the development of such type systems has been partly motivated by the wish to make the Curry-Howard correspondence practically relevant."

ntoshev 18y ago

The notation you'd use to represent the program/proof is very important.

jderick 18y ago

One interesting difference is that if you are learning a proof, then you know when you are successful. At least for my research, I generated a bunch of small cases of the theorem I was trying to prove, then tried to learn the general case. If I was successful, I would have a proof of the original conjecture. When learning programs from some data, you can always test your program against the data but never can be sure that you are generalizing the data properly.