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

21–30 of 191 posts

Re: On Two Views of Computation in Computer Science

#21

Post by SilasX »

catnaroek wrote: post #14
SilasX wrote: post #13

Earlier quoted context omitted.

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

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

The mapping exists, just not necessarily within the language; the CTT is orthogonal to practical difficulties of massaging the data into a usable input format. (e.g. how to convert a binary tree in to the TM's format and vice versa)

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

Those all speak to the issue of how difficult it is (for e.g. a human) to implement the function, not whether language/computation model can compute it at all.

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

If you have a computation for which no TM (or asm, C, etc program) exists that computes it, let us know! That would be real progress on the CTT towards a negative answer and a Fields Medal for whoever found it!

Re: On Two Views of Computation in Computer Science

#22

Post by nickpsecurity »

pron wrote: post #18
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…

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

Isn't the computation done with logical cells represented by a composition of boolean functions? And which are synthesized via functions sometimes from a functional language? What does this say about idea that, at ISA or abstract level, you're just doing computation if it's implemented as boolean, state machines.

Note: Next step down are analog components that are basically specific functions on real numbers. That's what I got from studying analog computers anyway.

Re: On Two Views of Computation in Computer Science

#23

Post by LolWolf »

pron wrote: post #19
LolWolf wrote: post #12

Earlier quoted context omitted.

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.

I see, okay; I caught that point in the article through the first part, but the latter part got me stuck back on the same point hence the question. Thank you for the clarification.

Re: On Two Views of Computation in Computer Science

#24

Post by marcosdumay »

catnaroek wrote: post #17
marcosdumay wrote: post #16

Earlier quoted context omitted.

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.

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

No argument about it. But notice that this applies to programmers, not computers.

The article is about two groups talking past each other because of different terminology. When you say that "programming in the real world is seldom about functions of nat -> nat" you are doing the same, due to badly defined meanings of "programming" and "functions".

Re: On Two Views of Computation in Computer Science

#25

Post by TelmoMenezes »

catnaroek wrote: post #11
TelmoMenezes wrote: post #10

Earlier quoted context omitted.

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.

Humm... But the set of Turing Machines is countably infinite, and a nat -> nat function is necessarily representable as a Turing Machine.

Re: On Two Views of Computation in Computer Science

#26

Post by mathgenius »

I think mathematicians would call this "representation theory." This is the whole question of do we think of a calculation as syntax, or can we represent this syntax as a "dynamic", or action; something that is being moved around or transformed.

Some people really are driven to just calculate stuff (pushing language itself around), and others seem to want to know "what does it mean?" Ie. what are the representations of this language. Logicians call this semantics: it's a model for the syntax.

I'm a theoretical physics grad student, and see plenty of this. Most physicists seem to just want to calculate stuff, and don't care where the symbols "live". For me, a calculation is rarely enlightening. I want the context, the type theory that tells me how the pieces talk to each other.

Re: On Two Views of Computation in Computer Science

#27

Post by AnimalMuppet »

pron wrote: post #18
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…

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

But isn't a computation that consumes and produces strings a function String -> String? (Or perhaps ordered_set -> ordered_set?)

It also seems kind of ironic to have the functional programming people in the camp that says that there's no such things as functions...

Re: On Two Views of Computation in Computer Science

#28

Post by AnimalMuppet »

pron wrote: post #19
LolWolf wrote: post #12

Earlier quoted context omitted.

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.

And it seems that most of the "my way is superior to yours" is based on setting up strawmen of "yours" to make it be addressing the same questions as "mine".

Re: On Two Views of Computation in Computer Science

#29

Post by tome »

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?

Sure, in Haskell 'IO ()' cannot be mapped to the set of natural numbers (within the language).

EDIT: In fact I'd guess any function type A -> B where A is infinite cannot be mapped to the naturals.

Re: On Two Views of Computation in Computer Science

#30

Post by clusmore »

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…

>The important question is what is the computational complexity of the transformation?

In my view it makes no sense to use metrics from one model on the other. There is no computational complexity involved in the transformations defined in ToP. This is like measuring the computational complexity of a mathematical proof - it has no complexity, it's delcarative.

Post reply on HN