3 ms·
not quite - I'm trying to implement existing proofs into an axiomatic system. All unproven theorems can be classified as the "don't know" outcome. But I don't k
by beaconstudios 8y ago
not quite - I'm trying to implement existing proofs into an axiomatic system. All unproven theorems can be classified as the "don't know" outcome. But I don't know what approach to use to implement a system that can look at "f(x: int) => x is cleanly divisible by 2 ? f(x + 1) : halt" and tell me that this recursive function all halt under all valid inputs. Because that would require that it be able to derive such a fact from a core understanding of what addition and division mean.
- lisper 8y ago> that would require that it be able to derive such a fact from a core understanding of what addition and division mean Yes, and that's the part that's not possible in general, only for specific cases. For example, you can prove that: f(P: int -> boolean, x: int) => P(x) ? f(x + 1) : halt will halt for any x IFF there are an infinite number of integers that have the property P, so f will halt if P is "is an even integer" because there are an infinite number of even integers (which, obviously, you can also prove). And with that in mind, you might want to go take another look at: https://news.ycombinator.com/item?id=17465542 https://news.ycombinator.com/item?id=17465542