9 ms·

> But now you're saying that you are interested in programming. TOC is about something else. (...) A model that requires a computationally powerful collaborator

> But now you're saying that you are interested in programming. TOC is about something else. (...) A model that requires a computationally powerful collaborator -- a programmer -- can't arise spontaneously in nature, for example. If you're trying to argue that “computation” is a physical phenomenon in the same sense gravity or electromagnetism are, I have bad news for you: it isn't. The theory of computation, just like information theory and probability theory, is first and foremost a mathematical theory: It is a priori only constrained by the requirement to be logically consistent. This is very different to what happens with a theory of gravitation or electromagnetism, which has to match external observations. > > Complexity in the sense of complexity theory? > Yes. Elaborate. > Whether that's an issue for the questions you're interested in asking doesn't define what "in practice" means. In practice, when I submit a Standard ML program to a REPL, the REPL tells me almost instantly whether my program is typable or not. > Again, burden is a question of meaning (proof: you need an agent for something to be a burden for). The requirement, however, shows that the different models are objectively, essentially and radically different. Agreed. Only one of the theories is actually useful. (Urgh, it's not a model in the logician's sense!)

pron 10y ago
> If you're trying to argue that “computation” is a physical phenomenon in the same sense gravity or electromagnetism are, I have bad news for you: it isn't. Don't know what you mean by "in the same sense", but Turing, von Neumann, Gödel and Hartmanis would have been saddened by your news because they thought (I guess Hartmanis still does) differently. So did Church. The very idea of algorithms -- as Church writes in his review of Turing's paper -- contains a notion of physical realizability. The idea of un/decidability -- only intuitively touched upon in Church's paper, and pretty thoroughly discussed in Turing's -- is predicated on the notion that a computational step takes at least some constant amount of physical time. It is true that a computation isn't a specific physical phenomenon like gravity, but a general, abstract phenomenon, that can be realized in different ways. But if it can't be realized, then it isn't considered computation, unless the people discussing it exclaim very clearly that they're discussing hypothetical computation. Some people take it further and say that not only computation is physical, but as it is meant to model the work of the mathematician, it grounds all of math in the physical along with it, and things that can't be feasibly computed (in some reasonable amount of time) should be left outside the realm of math. You may have heard this story by Harvey Friedman about the ultrafinitist Alexander Esenin-Volpin who attended his lecture[1], and Paul Cockshott from the Univeristy of Glasgow writes this[2]: > Turing starts a philosophical tradition of grounding mathematics on the material and hence ultimately on what can be allowed by the laws of physics. The truth of mathematics become truths like those of any other science — statements about sets of possible configurations of matter. So the truths of arithmetic are predictions about the behaviour of actual physical calculating systems, whether these be children with chalks and slates or microprocessors. In this view it makes no more sense to view mathematical abstractions as Platonic ideals than it does to posit the existence of ideal doors and cups of which actual doors and cups are partial manifestations. Mathematics then becomes a technology of modeling one part of the material world with another. As to the rest, there's much more to computation than programming, and your personal line of work is not the definition of utility. [1]: https://en.wikipedia.org/wiki/Alexander_Esenin-Volpin#Mathematical_work https://en.wikipedia.org/wiki/Alexander_Esenin-Volpin#Mathem... [2]: http://blogs.nature.com/soapboxscience/2012/06/20/turing-the-irruption-of-materialism-into-thought http://blogs.nature.com/soapboxscience/2012/06/20/turing-the...
- kd0amg 10y ago
  The notion of a function having any inherent complexity is rather at odds with your earlier assertion that putting any sort of meaning on the result of running a Turing machine is strictly human interpretation rather than a hard fact of computation (and of course, you also turn around and favor certain interpretations over others based on the cost of embedding them in your favorite computation model).
  - pron 10y ago
    > The notion of a function having any inherent complexity is rather at odds with your earlier assertion that putting any sort of meaning on the result of running a Turing machine is strictly human interpretation rather than a hard fact of computation I don't see how. That inherent complexity is precisely that computed by the machine (provided that you're talking about a function in the ordinary, set theory sense, rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership). > and of course, you also turn around and favor certain interpretations over others based on the cost of embedding them in your favorite computation model No, the complexity of evaluation differs in the different models by a small factor (polynomial at most), that is much smaller than the complexity differences of the representation. There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage. They aim prove something and proving something comes at a cost. There is no interpretation by which proving a possibly complex theorem is considered of having little complexity.
    - catnaroek 10y ago
      > I don't see how. That inherent complexity is precisely that computed by the machine The same function may be computed by different procedures with different complexity. > rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership Not all types denote sets. > There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage. This is the price of capturing the meaning of computation. Of course it doesn't come for free. But, in general, the earlier you do it, the less work it requires. In the limit, if you do it really late (e.g., test suites), it requires an infinite amount of work (searching infinite input spaces).

