6 ms·

Is This a Turing Machine?

39 points by martyalain 6y ago

martyalain 6y ago
This question is bound to two other pages: - http://lambdaway.free.fr/lambdawalks/?view=meta3 http://lambdaway.free.fr/lambdawalks/?view=meta3 - http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy Please don't be evil. It's just a question.
qubex 6y ago
Isn’t this just an illustration of the Church-Turing Thesis? https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis
- bhntr3 6y ago
  From the article: > It's not so amazing, the λ calculus is equivalent to a Turing machine. It seems meta3 is a very basic implementation of the lambda calculus. But I believe the equivalence of Turing machines and the lambda calculus is proven. The church Turing thesis is a bit more. My understanding is that it conjectures that there is nothing that can be computed that can't be computed by a Turing machine or the lambda calculus. So nothing more powerful than the lambda calculus exists. I'm not sure this article shows that.
  - isaachier 6y ago
    Usually the combination of names for the theory means that researchers recognize both versions as largely equivalent (e.g. Newton-Leibnitz axiom). The contention that the combined theories must be the definition of computability should be true about each theory in isolation. If a Turing machine cannot calculate any computable problem, then why bother defining a Turing machine? What is the purpose of the definition if not to prove that any computable problem can be solved using the device? The same goes for lambda calculus.
    - bhntr3 6y ago
      I think you're commenting on this line? > can't be computed by a Turing machine or the lambda calculus I agree they're equivalent. That's been proven. Maybe that would be clearer if it said "both a turing machine and the lambda calculus"? That's how I meant it. Anyway I was just trying to add to the discussion by pointing out that what makes the Church-Turing Thesis a thesis or conjecture is that it hasn't been proven that "any computable problem can be solved using the device". That's generally accepted but not proven. The equivalence of turing machines and the lambda calculus is actually a theorem though because it has been proven.
      - tialaramex 6y ago
        Yet, it's a conjecture because it hasn't been proven. It's unprovable in fact. Church-Turing is in effect a statement of belief about what computation is. Strong Church-Turing is a statement of belief about our universe. But it's normal to accept Church-Turing (though not Strong Church-Turing) because once you follow what Gödel, Church and Turing had uncovered the alternatives seem intuitively crazy - Church-Turing has to be right. It's like accepting Modus Ponens and Modus Tollens. I can't present a useful logical argument for why you should accept those because my logical argument will end up relying on them, if you won't accept them then we've nothing further to talk about.
        bhntr3 6y ago
        I agree with that. Would you agree that the Church-Turing Thesis is different from the equivalence between the lambda calculus and Turing machines? I was trying to argue that even if Church-Turing were somehow (magically) invalidated that the equivalence of the lambda calculus and Turing machines would still hold. Thanks for bringing up strong Church-Turing. It was interesting to read about it here (https://plato.stanford.edu/entries/church-turing/#StroWeakFormMaxiThes https://plato.stanford.edu/entries/church-turing/#StroWeakFo...) I think I had a broader interpretation of Church-Turing than I should. I was thinking that if we somehow discovered a working oracle machine on Mars, it would invalidate Church-Turing. But that article says: > the thesis concerns what a human being can achieve when working by rote, with paper and pencil (ignoring contingencies such as boredom, death, or insufficiency of paper)
- martyalain 6y ago
  I don't think so. This is a very simple implementation of lambda calculus showing as simply as possible how on two operations, abstraction and application, can be built the data and control structures at the bottom of a programming language: booleans, pairs, lists, recursion, numbers. Everything else being syntactic sugar. In theory.
M5x7wI3CmbEem10 6y ago
could ML language models be turing complete if they are able to solve functions given parameters in English? e.g. “x is a variable. y is equal to two plus x. if x is two, what is y?” and when run, it outputs four. what would be the implications of this?
- frabert 6y ago
  Maybe a lame answer, but it is my understanding that current ML models are based around neural networks, and NN can easily encode NAND gates which are universal, so they are already Turing-complete.
  - bhntr3 6y ago
    Here's an interesting paper on the topic. It seems that only some NN architectures are turing complete: https://arxiv.org/pdf/1901.03429.pdf https://arxiv.org/pdf/1901.03429.pdf To the essence of what I think the original question is asking: It seems possible (due to the turing completeness of some NN architectures) that a language model could learn a sub-network that was a turing complete computational framework + problem solver and then use that to solve problems in natural language. But it also seems highly unlikely that it would actually play out that way. The linked paper has a nice summary of attempts to build neural nets that learn algorithms. It seems this more direct approach would be likely to yield a result faster than waiting for such a capability to emerge in GPT-12 or something. Of course most ML models execute from within a turing complete programming language/execution environment anyway. If we want to solve math problems, it might be easier to train a model to translate natural language into a more formal definition (afaik this is still very hard) and then hand off the formal definition of the problem to an automated theorem prover. After all, being turing complete doesn't make all problems solvable or tractable from a run time / memory perspective and that's probably the bigger bottleneck when it comes to solving hard math problems.
- jobigoud 6y ago
  > x is a variable. y is equal to two plus x. if x is two, what is y? Alternative answer: "y is a variable".
martyalain 6y ago
I wonder why until now nobody wrote any comment about the content of this paper, a very simple implementation of lambda calculus showing as simply as possible how on two operations, abstraction and application, can be built the data and control structures at the bottom of a programming language: booleans, pairs, lists, recursion, numbers... And so, no answer to my question.
- martyalain 6y ago
  About this paper Simon Peyton Jones (Haskell, ...) mailed me: "It makes sense, yes, but it’s not clear what is new. This is just the untyped lambda calculus and church numerals, isn’t it? All good, but not new. Of course, old is good – it has stood the test of time. Lambda calculus is fantastically small yet it is Turing complete. Sometimes the implementation makes a difference." And my answer was: " Yes "Sometimes the implementation makes a difference" and here we are, the implementation of metatalk is absolutely different. As it can be seen at the end of this page http://lambdaway.free.fr/lambdawalks/?view=meta3 http://lambdaway.free.fr/lambdawalks/?view=meta3 in the "Annexe" section. Nothing but a hundred of vanilla javascript lines, which are the kernel of lambdatalk. Your opinion is welcome.

39 points by martyalain 6y ago

This question is bound to two other pages: - http://lambdaway.free.fr/lambdawalks/?view=meta3 http://lambdaway.free.fr/lambdawalks/?view=meta3 - http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy Please don't be evil. It's just a question.

qubex 6y ago

Isn’t this just an illustration of the Church-Turing Thesis? https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis

bhntr3 6y ago
From the article: > It's not so amazing, the λ calculus is equivalent to a Turing machine. It seems meta3 is a very basic implementation of the lambda calculus. But I believe the equivalence of Turing machines and the lambda calculus is proven. The church Turing thesis is a bit more. My understanding is that it conjectures that there is nothing that can be computed that can't be computed by a Turing machine or the lambda calculus. So nothing more powerful than the lambda calculus exists. I'm not sure this article shows that.
- isaachier 6y ago
  Usually the combination of names for the theory means that researchers recognize both versions as largely equivalent (e.g. Newton-Leibnitz axiom). The contention that the combined theories must be the definition of computability should be true about each theory in isolation. If a Turing machine cannot calculate any computable problem, then why bother defining a Turing machine? What is the purpose of the definition if not to prove that any computable problem can be solved using the device? The same goes for lambda calculus.
  - bhntr3 6y ago
    I think you're commenting on this line? > can't be computed by a Turing machine or the lambda calculus I agree they're equivalent. That's been proven. Maybe that would be clearer if it said "both a turing machine and the lambda calculus"? That's how I meant it. Anyway I was just trying to add to the discussion by pointing out that what makes the Church-Turing Thesis a thesis or conjecture is that it hasn't been proven that "any computable problem can be solved using the device". That's generally accepted but not proven. The equivalence of turing machines and the lambda calculus is actually a theorem though because it has been proven.
    - tialaramex 6y ago
      Yet, it's a conjecture because it hasn't been proven. It's unprovable in fact. Church-Turing is in effect a statement of belief about what computation is. Strong Church-Turing is a statement of belief about our universe. But it's normal to accept Church-Turing (though not Strong Church-Turing) because once you follow what Gödel, Church and Turing had uncovered the alternatives seem intuitively crazy - Church-Turing has to be right. It's like accepting Modus Ponens and Modus Tollens. I can't present a useful logical argument for why you should accept those because my logical argument will end up relying on them, if you won't accept them then we've nothing further to talk about.
      - bhntr3 6y ago
        I agree with that. Would you agree that the Church-Turing Thesis is different from the equivalence between the lambda calculus and Turing machines? I was trying to argue that even if Church-Turing were somehow (magically) invalidated that the equivalence of the lambda calculus and Turing machines would still hold. Thanks for bringing up strong Church-Turing. It was interesting to read about it here (https://plato.stanford.edu/entries/church-turing/#StroWeakFormMaxiThes https://plato.stanford.edu/entries/church-turing/#StroWeakFo...) I think I had a broader interpretation of Church-Turing than I should. I was thinking that if we somehow discovered a working oracle machine on Mars, it would invalidate Church-Turing. But that article says: > the thesis concerns what a human being can achieve when working by rote, with paper and pencil (ignoring contingencies such as boredom, death, or insufficiency of paper)
martyalain 6y ago
I don't think so. This is a very simple implementation of lambda calculus showing as simply as possible how on two operations, abstraction and application, can be built the data and control structures at the bottom of a programming language: booleans, pairs, lists, recursion, numbers. Everything else being syntactic sugar. In theory.

M5x7wI3CmbEem10 6y ago

could ML language models be turing complete if they are able to solve functions given parameters in English? e.g. “x is a variable. y is equal to two plus x. if x is two, what is y?” and when run, it outputs four. what would be the implications of this?

frabert 6y ago
Maybe a lame answer, but it is my understanding that current ML models are based around neural networks, and NN can easily encode NAND gates which are universal, so they are already Turing-complete.
- bhntr3 6y ago
  Here's an interesting paper on the topic. It seems that only some NN architectures are turing complete: https://arxiv.org/pdf/1901.03429.pdf https://arxiv.org/pdf/1901.03429.pdf To the essence of what I think the original question is asking: It seems possible (due to the turing completeness of some NN architectures) that a language model could learn a sub-network that was a turing complete computational framework + problem solver and then use that to solve problems in natural language. But it also seems highly unlikely that it would actually play out that way. The linked paper has a nice summary of attempts to build neural nets that learn algorithms. It seems this more direct approach would be likely to yield a result faster than waiting for such a capability to emerge in GPT-12 or something. Of course most ML models execute from within a turing complete programming language/execution environment anyway. If we want to solve math problems, it might be easier to train a model to translate natural language into a more formal definition (afaik this is still very hard) and then hand off the formal definition of the problem to an automated theorem prover. After all, being turing complete doesn't make all problems solvable or tractable from a run time / memory perspective and that's probably the bigger bottleneck when it comes to solving hard math problems.
jobigoud 6y ago
> x is a variable. y is equal to two plus x. if x is two, what is y? Alternative answer: "y is a variable".

martyalain 6y ago

I wonder why until now nobody wrote any comment about the content of this paper, a very simple implementation of lambda calculus showing as simply as possible how on two operations, abstraction and application, can be built the data and control structures at the bottom of a programming language: booleans, pairs, lists, recursion, numbers... And so, no answer to my question.

martyalain 6y ago
About this paper Simon Peyton Jones (Haskell, ...) mailed me: "It makes sense, yes, but it’s not clear what is new. This is just the untyped lambda calculus and church numerals, isn’t it? All good, but not new. Of course, old is good – it has stood the test of time. Lambda calculus is fantastically small yet it is Turing complete. Sometimes the implementation makes a difference." And my answer was: " Yes "Sometimes the implementation makes a difference" and here we are, the implementation of metatalk is absolutely different. As it can be seen at the end of this page http://lambdaway.free.fr/lambdawalks/?view=meta3 http://lambdaway.free.fr/lambdawalks/?view=meta3 in the "Annexe" section. Nothing but a hundred of vanilla javascript lines, which are the kernel of lambdatalk. Your opinion is welcome.