14 ms·

The Church-Turing thesis is a statement about which functions of type `nat -> nat` are computable, either in the lambda calculus or using Turing machines. This

The Church-Turing thesis is a statement about which functions of type `nat -> nat` are computable, either in the lambda calculus or using Turing machines. This completely disregards: (0) Computational complexity. Neither the lambda calculus nor Turing machines were invented to answer questions of computational complexity. (1) Functions at types other than `nat -> nat`. Curiously enough, programming in the real world is seldom about evaluating functions of type `nat -> nat`.

TelmoMenezes 10y ago
Does a type exist such that it cannot be mapped to the set of natural numbers?
- catnaroek 10y ago
  You mean mapped one-to-one? Depends on your model of computation. For example, in the simply typed lambda calculus, equipped with a natural number type, as well as structural recursion on it (but not general recursion), `nat` and `nat -> nat` aren't isomorphic types.
  - TelmoMenezes 10y ago
    Humm... But the set of Turing Machines is countably infinite, and a nat -> nat function is necessarily representable as a Turing Machine.
    - catnaroek 10y ago
      Externally, in the metalanguage, you can count syntactically distinct terms, and, of course, the collection of terms that have type `nat -> nat` is countable. Internally, in the lambda calculus itself, or a model of it, there are two caveats, however: (0) Nothing guarantees that all internal inhabitants of a type are denotable by external pieces of syntax. For example, most real numbers are undefinable. (There are only countably many formulas over a finite alphabet, but uncountably many real numbers, ergo, most real numbers can't be “pinned down” using a formula. That doesn't prevent them from existing. The situation is exactly the same with a type like `nat -> nat`.) (1) The right internal notion of equality isn't syntactic equality (which doesn't even make sense, for the reason stated above), but extensional equality. If all of this sounds too strange, read more about model theory, Gödel's completeness theorem, and the Löwenheim-Skolem theorems.
      - TelmoMenezes 10y ago
        Yes but the real number that cannot be pinned down using a formula can also not be pinned down using a computation, and we are talking of models of computation.
        catnaroek 10y ago
        > Yes but the real number that cannot be pinned down using a formula can also not be pinned down using a computation, Undefinable real numbers exist, whether you can compute them or not. > and we are talking of models of computation. A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model?
        TelmoMenezes 10y ago
        > Undefinable real numbers exist, whether you can compute them or not. I agree with you, but as you probably know this is a deep ontological question. The meaning of something "existing" has been debated for many centuries, especially for cases such as this. > A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model? There is a difference between rejecting and classifying. I am not proposing a new computational model. Turing's model classifies the busy beaver function as non-computable. Correct? I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines...
        catnaroek 10y ago
        > Turing's model classifies the busy beaver function as non-computable. Correct? Yep. > I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines... Turing never redefined the concept of “countable”, which belongs in set theory. If you had asked him what the cardinality is of the set of functions from the naturals to the naturals, he would've answered you “uncountable, of course”.
    - itscomplex 10y ago
      It is not necessarily representable. By diagonalization, in fact, nat -> nat can be shown to be uncountably infinite. Intuitively, an example nat -> nat function that is uncomputable is ~Ld, the function that, given a natural index i into the diagonal of the table of Turing machines and their accepted strings, returns the opposite of whether machine i accepts string i. The output is then clearly equal to no Turing machine, since it differs in at least one position. In order to encode this function, an oracle is required. As such, nat -> nat uncountability can be shown to be central to proving Turing recognizability.
      - TelmoMenezes 10y ago
        Ok, that's a good point, but it is also true that functions requiring an oracle cannot also be represented in any Turing-complete programming language, right? This seems trivial to prove: any function representable in any given programming language maps to a finite string of characters, and finite strings of characters maps to natural numbers.
- tome 10y ago
  Sure, in Haskell 'IO ()' cannot be mapped to the set of natural numbers (within the language). EDIT: In fact I'd guess any function type A -> B where A is infinite cannot be mapped to the naturals.
