4 ms·
The Curry-Howard correspondence suggests the analogy of computation with lambda calculus and logical proof systems. As a non-expert it seems that same analogy e
by justinhj 4y ago
The Curry-Howard correspondence suggests the analogy of computation with lambda calculus and logical proof systems. As a non-expert it seems that same analogy extends roughly to lambda calculus and a lisp system
- voxl 4y agoThe Curry-Howard Correspondence is about proof systems. You would have a very hard time finding a proof theorist that says it's okay to have an undecidable proof checker or an inconsistent one. For that reason, only _typed_ lambda calculi have any hope of corresponding to a proof system. You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent. Perhaps a para-consistent logic might work, but we're getting very exotic here.
- justinhj 4y agoInteresting, thanks
- hither_shores 4y ago> You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent. It's not. (x -> x) is always inhabited, so if you have a fixed point combinator (x -> x) -> x then every theorem is true.