pron 10y ago

> If you're trying to argue that “computation” is a physical phenomenon in the same sense gravity or electromagnetism are, I have bad news for you: it isn't. Don't know what you mean by "in the same sense", but Turing, von Neumann, Gödel and Hartmanis would have been saddened by your news because they thought (I guess Hartmanis still does) differently. So did Church. The very idea of algorithms -- as Church writes in his review of Turing's paper -- contains a notion of physical realizability. The idea of un/decidability -- only intuitively touched upon in Church's paper, and pretty thoroughly discussed in Turing's -- is predicated on the notion that a computational step takes at least some constant amount of physical time. It is true that a computation isn't a specific physical phenomenon like gravity, but a general, abstract phenomenon, that can be realized in different ways. But if it can't be realized, then it isn't considered computation, unless the people discussing it exclaim very clearly that they're discussing hypothetical computation. Some people take it further and say that not only computation is physical, but as it is meant to model the work of the mathematician, it grounds all of math in the physical along with it, and things that can't be feasibly computed (in some reasonable amount of time) should be left outside the realm of math. You may have heard this story by Harvey Friedman about the ultrafinitist Alexander Esenin-Volpin who attended his lecture[1], and Paul Cockshott from the Univeristy of Glasgow writes this[2]: > Turing starts a philosophical tradition of grounding mathematics on the material and hence ultimately on what can be allowed by the laws of physics. The truth of mathematics become truths like those of any other science — statements about sets of possible configurations of matter. So the truths of arithmetic are predictions about the behaviour of actual physical calculating systems, whether these be children with chalks and slates or microprocessors. In this view it makes no more sense to view mathematical abstractions as Platonic ideals than it does to posit the existence of ideal doors and cups of which actual doors and cups are partial manifestations. Mathematics then becomes a technology of modeling one part of the material world with another. As to the rest, there's much more to computation than programming, and your personal line of work is not the definition of utility. [1]: https://en.wikipedia.org/wiki/Alexander_Esenin-Volpin#Mathematical_work https://en.wikipedia.org/wiki/Alexander_Esenin-Volpin#Mathem... [2]: http://blogs.nature.com/soapboxscience/2012/06/20/turing-the-irruption-of-materialism-into-thought http://blogs.nature.com/soapboxscience/2012/06/20/turing-the...

kd0amg 10y ago
The notion of a function having any inherent complexity is rather at odds with your earlier assertion that putting any sort of meaning on the result of running a Turing machine is strictly human interpretation rather than a hard fact of computation (and of course, you also turn around and favor certain interpretations over others based on the cost of embedding them in your favorite computation model).
- pron 10y ago
  > The notion of a function having any inherent complexity is rather at odds with your earlier assertion that putting any sort of meaning on the result of running a Turing machine is strictly human interpretation rather than a hard fact of computation I don't see how. That inherent complexity is precisely that computed by the machine (provided that you're talking about a function in the ordinary, set theory sense, rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership). > and of course, you also turn around and favor certain interpretations over others based on the cost of embedding them in your favorite computation model No, the complexity of evaluation differs in the different models by a small factor (polynomial at most), that is much smaller than the complexity differences of the representation. There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage. They aim prove something and proving something comes at a cost. There is no interpretation by which proving a possibly complex theorem is considered of having little complexity.
  - catnaroek 10y ago
    > I don't see how. That inherent complexity is precisely that computed by the machine The same function may be computed by different procedures with different complexity. > rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership Not all types denote sets. > There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage. This is the price of capturing the meaning of computation. Of course it doesn't come for free. But, in general, the earlier you do it, the less work it requires. In the limit, if you do it really late (e.g., test suites), it requires an infinite amount of work (searching infinite input spaces).