On Two Views of Computation in Computer Science

> Turing's model classifies the busy beaver function as non-computable. Correct?

Yep.

> I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines...

Turing never redefined the concept of “countable”, which belongs in set theory. If you had asked him what the cardinality is of the set of functions from the naturals to the naturals, he would've answered you “uncountable, of course”.

> 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!)

Like entropy, computational/informational content is absolute. Strings have higher entropy. If I say, "I'll hand you a piece of fruit", that statement objectively has less information (and therefore smaller computational complexity to verify), then if I said, "I'll hand you an apple". A tree really is inherently more complex than a string. It's like an RNA molecule being more likely to be naturally synthesized in the primordial soup than, say, a cat. Of course, an unspecified "tree" could be as "entropic" as an unspecified string, but my guess is that you mean something more specific.

So there's a real difference between various configurations of gas molecules in a box, and a real difference in the computational cost of representing them. Your statement is not unlike saying, "oh, so you've picked a high-entropy configuration, how convenient! What's so special about high entropy?" High entropy and low entropy aren't symmetrical. It takes more energy to move in one direction than the other.

Again, you shouldn't be surprised by this at all (I'd think it's rather obvious). Since typed formulations do proof work in their validation step (that can be Turing-complete in some cases), obviously that means that there is more complexity in their representation, otherwise, you'd have computation for free.

You can choose whatever representations you like. But representations that express more information, come at a higher computational cost.

A tree is still more complex than strings, because it has rules: one parent per node and no cycles. Those need to be validated. But I have absolutely no problem accepting that it is possible to find an encoding of untyped LC which would bring it very close to a TM encoding. This wouldn't be surprising as LC doesn't do more computational work than TM at the validation step (unlike typed formalisms).

I specifically wrote that untyped LC is a borderline case, and it's unclear where precisely we want to draw the line. What is absoutely clear is that System F and TM are essentially, qualitatively and objectively very different, and when people try to compare them, they often, without noticing, describe two different computational problems, with two different complexities.

> 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#Mathem...

[2]: http://blogs.nature.com/soapboxscience/2012/06/20/turing-the...