On Two Views of Computation in Computer Science • Hacker News Board

Re: On Two Views of Computation in Computer Science

#101

Post by tome » Thu, Sep 01, 2016, 1:52 PM UTC

pron wrote: post #100

tome wrote: post #96

Earlier quoted context omitted.

> Again, you shouldn't be surprised by this at all (I'd think it's rather obvious). I'm not sure why you think that I'm surprised, or even why you think that I disagree with your overall argument. I'm just trying to help you build your argument by pointing out the most obvious aspects which need more careful elucidation. So your claim is that in the physical world strings are more fundamental than trees. Good to know…

I gave a more specific explanation in another comment: trees are more complex because they require nodes to be connected and each node to have no more than one parent. A string is any stream of measurements. The exponential growth of trees doesn't bother me, because you can have a natural encoding that doesn't grow exponentially, and doesn't increase interpretation cost exponentially.

And I gave a more specific objection there too.

A string is quite different from a stream. A string is typically considered random access, for a start.

Re: On Two Views of Computation in Computer Science

#102

Post by pron » Thu, Sep 01, 2016, 1:53 PM UTC

tome wrote: post #98

pron wrote: post #97

Earlier quoted context omitted.

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

> A tree is still more complex than strings, because it has rules: one parent per node and no cycles. Those need to be validated. Hmm, I'm not convinced that this is sufficient to show that strings are simpler. After all, a string has rules too: a cell in the string is either at the beginning, or the end, or the middle, and it has neighbours left, right or not at all depending on those conditions, and at most one suc…

You're talking about the graphical representation of a string. A string is any stream of measurements (over time, if you like).

> If they weren't, I'd be happy writing my day-to-day code in Turing Machines.

And if they weren't, we'd see neurons or DNA using type-theory!

Re: On Two Views of Computation in Computer Science

#103

Post by tome » Thu, Sep 01, 2016, 1:56 PM UTC

pron wrote: post #102

tome wrote: post #98

Earlier quoted context omitted.

> A tree is still more complex than strings, because it has rules: one parent per node and no cycles. Those need to be validated. Hmm, I'm not convinced that this is sufficient to show that strings are simpler. After all, a string has rules too: a cell in the string is either at the beginning, or the end, or the middle, and it has neighbours left, right or not at all depending on those conditions, and at most one suc…

You're talking about the graphical representation of a string. A string is any stream of measurements (over time, if you like). > If they weren't, I'd be happy writing my day-to-day code in Turing Machines. And if they weren't, we'd see neurons or DNA using type-theory!

Since you seem to have thought about the fine details of this much more than you are letting on here and on your blog post I suggest you post an addendum (or even a new blog post) to be more precise about what exactly they are. There's a lot missing as it stands, and interested readers like myself are left to fill in the blanks.

Re: On Two Views of Computation in Computer Science

#104

Post by kd0amg » Thu, Sep 01, 2016, 2:14 PM UTC

pron wrote: post #99

catnaroek wrote: post #93

Earlier quoted context omitted.

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

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

The notion of a function having any inherent complexity is rather at odds with your earlier assertion that putting any sort of meaning on the result of running a Turing machine is strictly human interpretation rather than a hard fact of computation (and of course, you also turn around and favor certain interpretations over others based on the cost of embedding them in your favorite computation model).

Re: On Two Views of Computation in Computer Science

#105

Post by catnaroek » Thu, Sep 01, 2016, 2:15 PM UTC

pron wrote: post #71

kd0amg wrote: post #63

Earlier quoted context omitted.

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

> and solves a harder problem than necessary to compute that function in the normal set-theory sense

People who use set theory as their foundations impose on themselves the even harder task of making sure their mappings are coherent w.r.t. whatever notion of structure they want to work with, i.e., homomorphisms in a category of interest.

> 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

No, this is wrong. Changing the input type means that you are not, in fact, solving the original problem.

Re: On Two Views of Computation in Computer Science

#106

Post by [deleted] » Thu, Sep 01, 2016, 3:28 PM UTC

tome wrote: post #76

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…

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…

[deleted]

Re: On Two Views of Computation in Computer Science

#107

Post by Ericson2314 » Thu, Sep 01, 2016, 4:03 PM UTC

pron wrote: post #89

ittekimasu wrote: post #81

Earlier quoted context omitted.

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?

It shouldn't be.

I'm skeptical of your parsing argument because the normal way to construct type theory terms is inductively in their "native" tree form, which is cheap. Looking at them as a formal language isn't so convenient.

