3 ms·
It's true! The reasoning is fairly simple, though. In such a language, types classify terms and types correspond to theorems. The type/theorem for a fixed poin
by tel 11y ago
It's true! The reasoning is fairly simple, though.
In such a language, types classify terms and types correspond to theorems. The type/theorem for a fixed point is
fix : forall a . (a -> a) -> a
which as a theorem reads: "for any proposition A, if we can prove 'if A, then A' then we can prove A". Hopefully it's now clear why having 'fix' in your prover language won't work!
- CHY872 11y agoNot quite. You're appleaing to the Curry-Howard correspondance, which is neat but is not used by many theorem provers. Furthermore, > fun fix (f : 'a -> 'a) : 'a = fix f; val fix = fn: ('a -> 'a) -> 'a The trick is that all functions must be total, which is the crux of the matter (and why the Y-combinator exhibits the paradox, because it allows nontermination). This is why we have stuff like the polymorphic lambda calculus, in which termination is guaranteed and the Y-combinator is untypeable.
- tel 11y agoYes, of course. I'm not trying to prove anything, just to not that non-termination leads to suspicious looking logics.