Curry-Howard correspondence states the equivalence between logic/deduction and types/programs.The Church-Turing thesis states the equivalence of some models of computation. Specifically, all computable functions can be written both on a Turing Machine and in Lambda Calculus.Not all logics are equivalent however. 2nd order logic can quantify over sets whilst 1st order can't.Can someone explain the dissonance? Can some computable functions be expressed at a higher-level but not at a simpler-level? [CLARIFICATION]If I define a model for computation off say 2nd order logic whilst the Turing Machine is a model for 1st order logic, then does that mean my hypothetical language can compute uncomputable functions? It appears so to me because 2nd order logic is more powerful than 1st order logic. This is clearly nonsense because Haskell is based off a flavor of 2 order logic (system F with extensions) but isn't more powerful than say C: any program achievable in Haskell is achievable in C. The mapping (or equivalence) between logic and computation does not appear to preserve the notion of strength: 2nd order logic is stronger than 1st order logic but programming languages off 2nd and 1st order logic have the same strength. Does that make sense?The only conclusion I can come to is that the relationship between logic and types is not a straightforward mapping. The Turing Machine is not based off any specific logic and that any logic/deductive system can be mapped to the Turing Machine. Can you confirm?[CLOSING WORDS]I think that my mistake is in not realizing that there is a large divide between the colloquial program and programs in the context of types.Haskell which is based on a stronger, more expressive type system does indeed provide stronger, more expressive programs. These programs are stronger in the sense that more can be guaranteed about them (in the same sense as type safe). This does not mean that Haskell can compute more; it is still merely Turing complete.
Curry Howard correspondence and Church-Turing thesis
computability;logic;functional programming;church turing thesis;curry howard
I'm not sure where you see the dissonance. The Church-Turing thesis is a hypothesis stating that Turing Machines (equiv. Lambda Calculus or Recursive Functions) can do anything that we'd think of as computable.The Curry-Howard correspondence is a much stronger statement that certain types of intuitionistic logic are structurally identical to things kind of like the Lambda Calculus. It doesn't really say which logic it corresponds to, it just shows that you can map the logical constructions in a canonical way to a (typed) computational model and vice versa. If you take different logics, you get different models and vice versa. The models may or may not be Turing-complete, although if we believe the Church-Turing thesis (it does seem to be doing alright so far), if you get a model that's more powerful than a Turing Machine, then you've got something incomputable in there.Nonetheless, the logic you deal with does limit what you can compute in the corresponding model. For example, the Calculus of Inductive Constructions, which is a type theory and the basis for Coq, only allows types that it can verify have decreasing definitions (i.e. a recursive destruction of the type will terminate), but there are perfectly computable types which it can't verify, so you're locked out of using them.