10 ms·

This is good thinking and I am sad to hear that it is unconventional. And now I'll contradict the part of what you said about finite structures: At a theoretic

This is good thinking and I am sad to hear that it is unconventional. And now I'll contradict the part of what you said about finite structures: At a theoretical level, the field deals with infinite structures, namely the Turing Machine tape and infinite time. We use finite Computing Machines to simulate a finite section of that tape in a finite time. Maybe we should call it Turing Machine Science, because we use computers to study the behavior of programs in Turing Machines, just as astronomers use telescopes to study the behavior of atoms in stars and particle physicists use particle accelerators to study the behavior of elementary particles. We will never touch those particles, stars, or Turing Machines, but we can know them, hence the science. Software engineering is like using one's understanding of the emissions of the sun to design better solar panels. Very practical, but you don't use your understanding of gravity-driven fusion reactors every day.

antonvs 5y ago
> Maybe we should call it Turing Machine Science Nope. Turing machines are arbitrary and rather unmathematical. The lambda calculus is a much better computational formalism, more mathematically grounded and oriented, with far more direct practical applications.
- jll29 5y ago
  If you like, we can generalize and call it "computation science" to avoid the focus on the tool/machine in favor of the process.
  - plumeria 5y ago
    https://youtu.be/2Op3QLzMgSY?t=16 https://youtu.be/2Op3QLzMgSY?t=16
  - antonvs 5y ago
    "Computing science" is more commonly used as an alternative, but yes, that approach makes much more sense than focusing on some particular abstraction.
- kaba0 5y ago
  Why would you think that? I believe I’ve read that even Church himself said that Turing machines are a more elegant basis for computations, since they are much easier to mathematically reason about. I’m sure one can prove everything proved for Turing machines for lambda calculus, but I disagree with your statement that it is more mathematically grounded. It may be true in a syntactic form, but definitely not in a mathematical structure one.
  - TuringTest 5y ago
    Turing machines are terribly inefficient, though. They may be easier to reason about than lambda calculus, but not good for practical computing purposes. Their value was in proving that logical and mathematical reasoning could be mechanized with an automatic device, something that had not been clear until then. Computing science cares a lot about building efficient processes. Thus to create real working programs, a better basis is a combination of lambda calculus for defining mathematical structures and (Von Neumann based) agent-based models for defining stateful processes. Modern programming languages are evolving to be capable of representing either model, to adapt themselves to the style more suited to the problem at hand.
    - kaba0 5y ago
      Efficiency is not important at all when you talk about a mathematical proof. Do we really care about a proof using induction taking n or n^2 operations? For seeing whether a given statement holds true, minimizing complexity is the most important.
      - TuringTest 5y ago
        > Efficiency is not important at all when you talk about a mathematical proof. Precisely, and that's the main difference between computer science and the rest of mathematics. Typically CS cares about the process to find a result, and not just its value nor the possibility or impossibility to find it.
        5y ago
- h8hawk 5y ago
  This by the way is the most arrogant comment I've seen on this site.
  - antonvs 5y ago
    What about my comment makes it so arrogant? In case it helps, I've provided some substantiation for my position here: https://news.ycombinator.com/item?id=27334163 https://news.ycombinator.com/item?id=27334163 I should also clarify that I didn't intend to argue that lambda calculus should be the only way of understanding computation, but rather that it doesn't make sense to privilege the Turing machine model, as the comment I was replying to suggested. The Turing machine model is arbitrary, and it is unmathematical in the sense I've described in my comment linked above. A different culture (or species!) would be likely to come up with a different computational machine-like model, but any culture that develops formal logics would be likely to discover the lambda calculus as a consequence of that.
