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

71–80 of 191 posts

Re: On Two Views of Computation in Computer Science

#71

Post by pron »

kd0amg wrote: post #63
pron wrote: post #56

Earlier 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; it's a human interpretation of the encoding. I would state the Church-Turing thesis like so: a universal computation model can compute anything any physical machine can. As Hodges says in one of the links in the article, this is how Church…

a function between any two countable sets, e.g. (Nat -> Nat) -> (Nat -> Nat): pick a representation for the input and output There isn't a TM-suitable representation for things of type (Nat -> Nat). No matter how you try to encode a Nat->Nat as a Nat (or a bitstring, if you prefer), you're going to screw up equality (which means you're actually encoding some other type ). You'll map two unequal functions to the same…

If you take the normal mathematical definition of a function as a mapping from one set to another, pick two sets, pick a representation and all models can compute the same mapped elements. Tell me what your (higher-order) function is — i.e., what output element it maps to what input element — and a TM would compute the exact same outputs. That it can’t internally “reason” about those functions is obvious, but, as I showed, that ability comes at a cost. You could build, say, a Haskell compiler that would pay that cost and translate the language to a machine representation (or, speaking more abstractly, a TM could simulate, say, System Fω — at a computational cost), or you can use an abstract language model without any underlying machine, but the same cost must be paid regardless.

This shows that the concept of a type requires actual computational work rather than just a matter of “free” perspective. Your mere presentation of a function as an inhabitant of a type creates a computationally harder problem than presenting a function as a mapping between sets. Put differently, when a typed language model computes a function (Nat -> Nat) -> Nat, it does more work, and solves a harder problem than necessary to compute that function in the normal set-theory sense. You can choose to solve that problem on a TM by simulating type checking if you like, but you can’t compare “compute a function in the set-theory sense” and “compute a function in the type theory sense”, because those are two different problems with two radically different computational complexity costs. You can decide to do that extra work or not (you may want to because you gain benefit from it), but you can’t compare a model that always does — and pays handsomely for it — with one that doesn’t.

Otherwise, I could create a language model that solves all NP problems in polynomial time by defining my language as requiring a proof certificate with every input problem, which my model would then check in polynomial time. No one would believe my language actually really solves a computational problem: it simply pushes the difficulty to the collaborator.

Equality is also an internal question. Define any relation between two sets (your definition of equality), and all models would be equally able (or unable) to decide it.

Re: On Two Views of Computation in Computer Science

#72

Post by pron »

catnaroek wrote: post #62
pron wrote: post #58

Earlier quoted context omitted.

> What actually exists in computing is procedures You can't free yourself from thinking in terms of languages :) Not a single one of the machine models -- TM, RAM, neural networks, DNA, digital circuits, quantum computers -- has a concept of a procedure. Procedures are language constructs. Whether you choose to compile Pascal or Haskell to x86 machine code is up to you, but in either case there would be a complexity…

> You can't free yourself from thinking in terms of languages Now would I want to. Why would I deprive myself of the benefits of compositionality, separation of concerns, or simply modeling the problem domain as faithfully as possible? > For meaning you have to pay real, measurable complexity. Complexity in the sense of complexity theory? I don't see how. If you mean the computational cost of type checking, that's in…

> Now would I want to. Why would I deprive myself of the benefits of compositionality, separation of concerns, or simply modeling the problem domain as closely as possible?

But now you're saying that you are interested in programming. TOC is about something else.

> Complexity in the sense of complexity theory?

Yes.

> that's in practice a non-problem as long as the type system is reasonable.

Whether that's an issue for the questions you're interested in asking doesn't define what "in practice" means. It certainly matters for the questions TOC is asking. A model that requires a computationally powerful collaborator -- a programmer -- can't arise spontaneously in nature, for example.

> I don't see the requirement of making sense as a burden.

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.

Re: On Two Views of Computation in Computer Science

#73

Post by pron »

clusmore wrote: post #30
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…

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

> This is like measuring the computational complexity of a mathematical proof - it has no complexity, it's delcarative.

There are few things that are absolute in this universe, but computational complexity is one of them. There is plenty of complexity involved. Have your heard of proof complexity? How do you know that a proof is a proof and how is a proof created? It's pretty much the core of P vs. NP question (and first discussed by Stephen Cook, the same guy who formally framed P vs. NP): https://en.wikipedia.org/wiki/Proof_complexity

Actually, the first one who asked the question of P vs. NP was Kurt Gödel (https://rjlipton.wordpress.com/the-gdel-letter/), and as a mathematician, he was very much interested in the complexity (although he didn't use that word) of proofs. He said that if P = NP (not in those words):

> If there really were a machine with φ(n) ∼ k ⋅ n (or even ∼ k ⋅ n2), this would have consequences of the greatest importance. Namely, it would obviously mean that in spite of the undecidability of the Entscheidungsproblem, the mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine.

Re: On Two Views of Computation in Computer Science

#74

Post by tome »

pron wrote: post #56
tome wrote: post #31

Earlier quoted context omitted.

How then do you state the Church-Turing thesis? I note that the Wikipedia page claims that Church and Turing themselves used the word "function": https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis#S...

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; it's a human interpretation of the encoding. I would state the Church-Turing thesis like so: a universal computation model can compute anything any physical machine can. As Hodges says in one of the links in the article, this is how Church…

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

Re: On Two Views of Computation in Computer Science

#75

Post by joe_the_user »

Honestly,

I think Aaronson is clearly and transparently correct about Church-Turing and higher types. Computation on higher types is just a higher-order construct having no more to do with computation as we understand it than other higher order constructs like Hilbert Spaces.

Re: On Two Views of Computation in Computer Science

#76

Post by tome »

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…

Regarding (1), can you give a compelling higher-order example for which Church-Turing fails?

On Scott's blog Neel talked about functions '(unit -> bool) -> (unit -> bool) -> bool', but this example seems spurious. He asserted that Turing Machines could receive the arguments Godel encoded but the Lambda Calculus couldn't. I don't see why. If you also let the Lambda Calculus receive its arguments Godel encoded then it can inspect them and perform the same dovetailing that the Turing Machine would.

Do you know of a more compelling example?

Re: On Two Views of Computation in Computer Science

#77

Post by pron »

AnimalMuppet wrote: post #28
pron wrote: post #19

Earlier quoted context omitted.

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

Yes, but it goes a little further. I can't say my way is superior to yours if my way means solving a harder task and paying market price for it.

I got the leather seats because I chose to pay full price for them. That they come as a standard option with the car because the car is more expensive is not an argument. You can choose to pay the same difference in price and have them installed in your car, too.

Whether those leather seats matter or not is no longer an objective question but a question of values, and here is where caring about completely different values is the point.

Re: On Two Views of Computation in Computer Science

#78

Post by pron »

tome wrote: post #74
pron wrote: post #56

Earlier 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; it's a human interpretation of the encoding. I would state the Church-Turing thesis like so: a universal computation model can compute anything any physical machine can. As Hodges says in one of the links in the article, this is how Church…

> 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

Re: On Two Views of Computation in Computer Science

#79

Post by tome »

pron wrote: post #5
pklausler wrote: post #4

The author contends in the article's abstract that machine models are "self-contained" whereas "language models" (not clearly defined, but meant to encompass at least an untyped lambda calculus) are not. 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.

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.

Re: On Two Views of Computation in Computer Science

#80

Post by tome »

pron wrote: post #54
l_dopa wrote: post #40

Earlier quoted context omitted.

Why is the complexity of parsing well-formed states from strings somehow interesting? If you generalize to trees and pick the right alphabet, suddenly every element of your datatype is a well-formed lambda term. It's also unclear if you're talking about the complexity of type inference or type checking, what annotations you're allowing, etc. Your claims about complexity re: states of typed languages are too hand-wavy…

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

Post reply on HN