Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

On Two Views of Computation in Computer Science

pressron.wordpress.com

Post reply on HN
Print view View original

11–20 of 191 posts

Re: On Two Views of Computation in Computer Science

#11

Post by catnaroek »

TelmoMenezes wrote: post #10
catnaroek wrote: post #7

Earlier 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…

Does a type exist such that it cannot be mapped to the set of natural numbers?

You mean mapped one-to-one? Depends on your model of computation. For example, in the simply typed lambda calculus, equipped with a natural number type, as well as structural recursion on it (but not general recursion), `nat` and `nat -> nat` aren't isomorphic types.

Re: On Two Views of Computation in Computer Science

#12

Post by LolWolf »

pron wrote: post #6
LolWolf wrote: post #2

This is an interesting article, but I'm still fairly confused about the notion that is made >Harper’s attack on the utility of machine models and lack of modularity is tantamount to an architect saying to a chemist, “both of our disciplines concern the arrangement of molecules, yet my discipline is superior, as yours doesn’t even have the modular notion of a room!” But wouldn't the whole point be that a chemist, seei…

You can translate and transform many things to many others. The important question is what is the computational complexity of the transformation? If it is large, then the two things are very different. As Scott Aaronson once said, waterfalls could be viewed as playing chess, but as the complexity of the translation from the "waterfall language" to a chess language understandable by humans is as great as the complexit…

Wait, but I thought the question being posed wasn't about the computational complexity of any model but about the power of a given computational model relative to another (e.g. the subject of the CT thesis).

Even if we're talking about just computational complexity, if we allow Turing machines with arbitrary oracles, or (equivalently) we allow arbitrary mathematical constructions in languages, I'm still unsure as to why the complexity matters.

W.r.t the waterfall case. Sure, I agree with that statement, but I'm unsure as to how it plays into the final case---the question isn't about a specific model performing a specific task, but about a model being able to completely replicate another in terms of computational power. Anything I can do in a language (with some functions) I can do in a Turing machine with the appropriate oracles; and conversely, anything I can do in a Turing machine with some given oracles, I can do in a language.

Re: On Two Views of Computation in Computer Science

#13

Post by SilasX »

catnaroek wrote: post #7
Kenji wrote: post #3

It’s really weird that the Church-Turing thesis, which is ridiculously robust at first order, falls apart so comprehensively at higher type. A statement like that makes me feel like Neel Krishnaswami does not understand the Church-Turing thesis at all (what does the Church-Turing thesis even mean at a "higher type"), but considering that this person has significant experience in this field, much more than I do, I am…

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…

Sorry if I'm missing something fundamental, but (1) shouldn't matter if there's some mapping between a) those types and b) functions of type `nat -> nat`. AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM. IOW, whatever transformation it is that the other-typed function makes (edit: or whatever input-output mapping), it is isomorphic to one on `nat -> nat`.

Since computers regularly implement exactly such a mapping, it doesn't sound like a problem.

>Curiously enough, programming in the real world is seldom about evaluating functions of type `nat -> nat`.

How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers). The whole job of programming can be described as "converting a problem to a format suitable for a fast `nat->nat`-implementing machine"; it's just that several of the layers of the conversion are hidden from you.

Re: On Two Views of Computation in Computer Science

#14

Post by catnaroek »

SilasX wrote: post #13
catnaroek wrote: post #7

Earlier 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…

Sorry if I'm missing something fundamental, but (1) shouldn't matter if there's some mapping between a) those types and b) functions of type `nat -> nat`. AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM. IOW, whatever transformation it is that the other-typed function makes (edit: or what…

> (1) shouldn't matter if there's some mapping between those types and functions of type `nat -> nat`.

That's the thing. In some languages, this mapping doesn't always exist.

> AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM.

The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., what you get if your language has parametric polymorphism (and no means to circumvent it, e.g., reflection).

These abstraction barriers might seem just like limitations that buy you nothing, but that's not the case. For example, if your language has abstract types (not the same thing as abstract classes), then you can be sure that any internal invariant violations can be traced to the module where the abstract type is defined. Have fun getting a static guarantee of this kind in C or Java.

> How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers).

Compilation translates programs in a source language into semantically equivalent programs in the target language. Compilation doesn't guarantee that every target language program is expressible in the source language - in fact, this is often not the case.

