Academia is feudal and thus no answer to this is about to become widely accepted. :(
Actually it's a bit more like 42.
On Two Views of Computation in Computer Science
81–90 of 191 posts
Re: On Two Views of Computation in Computer Science
#82Earlier quoted context omitted.
The Church-Turing thesis is a statement about which functions of type `nat -> nat` are computable, either in the lambda calculus or using Turing machines. This completely disregards: (0) Computational complexity. Neither the lambda calculus nor Turing machines were invented to answer questions of computational complexity. (1) Functions at types other than `nat -> nat`. Curiously enough, programming in the real world…
> The Church-Turing thesis is a statement about which functions of type `nat -> nat` are computable, either in the lambda calculus or using Turing machines. This is how Krishnaswami frames things. From the TOC perspective, there is no such thing as functions at all. Computations consume and produce strings. Both Church and Turing explain how those strings can encode the natural numbers (there was no talk of types by…
> Computations consume and produce strings.
Really? What's so special about strings? Perhaps I want computations to consume and produce trees. It seems like you've picked an arbitrary setting for computation and said "Look! My constructions which are naturally suited to this setting are naturally suited to this setting!".
Re: On Two Views of Computation in Computer Science
#83Earlier quoted context omitted.
> They do use the word function, just not in terms of the language itself, but in the same sense of saying that a falling apple integrates the function from its mass to acceleration That's the same sense in which Neel means it.
No, he doesn't. In the type view, the computation is asked to do two things: compute the output and check a proof that the output belongs to a set. Each of these questions has its own computational complexity. You may say that the first question comes from free by deciding how to think of the apple; the second certainly doesn't. See also https://news.ycombinator.com/item?id=12403508
Yes he does. If by "Which functions nat -> nat are computable" he meant "functions written in some typed language" then the answer is vacuously "all of them".
Re: On Two Views of Computation in Computer Science
#84Earlier quoted context omitted.
> If you generalize to trees and pick the right alphabet, suddenly every element of your datatype is a well-formed lambda term. How would you feed trees to the computation? Also, once types are involved, nothing can help you. I admit that untyped LC is somewhat of a borderline case. > It's also unclear if you're talking about the complexity of type inference or type checking Doesn't matter in this case. Pick a string…
> How would you feed trees to the computation Um, well the computation (can be set up to) proceeed(s) on algebraic datatypes, so this seems trivially easy.
:) You're just pushing the complexity into the validation of the algebraic type.
Look, a typed formalism does extra work of proving the type safety of the input. Checking a proof has a non-negligible complexity. If that cost could be ignored, then I have a computation model that solves NP problems in zero time: it has a type system that requires that the types form a proof certificate for the problem. All (obviously valid) inputs are then trivially reduced to "yes". In fact, you know very well that some type systems are Turing complete. If the complexity of validation is ignored, then those models can compute anything that's computable in zero time.
Types can prove things. The cost of the proof is well known, and is related to the difficulty of the problem. The universe doesn't let computational complexity slide. What, you think that God says, "oh, you clever boy, you chose a typed model so I'll let you have this proof for free!" ?
Re: On Two Views of Computation in Computer Science
#85Earlier quoted context omitted.
Author here. > But both can be viewed as a state plus a well-defined set of rewriting rules, so I suspect that the article is struggling to make what is really a distinction without a difference. 1. I state that the untyped lambda calculus is, indeed, a borderline case, and is a simple rewriting system which, in turn, is a special case of a nondeterministic abstract state machine. 2. That many things are abstract sta…
> zero for the machine models That's absolutely not true. It takes non-zero effort to determine whether the code for a Turing machine actually implements a valid Turing machine.
No,it's actually right. See my post comment answering the same question. It is the circuit models that actually pose a harder challenge, but even if you won't accept my reasonable zero-cost encoding where a misconnected input is interpreted as a constant 0,the cost of validation is still less than even untyped LC.
Re: On Two Views of Computation in Computer Science
#86Earlier quoted context omitted.
No, he doesn't. In the type view, the computation is asked to do two things: compute the output and check a proof that the output belongs to a set. Each of these questions has its own computational complexity. You may say that the first question comes from free by deciding how to think of the apple; the second certainly doesn't. See also https://news.ycombinator.com/item?id=12403508
Yes he does. If by "Which functions nat -> nat are computable" he meant "functions written in some typed language" then the answer is vacuously "all of them".
Not all functions of type nat -> nat are computable in any formalism. You can write plenty of programs that are really of type nat -> nat in say, Haskell, that try to compute a non-computable natural function. They just can't do it and they'll never terminate for some inputs. But they're still perfectly well-formed.
Re: On Two Views of Computation in Computer Science
#87Earlier quoted context omitted.
Humm... But the set of Turing Machines is countably infinite, and a nat -> nat function is necessarily representable as a Turing Machine.
It is not necessarily representable. By diagonalization, in fact, nat -> nat can be shown to be uncountably infinite. Intuitively, an example nat -> nat function that is uncomputable is ~Ld, the function that, given a natural index i into the diagonal of the table of Turing machines and their accepted strings, returns the opposite of whether machine i accepts string i. The output is then clearly equal to no Turing ma…
Ok, that's a good point, but it is also true that functions requiring an oracle cannot also be represented in any Turing-complete programming language, right?
This seems trivial to prove: any function representable in any given programming language maps to a finite string of characters, and finite strings of characters maps to natural numbers.
Re: On Two Views of Computation in Computer Science
#88> You’re free to think about computation as acting on bits… but for those bits to do us any good, they have to actually represent something (e.g., data structures). I suspect this is a case of confusing epistemology with ontology. Galaxies are ontologically composite in that they're the highest holonym in the supervenience hierarchy [0]. Atoms are ontologically fundamental in that they're the the lowest meronym in th…
Well, in this case all models are quite abstract, and there's a very real computational complexity difference between them. The key, if I were to use your way of presenting the issue, is the recognition that some epistemological abstractions are more computationally costly than others. So it's true that you can choose either representation as a foundation, but the representations objectively and radically differ in their computational complexity.
Re: On Two Views of Computation in Computer Science
#89Academia is feudal and thus no answer to this is about to become widely accepted. :(
Actually it's a bit more like 42.
How is showing that two representations are fundamentally different because they objectively and radically differ in computational complexity open to interpretation?
Re: On Two Views of Computation in Computer Science
#90Earlier quoted context omitted.
Yes but the real number that cannot be pinned down using a formula can also not be pinned down using a computation, and we are talking of models of computation.
> Yes but the real number that cannot be pinned down using a formula can also not be pinned down using a computation, Undefinable real numbers exist, whether you can compute them or not. > and we are talking of models of computation. A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy be…
> Undefinable real numbers exist, whether you can compute them or not.
I agree with you, but as you probably know this is a deep ontological question. The meaning of something "existing" has been debated for many centuries, especially for cases such as this.
> A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model?
There is a difference between rejecting and classifying. I am not proposing a new computational model. Turing's model classifies the busy beaver function as non-computable. Correct?
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...