11 ms·

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

by kd0amg 10y ago

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

pron 10y ago
> 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.
- catnaroek 10y ago
  > I don't see how. That inherent complexity is precisely that computed by the machine The same function may be computed by different procedures with different complexity. > rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership Not all types denote sets. > There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage. This is the price of capturing the meaning of computation. Of course it doesn't come for free. But, in general, the earlier you do it, the less work it requires. In the limit, if you do it really late (e.g., test suites), it requires an infinite amount of work (searching infinite input spaces).
  - pron 10y ago
    > The same function may be computed by different procedures with different complexity. The whole idea of computational complexity theory, the time- and space-hierarchy theorems, that are generalizations of the halting theorems and are probably the most important theorems in computer science, is that every function has an inherent complexity, that is independent of the algorithm that implements it. The time or space complexity of an algorithm may be greater than or equal to the complexity of the function. You may want to read my blog post about computational complexity in the context of software correctness: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... > Not all types denote sets In this case, what matters is what set they specify (not necessarily denote) and what proof. > This is the price of capturing the meaning of computation. Of course it doesn't come for free. But, in general, the earlier you do it, the less work it requires. In the limit, if you do it really late (e.g., test suites), it requires an infinite amount of work (searching infinite input spaces). First, the computational complexity of verifying a program is the same no matter when it's done. Read my other blog post. Second, I'm talking theoretical computer science here. Obviously there are all sorts of interesting trade offs in real world programming. Finally, the whole point of this article is that language models do this extra computational work and solve a different problem, while the people discussing them often don't notice or point this out.
    - catnaroek 10y ago
      > In this case, what matters is what set they specify (not necessarily denote) and what proof. How does this even make sense? The whole point to specifying something abstractly is that you want to denote anything that satisfies the specification. And what proof are you talking about? Are you confusing “proof” with “typing derivation”? A single term may admit multiple typing derivations. > First, the computational complexity of verifying a program is the same no matter when it's done. You're assuming that you can write correct programs, without taking verification into consideration right from the beginning. This assumption is incorrect.
      - pron 10y ago

by kd0amg 10y ago

pron 10y ago

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

catnaroek 10y ago
> I don't see how. That inherent complexity is precisely that computed by the machine The same function may be computed by different procedures with different complexity. > rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership Not all types denote sets. > There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage. This is the price of capturing the meaning of computation. Of course it doesn't come for free. But, in general, the earlier you do it, the less work it requires. In the limit, if you do it really late (e.g., test suites), it requires an infinite amount of work (searching infinite input spaces).
- pron 10y ago
  > The same function may be computed by different procedures with different complexity. The whole idea of computational complexity theory, the time- and space-hierarchy theorems, that are generalizations of the halting theorems and are probably the most important theorems in computer science, is that every function has an inherent complexity, that is independent of the algorithm that implements it. The time or space complexity of an algorithm may be greater than or equal to the complexity of the function. You may want to read my blog post about computational complexity in the context of software correctness: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... > Not all types denote sets In this case, what matters is what set they specify (not necessarily denote) and what proof. > This is the price of capturing the meaning of computation. Of course it doesn't come for free. But, in general, the earlier you do it, the less work it requires. In the limit, if you do it really late (e.g., test suites), it requires an infinite amount of work (searching infinite input spaces). First, the computational complexity of verifying a program is the same no matter when it's done. Read my other blog post. Second, I'm talking theoretical computer science here. Obviously there are all sorts of interesting trade offs in real world programming. Finally, the whole point of this article is that language models do this extra computational work and solve a different problem, while the people discussing them often don't notice or point this out.
  - catnaroek 10y ago
    > In this case, what matters is what set they specify (not necessarily denote) and what proof. How does this even make sense? The whole point to specifying something abstractly is that you want to denote anything that satisfies the specification. And what proof are you talking about? Are you confusing “proof” with “typing derivation”? A single term may admit multiple typing derivations. > First, the computational complexity of verifying a program is the same no matter when it's done. You're assuming that you can write correct programs, without taking verification into consideration right from the beginning. This assumption is incorrect.
    - pron 10y ago