|
|
|
|
|
|
by jw-
2868 days ago
|
|
|
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. |
|
|