8 ms·

If anything, if we want to take computation more seriously, we should adopt a foundation that accounts for non-terminating computation natively. One defect of M

If anything, if we want to take computation more seriously, we should adopt a foundation that accounts for non-terminating computation natively. One defect of MLTT is that, when you add non-terminating computation to it, the mathematical structures you can describe in it get horribly deformed. So MLTT users tend to limit themselves to a world where computation can't be expressed unless you have established beforehand that it will halt. What a sorry state of affairs! (Of course, ZFC is even worse in this regard, at least in MLTT you have a more or less direct relationship between programming and proving.) Fortunately, I think the solution already exists, although the details might yet have to be polished: take Paul Blain Levy's “call by push value” (which distinguishes between values and computations), and make the dependent type formers (sigma and pi) range over values and only values...

pron 10y ago
> If anything, if we want to take computation more seriously, we should adopt a foundation that accounts for non-terminating computation natively... Of course, ZFC is even worse in this regard. I really don't understand this line of argument, regardless of the conclusion. Does the application of math to physics suggest that we should adopt a logical foundation of mathematics that does not allow expressing speed quantities greater than the speed of light? This notion may not be as far-fetched as it may seem, because the sole justification for defining problems that take an infinite number of steps to compute as "non-computable" in the first place was physical, as was Brouwer's justification for intuitionistic mathematics. Moreover, Turing quickly realized that computability (or its converse, non-termination) are crude approximations for feasibility (or tractability), that was more fully developed later. And we could continue this argument further to any degree, so why stop at computability?
- catnaroek 10y ago
  With all due respect to physicists and their work, physics doesn't belong in the foundation of mathematics. If our understanding of physics changed drastically tomorrow (an admittedly very improbable event), all mathematics not directly related to physics should remain unaffected. On the other hand, computation does belong in the foundations: constructing and verifying proofs (even informal ones) is computing, and it is the role of foundations to tell us how those computations can be carried out in a pleasant way. Any change in our understanding of computation should lead us to revise how we construct and verify proofs.
  - pron 10y ago
    But the definition of computation is physical. The Church-Turing thesis is a physical hypothesis. It is conceivable that a new physical discovery will contradict the Church-Turing thesis, and with it the definition of what is computable (and in particular how we construct and verify proofs, which is but a small part of computation).
    - catnaroek 10y ago
      > But the definition of computation is physical. A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical. In particular, computation is just having state transitions, not necessarily in a physical system. (Just like recursion is any form of self-reference in any definition, not necessarily procedure definitions.) > The Church-Turing thesis is a physical hypothesis. Then let's not mention it, and stick to what can be dealt with mathematically.
      - pron 10y ago
        > A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical. I'm not sure I understand your point. It is true that any computation can be modeled mathematically, but so can any other physical process. Also, computation does not require a specific physical implementation and is an abstract concept, but so what? Gödel, Turing and von Neumann were very well aware that computation is a physical/philosophical concept described mathematically, not a purely mathematical one. > Then let's not mention it, and stick to what can be dealt with mathematically. But the definition of what is computable and what isn't depends on the Church-Turing thesis.
    - eastWestMath 10y ago
      Computation is an entirely abstract thing. Nowhere does the definition of Turing machines or the lambda calculus makes any reference to actual physical things.
      - pron 10y ago

pron 10y ago

> If anything, if we want to take computation more seriously, we should adopt a foundation that accounts for non-terminating computation natively... Of course, ZFC is even worse in this regard. I really don't understand this line of argument, regardless of the conclusion. Does the application of math to physics suggest that we should adopt a logical foundation of mathematics that does not allow expressing speed quantities greater than the speed of light? This notion may not be as far-fetched as it may seem, because the sole justification for defining problems that take an infinite number of steps to compute as "non-computable" in the first place was physical, as was Brouwer's justification for intuitionistic mathematics. Moreover, Turing quickly realized that computability (or its converse, non-termination) are crude approximations for feasibility (or tractability), that was more fully developed later. And we could continue this argument further to any degree, so why stop at computability?

catnaroek 10y ago
With all due respect to physicists and their work, physics doesn't belong in the foundation of mathematics. If our understanding of physics changed drastically tomorrow (an admittedly very improbable event), all mathematics not directly related to physics should remain unaffected. On the other hand, computation does belong in the foundations: constructing and verifying proofs (even informal ones) is computing, and it is the role of foundations to tell us how those computations can be carried out in a pleasant way. Any change in our understanding of computation should lead us to revise how we construct and verify proofs.
- pron 10y ago
  But the definition of computation is physical. The Church-Turing thesis is a physical hypothesis. It is conceivable that a new physical discovery will contradict the Church-Turing thesis, and with it the definition of what is computable (and in particular how we construct and verify proofs, which is but a small part of computation).
  - catnaroek 10y ago
    > But the definition of computation is physical. A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical. In particular, computation is just having state transitions, not necessarily in a physical system. (Just like recursion is any form of self-reference in any definition, not necessarily procedure definitions.) > The Church-Turing thesis is a physical hypothesis. Then let's not mention it, and stick to what can be dealt with mathematically.
    - pron 10y ago
      > A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical. I'm not sure I understand your point. It is true that any computation can be modeled mathematically, but so can any other physical process. Also, computation does not require a specific physical implementation and is an abstract concept, but so what? Gödel, Turing and von Neumann were very well aware that computation is a physical/philosophical concept described mathematically, not a purely mathematical one. > Then let's not mention it, and stick to what can be dealt with mathematically. But the definition of what is computable and what isn't depends on the Church-Turing thesis.
  - eastWestMath 10y ago
    Computation is an entirely abstract thing. Nowhere does the definition of Turing machines or the lambda calculus makes any reference to actual physical things.
    - pron 10y ago