- qsort 5y ago
  This reads like total nonsense to me. Why would Turing machines be 'arbitrary and unmathematical'? What's 'unmathematical' about them? They can be formally and precisely described and I don't know of any mathematician who wouldn't accept TMs as a sound definition.
  - antonvs 5y ago
    Turing machines are arbitrary in that they don't derive from some mathematical basis. You could easily reformulate the abstraction in many different ways, replacing "tape" or a "read/write head" with some other quasi-physical concept that don't normally appear in mathematics. Those concepts are spurious, just provided for their analogy to real-world machines. You can provide formal descriptions for many things - the Perl programming language, for example. I would also call that language unmathematical. You can study such objects mathematically, but they are essentially external objects of study which one is using mathematics to make more tractable. In contrast, Curry and Howard discovered direct correspondences between logic and lambda calculus. For example, intuitionistic natural deduction is isomorphic to typed lambda calculus. The internal languages of Cartesian closed categories are lambda calculi. If Church hadn't discovered lambda calculi, they would have eventually been discovered via one of these correspondences. Wikipedia provides a partial list of these correspondences at https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... : * Girard-Reynolds System F as a common language for both second-order propositional logic and polymorphic lambda calculus * higher-order logic and Girard's System Fω * inductive types as algebraic data type * necessity in modal logic and staged computation * possibility in modal logic and monadic types for effects * The λI calculus corresponds to relevant logic. * The local truth (∇) modality in Grothendieck topology or the equivalent "lax" modality (◯) of Benton, Bierman, and de Paiva (1998) correspond to CL-logic describing "computation types". As such, lambda calculi are inextricably embedded in mathematics and logic, and their core features (ignoring superficial choices such as syntax) are a discovery, rather than an invention. We can't change the equivalences described above, they are facts that arise from the formalisms developed to address subjects like logic and categorical analysis. The same is not true of Turing machines.
  - siraben 5y ago
- tom_mellior 5y ago
  > Turing machines are arbitrary and rather unmathematical. Thus proving the point that a field that studies them cannot be considered a branch of mathematics.
  - antonvs 5y ago
    That might be true if there were no more natural mathematical representations of computation. But as I've pointed out in another comment (https://news.ycombinator.com/item?id=27334163 https://news.ycombinator.com/item?id=27334163), there is such a representation - the lambda calculus.
fnrslvr 5y ago
When you mentioned infinite structures, I thought you'd bring up the idea that our goal to automate often pits us against problems defined as collections of infinitary instances. I don't think the potential infinity of tapes and running times poses as much of a concern by comparison. Maybe computer science is about giving, to borrow a little bit from Hilbert, finitary representation to infinitary structures. (Finitary representation with other properties of interest, such as tractability and whatnot, of course.)

antonvs 5y ago

> Maybe we should call it Turing Machine Science Nope. Turing machines are arbitrary and rather unmathematical. The lambda calculus is a much better computational formalism, more mathematically grounded and oriented, with far more direct practical applications.

jll29 5y ago
If you like, we can generalize and call it "computation science" to avoid the focus on the tool/machine in favor of the process.
- plumeria 5y ago
  https://youtu.be/2Op3QLzMgSY?t=16 https://youtu.be/2Op3QLzMgSY?t=16
- antonvs 5y ago
  "Computing science" is more commonly used as an alternative, but yes, that approach makes much more sense than focusing on some particular abstraction.
kaba0 5y ago
Why would you think that? I believe I’ve read that even Church himself said that Turing machines are a more elegant basis for computations, since they are much easier to mathematically reason about. I’m sure one can prove everything proved for Turing machines for lambda calculus, but I disagree with your statement that it is more mathematically grounded. It may be true in a syntactic form, but definitely not in a mathematical structure one.
- TuringTest 5y ago
  Turing machines are terribly inefficient, though. They may be easier to reason about than lambda calculus, but not good for practical computing purposes. Their value was in proving that logical and mathematical reasoning could be mechanized with an automatic device, something that had not been clear until then. Computing science cares a lot about building efficient processes. Thus to create real working programs, a better basis is a combination of lambda calculus for defining mathematical structures and (Von Neumann based) agent-based models for defining stateful processes. Modern programming languages are evolving to be capable of representing either model, to adapt themselves to the style more suited to the problem at hand.
  - kaba0 5y ago
    Efficiency is not important at all when you talk about a mathematical proof. Do we really care about a proof using induction taking n or n^2 operations? For seeing whether a given statement holds true, minimizing complexity is the most important.
    - TuringTest 5y ago
      > Efficiency is not important at all when you talk about a mathematical proof. Precisely, and that's the main difference between computer science and the rest of mathematics. Typically CS cares about the process to find a result, and not just its value nor the possibility or impossibility to find it.
      - 5y ago
