7 ms·

it's self-evident _at this point in time_, given you could feed such a machine the collatz conjecture as an algorithm and we just don't know if any arbitrary in

it's self-evident _at this point in time_, given you could feed such a machine the collatz conjecture as an algorithm and we just don't know if any arbitrary input will halt. I'm not claiming it is self-evident in perpetuity. By bounding problem I guess I mean the mathematical equivalent of knowing it can halt. I'm not a mathematician as I previously stated so I don't know the terminology. 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. But a subset of all mathematics, sure (perhaps computability, or logic in general although of a higher kind than first-order). My interest is in creating a static analyser based on the set of axioms or deductions that can be derived from that space.

lisper 8y ago
> it's self-evident _at this point in time_ No, it's not. Just because you and I don't know the answer is not proof that no one knows the answer. Someone may have discovered the answer in the last five minutes. (In fact, for any mathematical discovery there is always necessarily a period time when only one person knows the answer.) > AFAIK not all problems relate directly to this space And I am telling you that you are wrong about that. If you think that there is anything about computation that does not relate to math then you have a deep misunderstanding of either computation or math (possibly both).
- 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 ago
    Let 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 ago
      well 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.
chriswarbo 8y ago
> My interest is in creating a static analyser based on the set of axioms or deductions that can be derived from that space. From the sound of it, I think this might be a little backwards: axioms and deductions give rise to a space of possible proofs, and those can be used for things like static analysis. One example of going the other way is "reverse mathematics", where we try to find a set of axioms that give rise to some statement. I'm not sure if that could be applied to a (perhaps informal) "space" of theorems rather than some particular theorem.
- beaconstudios 8y ago
  you're right, my phrasing wasn't ideal there. I'll try to clarify: what I want to do is to create a static analyser based on a set of axioms/deductions that can determine which of the "always halts/does not always halt/don't know" categories a program fits into. (I'm rephrasing the categories because a program like "(x: int) => x == 1 ? halt : loop" fits into the second category). What I'm wanting to figure out is the mathematical field in which these types of axioms reside. My naive assumption was that computability theory is the answer but in researching the various branches of similar fields it seems to me that there is a lot of crossover and similarities between concepts in different fields. So I wasn't sure if there was a field that covers what I would describe as "given a sequence of transformations of typed values, representing those transformations as relationships between inputs and an output, can we definitively prove that the program halts, or does not always halt". For example, given the function "f(x: int) => x is even ? f(x + 1) : halt" I can know from looking at it that it will halt on any valid input because for any int x, recursing on x + 1 has to reach a value where x is not even. I just don't know how I would formalise such knowledge into a system that can actually deduce such conclusions as you could clearly change "x is even" to any "x is wholly divisible by <integer>" and the conclusion would hold.
  - lisper 8y ago
    > you could clearly change "x is even" to any "x is wholly divisible by <integer>" Or... "x is a prime number" "x is a counterexample to the Goldbach conjecture" "x is an encoding of a planar map that cannot be four-colored" "x is the encoding of an algorithm that solves the traveling salesman problem in polynomial time" "x is the encoding of a formal proof of the Riemann hypothesis"

lisper 8y ago

> it's self-evident _at this point in time_ No, it's not. Just because you and I don't know the answer is not proof that no one knows the answer. Someone may have discovered the answer in the last five minutes. (In fact, for any mathematical discovery there is always necessarily a period time when only one person knows the answer.) > AFAIK not all problems relate directly to this space And I am telling you that you are wrong about that. If you think that there is anything about computation that does not relate to math then you have a deep misunderstanding of either computation or math (possibly both).

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 ago
  Let 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 ago
    well 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.

chriswarbo 8y ago

> My interest is in creating a static analyser based on the set of axioms or deductions that can be derived from that space. From the sound of it, I think this might be a little backwards: axioms and deductions give rise to a space of possible proofs, and those can be used for things like static analysis. One example of going the other way is "reverse mathematics", where we try to find a set of axioms that give rise to some statement. I'm not sure if that could be applied to a (perhaps informal) "space" of theorems rather than some particular theorem.

beaconstudios 8y ago
you're right, my phrasing wasn't ideal there. I'll try to clarify: what I want to do is to create a static analyser based on a set of axioms/deductions that can determine which of the "always halts/does not always halt/don't know" categories a program fits into. (I'm rephrasing the categories because a program like "(x: int) => x == 1 ? halt : loop" fits into the second category). What I'm wanting to figure out is the mathematical field in which these types of axioms reside. My naive assumption was that computability theory is the answer but in researching the various branches of similar fields it seems to me that there is a lot of crossover and similarities between concepts in different fields. So I wasn't sure if there was a field that covers what I would describe as "given a sequence of transformations of typed values, representing those transformations as relationships between inputs and an output, can we definitively prove that the program halts, or does not always halt". For example, given the function "f(x: int) => x is even ? f(x + 1) : halt" I can know from looking at it that it will halt on any valid input because for any int x, recursing on x + 1 has to reach a value where x is not even. I just don't know how I would formalise such knowledge into a system that can actually deduce such conclusions as you could clearly change "x is even" to any "x is wholly divisible by <integer>" and the conclusion would hold.
- lisper 8y ago
  > you could clearly change "x is even" to any "x is wholly divisible by <integer>" Or... "x is a prime number" "x is a counterexample to the Goldbach conjecture" "x is an encoding of a planar map that cannot be four-colored" "x is the encoding of an algorithm that solves the traveling salesman problem in polynomial time" "x is the encoding of a formal proof of the Riemann hypothesis"