SilasX 10y ago
Sorry if I'm missing something fundamental, but (1) shouldn't matter if there's some mapping between a) those types and b) functions of type `nat -> nat`. AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM. IOW, whatever transformation it is that the other-typed function makes (edit: or whatever input-output mapping), it is isomorphic to one on `nat -> nat`. Since computers regularly implement exactly such a mapping, it doesn't sound like a problem. >Curiously enough, programming in the real world is seldom about evaluating functions of type `nat -> nat`. How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers). The whole job of programming can be described as "converting a problem to a format suitable for a fast `nat->nat`-implementing machine"; it's just that several of the layers of the conversion are hidden from you.
- catnaroek 10y ago
  > (1) shouldn't matter if there's some mapping between those types and functions of type `nat -> nat`. That's the thing. In some languages, this mapping doesn't always exist. > AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM. The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., what you get if your language has parametric polymorphism (and no means to circumvent it, e.g., reflection). These abstraction barriers might seem just like limitations that buy you nothing, but that's not the case. For example, if your language has abstract types (not the same thing as abstract classes), then you can be sure that any internal invariant violations can be traced to the module where the abstract type is defined. Have fun getting a static guarantee of this kind in C or Java. > How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers). Compilation translates programs in a source language into semantically equivalent programs in the target language. Compilation doesn't guarantee that every target language program is expressible in the source language - in fact, this is often not the case.
marcosdumay 10y ago
Computers in the real world pass all their time evaluating functions from nat -> nat. It is programmers that use different types.
- catnaroek 10y ago
  Computers in the real world pass all their time executing the instructions that programmers give them. (Okay, not true, they pass most of their time waiting for I/O to complete, or simply doing nothing.) If a linguistic abstraction prevents you from giving certain classes of wrong instructions, that's very useful, even if the abstraction has no runtime manifestation.
  - marcosdumay 10y ago
    > If a linguistic abstraction prevents you from giving certain classes of wrong instructions, that's very useful, even if the abstraction has no runtime manifestation. No argument about it. But notice that this applies to programmers, not computers. The article is about two groups talking past each other because of different terminology. When you say that "programming in the real world is seldom about functions of nat -> nat" you are doing the same, due to badly defined meanings of "programming" and "functions".
    - catnaroek 10y ago
      > But notice that this applies to programmers, not computers. It applies to computers, because it's the computer itself that's preventing you from giving it certain classes of wrong instructions. I'm talking about enforcing things mechanically (type checking), not socially (design patterns, best practices, etc.).
      - marcosdumay 10y ago
        As far as the computer is concerned, it is running a nat -> nat function over some data you passed it, and displaying the result. If you consider that data to be a program, and the resulting messages to be errors, that is completely up to you.
pron 10y ago
> The Church-Turing thesis is a statement about which functions of type `nat -> nat` are computable, either in the lambda calculus or using Turing machines. This is how Krishnaswami frames things. From the TOC perspective, there is no such thing as functions at all. Computations consume and produce strings. Both Church and Turing explain how those strings can encode the natural numbers (there was no talk of types by either). Interpreting a computation as one computing functions on the natural numbers or any other set is an entirely interpretive activity that is external to the computation itself.
- nickpsecurity 10y ago
  Isn't the computation done with logical cells represented by a composition of boolean functions? And which are synthesized via functions sometimes from a functional language? What does this say about idea that, at ISA or abstract level, you're just doing computation if it's implemented as boolean, state machines. Note: Next step down are analog components that are basically specific functions on real numbers. That's what I got from studying analog computers anyway.
  - pron 10y ago
    Turing personally addressed the question of analog computation and determined that they add nothing over discrete machines, as discrete computers can compute anything an analog computer would do to the desired precision that matters to you. He even discussed the subject in his 1936 paper, when he introduced his model. He wrote that eventually one would need to distinguish between two states, and so a model where states can be arbitrarily indistinguishable adds nothing, so you may as well discretize. When he wrote about the operation of the brain he said that it shouldn't matter if the brain is continuous or discrete; its operation could be simulated to arbitrary precision by a discrete process. He did wonder about quantum effects, though (he understood quantum entanglement when he was 16, Hodges writes).
- AnimalMuppet 10y ago
  But isn't a computation that consumes and produces strings a function String -> String? (Or perhaps ordered_set<String> -> ordered_set<String>?) It also seems kind of ironic to have the functional programming people in the camp that says that there's no such things as functions...
tome 10y ago
Regarding (1), can you give a compelling higher-order example for which Church-Turing fails? On Scott's blog Neel talked about functions '(unit -> bool) -> (unit -> bool) -> bool', but this example seems spurious. He asserted that Turing Machines could receive the arguments Godel encoded but the Lambda Calculus couldn't. I don't see why. If you also let the Lambda Calculus receive its arguments Godel encoded then it can inspect them and perform the same dovetailing that the Turing Machine would. Do you know of a more compelling example?
- deleted 10y ago
  [deleted]
- catnaroek 10y ago
  > Regarding (1), can you give a compelling higher-order example for which Church-Turing fails? I never said the Church-Turing thesis fails. I only said that it only claims what it claims. > He asserted that Turing Machines could receive the arguments Gödel encoded but the Lambda Calculus couldn't. I don't see why. In the lambda calculus, if you have the Gödel number of a Turing machine, you can simulate that Turing machine. But if you have a lambda abstraction, you can't produce the Gödel number of a Turing machine that computes the same (partial) function as the lambda abstraction. The only thing you can do with a lambda abstraction is apply it.

