6 ms·

> Maybe we should call it Turing Machine Science Nope. Turing machines are arbitrary and rather unmathematical. The lambda calculus is a much better computatio

> 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.
      - bregma 5y ago
        > Typically CS cares about the process to find a result, and not just its value nor the possibility or impossibility to find it. Typically, programmers care about the process to find the result. Some programmers are computer scientists. You can not conclude that all computer scientists are programmers, so your statement is based on logical fallacy.
        TuringTest 5y ago
        Computer science still has computational complexity theory and analysis of algorithms as sub-fields, with complexity classes and Big O notation. These very much care about the process to find results, which was the basis for my statement :-) The fallacy is on your interpretation of what I said. There are results in theoretical computer science that don't care about the efficiency in the process; the most essential are the computability theorems exploring what parts of mathematics can be computed, and what we mean by computation anyway. But the most essential part -the halting problem- was resolved long ago, so the lion's share of applications of computing science is in finding practical ways to use computers, which again needs to take efficiency into account.
    - antonvs 5y ago
- antonvs 5y ago
  > 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'd be interested in a source for this. Lambda calculi are used as the basis for several functional programming languages, which seems to argue against the idea that they're less easy to reason about. They're also used as the basis for proof assistants such as Coq. Coq is based on the calculus of constructions, which is a typed lambda calculus. Again, this would be a mystifying choice if lambda calculi are difficult to reason about. > I disagree with your statement that it is more mathematically grounded. I've provided more support for my position here: https://news.ycombinator.com/item?id=27334163 https://news.ycombinator.com/item?id=27334163
  - _game_of_life 5y ago
    According to this: https://plato.stanford.edu/entries/church-turing/ https://plato.stanford.edu/entries/church-turing/ "In his review of Turing’s work, Church himself acknowledged the superiority of Turing’s analysis of effectiveness, saying: computability by a Turing machine … has the advantage of making the identification with effectiveness in the ordinary (not explicitly defined) sense evident immediately. (Church 1937a: 43)" Moreover, Gödel himself (as well as other mathematicians) found Turing machines and Turing's thesis to be more persuasive: Gödel also found Turing’s analysis superior. Kleene related that Gödel was unpersuaded by Church’s thesis until he saw Turing’s formulation: According to a November 29, 1935, letter from Church to me, Gödel “regarded as thoroughly unsatisfactory” Church’s proposal to use λ-definability as a definition of effective calculability. … It seems that only after Turing’s formulation appeared did Gödel accept Church’s thesis. (Kleene 1981: 59, 61) Gödel described Turing’s analysis of computability as “most satisfactory” and “correct … beyond any doubt” (Gödel 1951: 304 and *193?: 168)." For what it's worth, I do think you've started an interesting discussion! You're allowed to have an opinion that you prefer lambda calculus over LCMs (logical computing machines -- a better term for Turing machine's that Turing favoured) for conceptualizing and reasoning about computation mathematically. Myself, I find Conway's game of life to be the superior framework over both lambda calculus and Turing's Logical Computing Machine :-P
    - 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.

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.
    - bregma 5y ago
      > Typically CS cares about the process to find a result, and not just its value nor the possibility or impossibility to find it. Typically, programmers care about the process to find the result. Some programmers are computer scientists. You can not conclude that all computer scientists are programmers, so your statement is based on logical fallacy.
      - TuringTest 5y ago
        Computer science still has computational complexity theory and analysis of algorithms as sub-fields, with complexity classes and Big O notation. These very much care about the process to find results, which was the basis for my statement :-) The fallacy is on your interpretation of what I said. There are results in theoretical computer science that don't care about the efficiency in the process; the most essential are the computability theorems exploring what parts of mathematics can be computed, and what we mean by computation anyway. But the most essential part -the halting problem- was resolved long ago, so the lion's share of applications of computing science is in finding practical ways to use computers, which again needs to take efficiency into account.
  - antonvs 5y ago
antonvs 5y ago
> 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'd be interested in a source for this. Lambda calculi are used as the basis for several functional programming languages, which seems to argue against the idea that they're less easy to reason about. They're also used as the basis for proof assistants such as Coq. Coq is based on the calculus of constructions, which is a typed lambda calculus. Again, this would be a mystifying choice if lambda calculi are difficult to reason about. > I disagree with your statement that it is more mathematically grounded. I've provided more support for my position here: https://news.ycombinator.com/item?id=27334163 https://news.ycombinator.com/item?id=27334163
- _game_of_life 5y ago
  According to this: https://plato.stanford.edu/entries/church-turing/ https://plato.stanford.edu/entries/church-turing/ "In his review of Turing’s work, Church himself acknowledged the superiority of Turing’s analysis of effectiveness, saying: computability by a Turing machine … has the advantage of making the identification with effectiveness in the ordinary (not explicitly defined) sense evident immediately. (Church 1937a: 43)" Moreover, Gödel himself (as well as other mathematicians) found Turing machines and Turing's thesis to be more persuasive: Gödel also found Turing’s analysis superior. Kleene related that Gödel was unpersuaded by Church’s thesis until he saw Turing’s formulation: According to a November 29, 1935, letter from Church to me, Gödel “regarded as thoroughly unsatisfactory” Church’s proposal to use λ-definability as a definition of effective calculability. … It seems that only after Turing’s formulation appeared did Gödel accept Church’s thesis. (Kleene 1981: 59, 61) Gödel described Turing’s analysis of computability as “most satisfactory” and “correct … beyond any doubt” (Gödel 1951: 304 and *193?: 168)." For what it's worth, I do think you've started an interesting discussion! You're allowed to have an opinion that you prefer lambda calculus over LCMs (logical computing machines -- a better term for Turing machine's that Turing favoured) for conceptualizing and reasoning about computation mathematically. Myself, I find Conway's game of life to be the superior framework over both lambda calculus and Turing's Logical Computing Machine :-P
  - 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.