Re:Curry–Howard correspondence
by jw- on Tuesday August 14, 2018 @06:23AM
(#17756659)
General recursion in programs (that makes termination undecidable) requires a fix-point operator of type (a -> a) -> a
The logical equivalent of this is an axiom (P -> P) -> P which lets you prove anything. So non-termination in a programming language corresponds to being able to prove anything - including False - in the logic.
The logical equivalent of this is an axiom (P -> P) -> P which lets you prove anything. So non-termination in a programming language corresponds to being able to prove anything - including False - in the logic.