As a PLer, I hope dependently typed langauges see wide use not because they are the one true foundation of everything, but because they are the richest lingua franca for every academic discipline to represent their ideas—I'm personally enamored of such theories as a foundation for math, but I don't know much about the theory of computation and I'm fine if others just see it as a tool.

Anyways once that happens and fields have distilled their intentions into precise models in the lingua franca, perhaps the walls between fields can be broken down and we finally grok each other's concepts.

Re: On Two Views of Computation in Computer Science

#108

Post by pron » Thu, Sep 01, 2016, 4:19 PM UTC

kd0amg wrote: post #104

pron wrote: post #99

Earlier quoted context omitted.

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

The notion of a function having any inherent complexity is rather at odds with your earlier assertion that putting any sort of meaning on the result of running a Turing machine is strictly human interpretation rather than a hard fact of computation (and of course, you also turn around and favor certain interpretations over others based on the cost of embedding them in your favorite computation model).

> The notion of a function having any inherent complexity is rather at odds with your earlier assertion that putting any sort of meaning on the result of running a Turing machine is strictly human interpretation rather than a hard fact of computation

I don't see how. That inherent complexity is precisely that computed by the machine (provided that you're talking about a function in the ordinary, set theory sense, rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership).

> and of course, you also turn around and favor certain interpretations over others based on the cost of embedding them in your favorite computation model

No, the complexity of evaluation differs in the different models by a small factor (polynomial at most), that is much smaller than the complexity differences of the representation. There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage. They aim prove something and proving something comes at a cost. There is no interpretation by which proving a possibly complex theorem is considered of having little complexity.

Re: On Two Views of Computation in Computer Science

#109

Post by joe_the_user » Thu, Sep 01, 2016, 4:27 PM UTC

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…

Well,

Another factor is that Church-Turing "at first order" isn't a mathematical theorem - (notice "thesis", not theorem).

The thesis is that all determinant computation is equivalent to Turing machines and lambda calculus (which are each computable with each other). This is a hypothesis about the physical world (or the "imaginable" world).

Thus Church-Turing is very significant - but not necessarily mathematically significant, as a mathematical theory, it's taken as the equivalence of Turing machines and Church's recursive functions (but that's just a theorem which only suggests the (nonmathematical) thesis.

The thing is, a lot of mathematicians are much more enamored of the mathematical world than the physical world. For an enthusiastic mathematician playing with high order recursive functions, a generalization of the Church-Turing theorem seems much cooler than the statement about the physical world that the Church-Turing thesis implies.

Re: On Two Views of Computation in Computer Science

#110

Post by pron » Thu, Sep 01, 2016, 4:28 PM UTC

catnaroek wrote: post #105

pron wrote: post #71

Earlier quoted context omitted.

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

> and solves a harder problem than necessary to compute that function in the normal set-theory sense People who use set theory as their foundations impose on themselves the even harder task of making sure their mappings are coherent w.r.t. whatever notion of structure they want to work with, i.e., homomorphisms in a category of interest. > Otherwise, I could create a language model that solves all NP problems in poly…

> People who use set theory as their foundations...

Let's not get into this old debate because we'll never get out of it. Suffice it to say that it that there is no doubt that Turing and Church (and Gödel and von Neumann) used set theory as their foundation, and when they said "function" they meant a set-theoretic function, namely a mapping from a domain (set) to a range/co-domain (set). If by "function" you mean a type-theoretic function then you're talking about a computationally harder problem, as you need to compute the underlying set-theoretic function and check a proof. You can certainly ask a TM to simulate a type checker and compute a type-theoretic function. There's actual work involved, and someone must do it. You cannot say that your formalism gives it to you for free, or you'll have a formalism that proves things for free, which is impossible.

> Changing the input type means that you are not, in fact, solving the original problem.

Exactly! But that is precisely what you do when you interpret "function" to mean a "type-theoretic function", and solve a different problem. Any work that needs to be done under the normal meaning of "function" also needs to be done in the typed formalism. If you need to ensure/prove something, there is work and computational complexity involved. Pushing it to a collaborator doesn't make it disappear (let's call this the law of preservation of computational complexity). Someone has to do it, and in no model does it suddenly become free. It's perfectly OK to say that you start counting after much of the hard work is done, but in that case you need to say that your model requires upfront work, and therefore cannot be compared to models that don't. That's my whole point.