TelmoMenezes 10y ago

Does a type exist such that it cannot be mapped to the set of natural numbers?

catnaroek 10y ago
You mean mapped one-to-one? Depends on your model of computation. For example, in the simply typed lambda calculus, equipped with a natural number type, as well as structural recursion on it (but not general recursion), `nat` and `nat -> nat` aren't isomorphic types.
- TelmoMenezes 10y ago
  Humm... But the set of Turing Machines is countably infinite, and a nat -> nat function is necessarily representable as a Turing Machine.
  - catnaroek 10y ago
    Externally, in the metalanguage, you can count syntactically distinct terms, and, of course, the collection of terms that have type `nat -> nat` is countable. Internally, in the lambda calculus itself, or a model of it, there are two caveats, however: (0) Nothing guarantees that all internal inhabitants of a type are denotable by external pieces of syntax. For example, most real numbers are undefinable. (There are only countably many formulas over a finite alphabet, but uncountably many real numbers, ergo, most real numbers can't be “pinned down” using a formula. That doesn't prevent them from existing. The situation is exactly the same with a type like `nat -> nat`.) (1) The right internal notion of equality isn't syntactic equality (which doesn't even make sense, for the reason stated above), but extensional equality. If all of this sounds too strange, read more about model theory, Gödel's completeness theorem, and the Löwenheim-Skolem theorems.
    - TelmoMenezes 10y ago
      Yes but the real number that cannot be pinned down using a formula can also not be pinned down using a computation, and we are talking of models of computation.
      - catnaroek 10y ago
        > Yes but the real number that cannot be pinned down using a formula can also not be pinned down using a computation, Undefinable real numbers exist, whether you can compute them or not. > and we are talking of models of computation. A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model?
        TelmoMenezes 10y ago
        > Undefinable real numbers exist, whether you can compute them or not. I agree with you, but as you probably know this is a deep ontological question. The meaning of something "existing" has been debated for many centuries, especially for cases such as this. > A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model? There is a difference between rejecting and classifying. I am not proposing a new computational model. Turing's model classifies the busy beaver function as non-computable. Correct? I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines...
        catnaroek 10y ago
        > Turing's model classifies the busy beaver function as non-computable. Correct? Yep. > I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines... Turing never redefined the concept of “countable”, which belongs in set theory. If you had asked him what the cardinality is of the set of functions from the naturals to the naturals, he would've answered you “uncountable, of course”.
  - itscomplex 10y ago
    It is not necessarily representable. By diagonalization, in fact, nat -> nat can be shown to be uncountably infinite. Intuitively, an example nat -> nat function that is uncomputable is ~Ld, the function that, given a natural index i into the diagonal of the table of Turing machines and their accepted strings, returns the opposite of whether machine i accepts string i. The output is then clearly equal to no Turing machine, since it differs in at least one position. In order to encode this function, an oracle is required. As such, nat -> nat uncountability can be shown to be central to proving Turing recognizability.
    - TelmoMenezes 10y ago
      Ok, that's a good point, but it is also true that functions requiring an oracle cannot also be represented in any Turing-complete programming language, right? This seems trivial to prove: any function representable in any given programming language maps to a finite string of characters, and finite strings of characters maps to natural numbers.
tome 10y ago
Sure, in Haskell 'IO ()' cannot be mapped to the set of natural numbers (within the language). EDIT: In fact I'd guess any function type A -> B where A is infinite cannot be mapped to the naturals.

SilasX 10y ago

Sorry if I'm missing something fundamental, but (1) shouldn't matter if there's some mapping between a) those types and b) functions of type `nat -> nat`. AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM. IOW, whatever transformation it is that the other-typed function makes (edit: or whatever input-output mapping), it is isomorphic to one on `nat -> nat`. Since computers regularly implement exactly such a mapping, it doesn't sound like a problem. >Curiously enough, programming in the real world is seldom about evaluating functions of type `nat -> nat`. How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers). The whole job of programming can be described as "converting a problem to a format suitable for a fast `nat->nat`-implementing machine"; it's just that several of the layers of the conversion are hidden from you.

