3 ms·
And if those functional languages are Turing complete, then they are equivalent to all other Turing complete languages, and thus the C-H isomorphism would hold
by gatlin 14y ago
And if those functional languages are Turing complete, then they are equivalent to all other Turing complete languages, and thus the C-H isomorphism would hold for all Turing complete languages.
- jahewson 14y agoNope. C-H concerns the simply typed lambda calculus which is not Turing-complete. Thus C-H only applies to non-recursive functional programs (or equivalent). A proof is a program, but a program is not always a proof (as proofs must terminate).
- gatlin 14y agoI concede. Thanks for the interesting tangent of reading that brought on, too!