3 ms·

If you think I'm trying to discover something then you've completely missed my point. I was never looking to discover some new concept, but to find an existing

If you think I'm trying to discover something then you've completely missed my point. I was never looking to discover some new concept, but to find an existing model of looking at computability and implement it as software. I know its possible to decide computability for at least some subset of programs because we can do it by eye, I'm just looking to do the same thing programmatically in a way that is theoretically sound.

lisper 8y ago
Yes, I understand that. And what I'm trying to tell you is that this problem you have set for yourself is formally equivalent to the problem proving mathematical theorems. They are the same problem. Any substantial progress on one is necessarily also substantial progress on the other.
- 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

lisper 8y ago

Yes, I understand that. And what I'm trying to tell you is that this problem you have set for yourself is formally equivalent to the problem proving mathematical theorems. They are the same problem. Any substantial progress on one is necessarily also substantial progress on the other.

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