catnaroek 10y ago
> (1) shouldn't matter if there's some mapping between those types and functions of type `nat -> nat`. That's the thing. In some languages, this mapping doesn't always exist. > AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM. The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., what you get if your language has parametric polymorphism (and no means to circumvent it, e.g., reflection). These abstraction barriers might seem just like limitations that buy you nothing, but that's not the case. For example, if your language has abstract types (not the same thing as abstract classes), then you can be sure that any internal invariant violations can be traced to the module where the abstract type is defined. Have fun getting a static guarantee of this kind in C or Java. > How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers). Compilation translates programs in a source language into semantically equivalent programs in the target language. Compilation doesn't guarantee that every target language program is expressible in the source language - in fact, this is often not the case.

marcosdumay 10y ago

Computers in the real world pass all their time evaluating functions from nat -> nat. It is programmers that use different types.

catnaroek 10y ago
Computers in the real world pass all their time executing the instructions that programmers give them. (Okay, not true, they pass most of their time waiting for I/O to complete, or simply doing nothing.) If a linguistic abstraction prevents you from giving certain classes of wrong instructions, that's very useful, even if the abstraction has no runtime manifestation.
- marcosdumay 10y ago
  > If a linguistic abstraction prevents you from giving certain classes of wrong instructions, that's very useful, even if the abstraction has no runtime manifestation. No argument about it. But notice that this applies to programmers, not computers. The article is about two groups talking past each other because of different terminology. When you say that "programming in the real world is seldom about functions of nat -> nat" you are doing the same, due to badly defined meanings of "programming" and "functions".
  - catnaroek 10y ago
    > But notice that this applies to programmers, not computers. It applies to computers, because it's the computer itself that's preventing you from giving it certain classes of wrong instructions. I'm talking about enforcing things mechanically (type checking), not socially (design patterns, best practices, etc.).
    - marcosdumay 10y ago
      As far as the computer is concerned, it is running a nat -> nat function over some data you passed it, and displaying the result. If you consider that data to be a program, and the resulting messages to be errors, that is completely up to you.

pron 10y ago

> The Church-Turing thesis is a statement about which functions of type `nat -> nat` are computable, either in the lambda calculus or using Turing machines. This is how Krishnaswami frames things. From the TOC perspective, there is no such thing as functions at all. Computations consume and produce strings. Both Church and Turing explain how those strings can encode the natural numbers (there was no talk of types by either). Interpreting a computation as one computing functions on the natural numbers or any other set is an entirely interpretive activity that is external to the computation itself.

nickpsecurity 10y ago
Isn't the computation done with logical cells represented by a composition of boolean functions? And which are synthesized via functions sometimes from a functional language? What does this say about idea that, at ISA or abstract level, you're just doing computation if it's implemented as boolean, state machines. Note: Next step down are analog components that are basically specific functions on real numbers. That's what I got from studying analog computers anyway.
- pron 10y ago
  Turing personally addressed the question of analog computation and determined that they add nothing over discrete machines, as discrete computers can compute anything an analog computer would do to the desired precision that matters to you. He even discussed the subject in his 1936 paper, when he introduced his model. He wrote that eventually one would need to distinguish between two states, and so a model where states can be arbitrarily indistinguishable adds nothing, so you may as well discretize. When he wrote about the operation of the brain he said that it shouldn't matter if the brain is continuous or discrete; its operation could be simulated to arbitrary precision by a discrete process. He did wonder about quantum effects, though (he understood quantum entanglement when he was 16, Hodges writes).
AnimalMuppet 10y ago
But isn't a computation that consumes and produces strings a function String -> String? (Or perhaps ordered_set<String> -> ordered_set<String>?) It also seems kind of ironic to have the functional programming people in the camp that says that there's no such things as functions...

tome 10y ago

Regarding (1), can you give a compelling higher-order example for which Church-Turing fails? On Scott's blog Neel talked about functions '(unit -> bool) -> (unit -> bool) -> bool', but this example seems spurious. He asserted that Turing Machines could receive the arguments Godel encoded but the Lambda Calculus couldn't. I don't see why. If you also let the Lambda Calculus receive its arguments Godel encoded then it can inspect them and perform the same dovetailing that the Turing Machine would. Do you know of a more compelling example?

deleted 10y ago
[deleted]
catnaroek 10y ago
> Regarding (1), can you give a compelling higher-order example for which Church-Turing fails? I never said the Church-Turing thesis fails. I only said that it only claims what it claims. > He asserted that Turing Machines could receive the arguments Gödel encoded but the Lambda Calculus couldn't. I don't see why. In the lambda calculus, if you have the Gödel number of a Turing machine, you can simulate that Turing machine. But if you have a lambda abstraction, you can't produce the Gödel number of a Turing machine that computes the same (partial) function as the lambda abstraction. The only thing you can do with a lambda abstraction is apply it.