h8hawk 5y ago
This by the way is the most arrogant comment I've seen on this site.
- antonvs 5y ago
  What about my comment makes it so arrogant? In case it helps, I've provided some substantiation for my position here: https://news.ycombinator.com/item?id=27334163 https://news.ycombinator.com/item?id=27334163 I should also clarify that I didn't intend to argue that lambda calculus should be the only way of understanding computation, but rather that it doesn't make sense to privilege the Turing machine model, as the comment I was replying to suggested. The Turing machine model is arbitrary, and it is unmathematical in the sense I've described in my comment linked above. A different culture (or species!) would be likely to come up with a different computational machine-like model, but any culture that develops formal logics would be likely to discover the lambda calculus as a consequence of that.
qsort 5y ago
This reads like total nonsense to me. Why would Turing machines be 'arbitrary and unmathematical'? What's 'unmathematical' about them? They can be formally and precisely described and I don't know of any mathematician who wouldn't accept TMs as a sound definition.
- antonvs 5y ago
  Turing machines are arbitrary in that they don't derive from some mathematical basis. You could easily reformulate the abstraction in many different ways, replacing "tape" or a "read/write head" with some other quasi-physical concept that don't normally appear in mathematics. Those concepts are spurious, just provided for their analogy to real-world machines. You can provide formal descriptions for many things - the Perl programming language, for example. I would also call that language unmathematical. You can study such objects mathematically, but they are essentially external objects of study which one is using mathematics to make more tractable. In contrast, Curry and Howard discovered direct correspondences between logic and lambda calculus. For example, intuitionistic natural deduction is isomorphic to typed lambda calculus. The internal languages of Cartesian closed categories are lambda calculi. If Church hadn't discovered lambda calculi, they would have eventually been discovered via one of these correspondences. Wikipedia provides a partial list of these correspondences at https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... : * Girard-Reynolds System F as a common language for both second-order propositional logic and polymorphic lambda calculus * higher-order logic and Girard's System Fω * inductive types as algebraic data type * necessity in modal logic and staged computation * possibility in modal logic and monadic types for effects * The λI calculus corresponds to relevant logic. * The local truth (∇) modality in Grothendieck topology or the equivalent "lax" modality (◯) of Benton, Bierman, and de Paiva (1998) correspond to CL-logic describing "computation types". As such, lambda calculi are inextricably embedded in mathematics and logic, and their core features (ignoring superficial choices such as syntax) are a discovery, rather than an invention. We can't change the equivalences described above, they are facts that arise from the formalisms developed to address subjects like logic and categorical analysis. The same is not true of Turing machines.
- siraben 5y ago
tom_mellior 5y ago
> Turing machines are arbitrary and rather unmathematical. Thus proving the point that a field that studies them cannot be considered a branch of mathematics.
- antonvs 5y ago
  That might be true if there were no more natural mathematical representations of computation. But as I've pointed out in another comment (https://news.ycombinator.com/item?id=27334163 https://news.ycombinator.com/item?id=27334163), there is such a representation - the lambda calculus.

fnrslvr 5y ago

When you mentioned infinite structures, I thought you'd bring up the idea that our goal to automate often pits us against problems defined as collections of infinitary instances. I don't think the potential infinity of tapes and running times poses as much of a concern by comparison. Maybe computer science is about giving, to borrow a little bit from Hilbert, finitary representation to infinitary structures. (Finitary representation with other properties of interest, such as tractability and whatnot, of course.)