4 ms·

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

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

pron 10y ago
> 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.
- catnaroek 10y ago
  Of course, proving things, that is, doing mathematics requires work. But at least it's work that produces a useful result, unlike carrying out computations without paying attention to their meaning. (By the way, this meaning always exists, even if you don't particularly care about it.) And the best moment to study the meaning of a computation, in the sense of minimizing the amount of long-term work, is as early as possible, which is exactly what types force you to do.
  - pron 10y ago
    But this is now a programming discussion, not a computation discussion. Also, I don't think it's right to declare things "useful" only if they're useful to the particular problems you're trying to solve. BTW, any logical formalism forces you to pay attention to meaning; choosing to encode the logic in types has advantages and disadvantages, but it is not at all the only way to logically describe a program.
    - catnaroek 10y ago
      > Also, I don't think it's right to declare things "useful" only if they're useful to the particular problems you're trying to solve. Pray tell, what's the use of a computation without paying attention to its meaning? My use case is simply “knowing the meaning as early as possible”, and there ought to be no discussion that this should be everyone else's use case as well. Nobody performs a computation without some sort of expectation about the relation between the inputs and the outputs. > BTW, any logical formalism forces you to pay attention to meaning I never said types are the only way. For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning.
      - pron 10y ago
        > Pray tell, what's the use of a computation without paying attention to its meaning? First, I don't think that the only way to assign meaning to computation is by formally assigning meaning to the syntactic components that comprise its program, as written in some human-readable language. Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators. Components' meaning may be stated informally. I am not aware that formal meaning is the only valid meaning. People wrote the software that landed men on the moon in assembly; that was pretty meaningful. I believe this is still the prevailing view in computer science. Second, you keep identifying the notion of computation with the notion of a program written by a person. The theory of computation, from its earliest days -- by Turing himself -- has studied computational phenomena in neural networks, genetics (Turing was a pioneer of both NNs and genetic algorithms) and quantum phenomena. Some of the greatest achievements in CS are not specifically related to software (I count at least 20% of all Turing awards). > For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning. Or TLA+, which makes types notoriously more difficult to use by comparison.

pron 10y ago

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

catnaroek 10y ago
Of course, proving things, that is, doing mathematics requires work. But at least it's work that produces a useful result, unlike carrying out computations without paying attention to their meaning. (By the way, this meaning always exists, even if you don't particularly care about it.) And the best moment to study the meaning of a computation, in the sense of minimizing the amount of long-term work, is as early as possible, which is exactly what types force you to do.
- pron 10y ago
  But this is now a programming discussion, not a computation discussion. Also, I don't think it's right to declare things "useful" only if they're useful to the particular problems you're trying to solve. BTW, any logical formalism forces you to pay attention to meaning; choosing to encode the logic in types has advantages and disadvantages, but it is not at all the only way to logically describe a program.
  - catnaroek 10y ago
    > Also, I don't think it's right to declare things "useful" only if they're useful to the particular problems you're trying to solve. Pray tell, what's the use of a computation without paying attention to its meaning? My use case is simply “knowing the meaning as early as possible”, and there ought to be no discussion that this should be everyone else's use case as well. Nobody performs a computation without some sort of expectation about the relation between the inputs and the outputs. > BTW, any logical formalism forces you to pay attention to meaning I never said types are the only way. For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning.
    - pron 10y ago
      > Pray tell, what's the use of a computation without paying attention to its meaning? First, I don't think that the only way to assign meaning to computation is by formally assigning meaning to the syntactic components that comprise its program, as written in some human-readable language. Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators. Components' meaning may be stated informally. I am not aware that formal meaning is the only valid meaning. People wrote the software that landed men on the moon in assembly; that was pretty meaningful. I believe this is still the prevailing view in computer science. Second, you keep identifying the notion of computation with the notion of a program written by a person. The theory of computation, from its earliest days -- by Turing himself -- has studied computational phenomena in neural networks, genetics (Turing was a pioneer of both NNs and genetic algorithms) and quantum phenomena. Some of the greatest achievements in CS are not specifically related to software (I count at least 20% of all Turing awards). > For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning. Or TLA+, which makes types notoriously more difficult to use by comparison.