4 ms·

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.

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.