Re: On Two Views of Computation in Computer Science

#15

Post by marcosdumay »

LolWolf wrote: post #12
pron wrote: post #6

Earlier quoted context omitted.

You can translate and transform many things to many others. The important question is what is the computational complexity of the transformation? If it is large, then the two things are very different. As Scott Aaronson once said, waterfalls could be viewed as playing chess, but as the complexity of the translation from the "waterfall language" to a chess language understandable by humans is as great as the complexit…

Wait, but I thought the question being posed wasn't about the computational complexity of any model but about the power of a given computational model relative to another (e.g. the subject of the CT thesis). Even if we're talking about just computational complexity, if we allow Turing machines with arbitrary oracles, or (equivalently) we allow arbitrary mathematical constructions in languages, I'm still unsure as to…

What I get is that the question is "Does it make any sense to compare the two models, or are they just different things?" and the tentative answer is "They are different things, but one end of TOP coincides with TOC".

I'm fully convinced. Both concepts answer different questions, and that is my favorite test (instead of the OP's "does one model map into the other?").

Re: On Two Views of Computation in Computer Science

#16

Post by marcosdumay »

catnaroek wrote: post #7
Kenji wrote: post #3

It’s really weird that the Church-Turing thesis, which is ridiculously robust at first order, falls apart so comprehensively at higher type. A statement like that makes me feel like Neel Krishnaswami does not understand the Church-Turing thesis at all (what does the Church-Turing thesis even mean at a "higher type"), but considering that this person has significant experience in this field, much more than I do, I am…

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…

Computers in the real world pass all their time evaluating functions from nat -> nat. It is programmers that use different types.

Re: On Two Views of Computation in Computer Science

#17

Post by catnaroek »

marcosdumay wrote: post #16
catnaroek wrote: post #7

Earlier 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…

Computers in the real world pass all their time evaluating functions from nat -> nat. It is programmers that use different types.

Computers in the real world pass all their time executing the instructions that programmers give them. (Okay, not true, they pass most of their time waiting for I/O to complete, or simply doing nothing.) If a linguistic abstraction prevents you from giving certain classes of wrong instructions, that's very useful, even if the abstraction has no runtime manifestation.

Re: On Two Views of Computation in Computer Science

#18

Post by pron »

catnaroek wrote: post #7
Kenji wrote: post #3

It’s really weird that the Church-Turing thesis, which is ridiculously robust at first order, falls apart so comprehensively at higher type. A statement like that makes me feel like Neel Krishnaswami does not understand the Church-Turing thesis at all (what does the Church-Turing thesis even mean at a "higher type"), but considering that this person has significant experience in this field, much more than I do, I am…

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 either). Interpreting a computation as one computing functions on the natural numbers or any other set is an entirely interpretive activity that is external to the computation itself.

Re: On Two Views of Computation in Computer Science

#19

Post by pron »

LolWolf wrote: post #12
pron wrote: post #6

Earlier quoted context omitted.

You can translate and transform many things to many others. The important question is what is the computational complexity of the transformation? If it is large, then the two things are very different. As Scott Aaronson once said, waterfalls could be viewed as playing chess, but as the complexity of the translation from the "waterfall language" to a chess language understandable by humans is as great as the complexit…

Wait, but I thought the question being posed wasn't about the computational complexity of any model but about the power of a given computational model relative to another (e.g. the subject of the CT thesis). Even if we're talking about just computational complexity, if we allow Turing machines with arbitrary oracles, or (equivalently) we allow arbitrary mathematical constructions in languages, I'm still unsure as to…

Both models are equally powerful in the things they compute in terms of the Church-Turing Thesis. The TOP view also has other consideration. My point in the article was not to settle the debate on Aaronson's blog but to show that language models and machine models are objectively and inherently so different from one another that comparing them in terms of programming concepts (like types) is meaningless.

Re: On Two Views of Computation in Computer Science

#20

Post by pron »

amatus wrote: post #8
pron wrote: post #5

Earlier 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…

Could you encode all untyped lambda calculus expressions by just numbering them and writing the number as the string of bits? Maybe this enumeration is the "external collaborator" in this case, but it's a very simple one.

You could, but you'd need to spend even more effort before beginning interpretation to turn the number into a form that LC can interpret.
Post reply on HN