3 ms·
alright, if you're going to resort to nitpicking and being wilfully insulting then I see there's not much point discussing this further with you.
by beaconstudios 8y ago
alright, if you're going to resort to nitpicking and being wilfully insulting then I see there's not much point discussing this further with you.
- lisper 8y agoLet me rephrase that to hopefully make it sound a little less insulting: if you are able to identify an aspect of computation that cannot be described mathematically then you will be remembered alongside Turing, Godel and von Neuman as one of the greatest thinkers humanity has ever produced. (But a priori, the odds of your being able to do that seem pretty low to me.)
- beaconstudios 8y agowell you've just gone and been inaccurate yourself - I said that I didn't believe all mathematical discoveries had an impact on computability, but you just suggested I was saying that not all computation is based in mathematics. Which is absurd and it's clear you think I'm stupid, where to me it's pretty clear you are misinterpreting what I'm saying, whether that's poor communication on my part or uncharitable interpretation on yours. I've been friends with academics before who had an unyielding desire to interpret lay speak as an attempt to be rigorous and then criticise it as such, as you have done with me saying "self-evident", but surely you realise I'm not trying to say "self-evident" in some kind of rigorous mathematical sense? I mean if you're just trying to be obtuse it's working well but it comes off like you're trying to hold my conversational and largely intuition-based ideas to a much higher standard than I am trying to meet. I don't understand the impulse at all. If I were trying to be totally rigorous with my thoughts rather than just conversationally trying to communicate an idea that is still taking shape, I would be learning the correct syntax to write a paper and sharing that instead.
- lisper 8y ago> I said that I didn't believe all mathematical discoveries had an impact on computability, but you just suggested I was saying that not all computation is based in mathematics. Which is absurd No, that's not what I said. What I said was that this statement: "I don't think the space I'm talking about is equivalent to the state of all of our mathematical knowledge, as AFAIK not all problems relate directly to this space." is false. This is not a matter of opinion. There is a formal equivalence between math and computability. For every theorem, there is a corresponding program that halts IFF the theorem is true, and for every program, there is a corresponding theorem that is true IFF the program halts. Therefore, it is necessarily the case that all mathematical discoveries have an impact on our knowledge of computability because there is in fact no distinction between math and computability. They are the exact same field of study, just with different window-dressing. > and it's clear you think I'm stupid No, I don't think you're stupid, merely ignorant (and a bit defensive). And this has nothing to do with your lack of rigor, it has to do with your intuition that there might be something worthwhile to be discovered by trying to examine the structure of known halting and non-halting programs. This is a well understood problem. It is possible that you could discover something that everyone else has overlooked. But if you do, it would be a breakthrough of the highest order, a major revolution in both computability theory and mathematics.
- beaconstudios 8y agoIf 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 agoYes, 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 agonot 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