7 ms·

How then do you state the Church-Turing thesis? I note that the Wikipedia page claims that Church and Turing themselves used the word "function": https://en.w

by tome 10y ago

How then do you state the Church-Turing thesis? I note that the Wikipedia page claims that Church and Turing themselves used the word "function": https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis#Statement_in_Church.27s_and_Turing.27s_words https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis#S...

pron 10y ago
They do use the word function, just not in terms of the language itself, but in the same sense of saying that a falling apple integrates the function from its mass to acceleration; it's a human interpretation of the encoding. I would state the Church-Turing thesis like so: a universal computation model can compute anything any physical machine can. As Hodges says in one of the links in the article, this is how Church and Turing themselves understood it. How would I define "anything"? As a function on any countable set -- the natural numbers, would do -- and I would explain what it mean to compute a function: pick a function, pick an input element, pick a finite representation for the input and output; if a physical machine can compute the output representation from the input representation, so can a universal computation model. I could choose a function between any two countable sets, e.g. (Nat -> Nat) -> (Nat -> Nat): pick a representation for the input and output and all models can compute the same functions, and those are the functions that machines can compute. They differ in abilities regarding representation within the model, but as the language models' representation require very significant computational work, I'd expect their representation to do more: they're paying for it. A C compiler works hard, so you'd expect it to provide you with a representation more suitable to your wishes than machine code. It's just that as a compiler like C translates a "meaningful" language to a machine encoding, everybody notices the work. The language "computation" models work in a vacuum, so I just pointed out that even though they don't translate anything from one representation to another, they still have to pay for their natural representation.
- kd0amg 10y ago
  a function between any two countable sets, e.g. (Nat -> Nat) -> (Nat -> Nat): pick a representation for the input and output There isn't a TM-suitable representation for things of type (Nat -> Nat). No matter how you try to encode a Nat->Nat as a Nat (or a bitstring, if you prefer), you're going to screw up equality (which means you're actually encoding some other type). You'll map two unequal functions to the same Nat, or (more likely) map one function to multiple unequal Nats. This is the difference between how lambda calculi and Turing machines handle higher-order things: A Turing machine can always inspect the "internals," so you need an actual bijection from functions to strings, whereas lambda calculus hides the internals, so it's safe to map one function to multiple syntactic representations.
  - catnaroek 10y ago
    > so it's safe to map one function to multiple syntactic representations. If the benefits of multiple representations of the same value aren't clear from this example, consider a more mundane one: red-black trees as representations of ordered sets. For obvious efficiency reasons, it's not desirable to assign to each ordered set a canonical red-black tree representation.
  - pron 10y ago
    If you take the normal mathematical definition of a function as a mapping from one set to another, pick two sets, pick a representation and all models can compute the same mapped elements. Tell me what your (higher-order) function is — i.e., what output element it maps to what input element — and a TM would compute the exact same outputs. That it can’t internally “reason” about those functions is obvious, but, as I showed, that ability comes at a cost. You could build, say, a Haskell compiler that would pay that cost and translate the language to a machine representation (or, speaking more abstractly, a TM could simulate, say, System Fω — at a computational cost), or you can use an abstract language model without any underlying machine, but the same cost must be paid regardless. This shows that the concept of a type requires actual computational work rather than just a matter of “free” perspective. Your mere presentation of a function as an inhabitant of a type creates a computationally harder problem than presenting a function as a mapping between sets. Put differently, when a typed language model computes a function (Nat -> Nat) -> Nat, it does more work, and solves a harder problem than necessary to compute that function in the normal set-theory sense. You can choose to solve that problem on a TM by simulating type checking if you like, but you can’t compare “compute a function in the set-theory sense” and “compute a function in the type theory sense”, because those are two different problems with two radically different computational complexity costs. You can decide to do that extra work or not (you may want to because you gain benefit from it), but you can’t compare a model that always does — and pays handsomely for it — with one that doesn’t. Otherwise, I could create a language model that solves all NP problems in polynomial time by defining my language as requiring a proof certificate with every input problem, which my model would then check in polynomial time. No one would believe my language actually really solves a computational problem: it simply pushes the difficulty to the collaborator. Equality is also an internal question. Define any relation between two sets (your definition of equality), and all models would be equally able (or unable) to decide it.
- tome 10y ago
  > They do use the word function, just not in terms of the language itself, but in the same sense of saying that a falling apple integrates the function from its mass to acceleration That's the same sense in which Neel means it.
  - pron 10y ago
    No, he doesn't. In the type view, the computation is asked to do two things: compute the output and check a proof that the output belongs to a set. Each of these questions has its own computational complexity. You may say that the first question comes from free by deciding how to think of the apple; the second certainly doesn't. See also https://news.ycombinator.com/item?id=12403508 https://news.ycombinator.com/item?id=12403508
    - tome 10y ago
      Yes he does. If by "Which functions nat -> nat are computable" he meant "functions written in some typed language" then the answer is vacuously "all of them".
      - pron 10y ago
        Not all functions of type nat -> nat are computable in any formalism. You can write plenty of programs that are really of type nat -> nat in say, Haskell, that try to compute a non-computable natural function. They just can't do it and they'll never terminate for some inputs. But they're still perfectly well-formed.

by tome 10y ago

pron 10y ago

They do use the word function, just not in terms of the language itself, but in the same sense of saying that a falling apple integrates the function from its mass to acceleration; it's a human interpretation of the encoding. I would state the Church-Turing thesis like so: a universal computation model can compute anything any physical machine can. As Hodges says in one of the links in the article, this is how Church and Turing themselves understood it. How would I define "anything"? As a function on any countable set -- the natural numbers, would do -- and I would explain what it mean to compute a function: pick a function, pick an input element, pick a finite representation for the input and output; if a physical machine can compute the output representation from the input representation, so can a universal computation model. I could choose a function between any two countable sets, e.g. (Nat -> Nat) -> (Nat -> Nat): pick a representation for the input and output and all models can compute the same functions, and those are the functions that machines can compute. They differ in abilities regarding representation within the model, but as the language models' representation require very significant computational work, I'd expect their representation to do more: they're paying for it. A C compiler works hard, so you'd expect it to provide you with a representation more suitable to your wishes than machine code. It's just that as a compiler like C translates a "meaningful" language to a machine encoding, everybody notices the work. The language "computation" models work in a vacuum, so I just pointed out that even though they don't translate anything from one representation to another, they still have to pay for their natural representation.

kd0amg 10y ago
a function between any two countable sets, e.g. (Nat -> Nat) -> (Nat -> Nat): pick a representation for the input and output There isn't a TM-suitable representation for things of type (Nat -> Nat). No matter how you try to encode a Nat->Nat as a Nat (or a bitstring, if you prefer), you're going to screw up equality (which means you're actually encoding some other type). You'll map two unequal functions to the same Nat, or (more likely) map one function to multiple unequal Nats. This is the difference between how lambda calculi and Turing machines handle higher-order things: A Turing machine can always inspect the "internals," so you need an actual bijection from functions to strings, whereas lambda calculus hides the internals, so it's safe to map one function to multiple syntactic representations.
- catnaroek 10y ago
  > so it's safe to map one function to multiple syntactic representations. If the benefits of multiple representations of the same value aren't clear from this example, consider a more mundane one: red-black trees as representations of ordered sets. For obvious efficiency reasons, it's not desirable to assign to each ordered set a canonical red-black tree representation.
- pron 10y ago
  If you take the normal mathematical definition of a function as a mapping from one set to another, pick two sets, pick a representation and all models can compute the same mapped elements. Tell me what your (higher-order) function is — i.e., what output element it maps to what input element — and a TM would compute the exact same outputs. That it can’t internally “reason” about those functions is obvious, but, as I showed, that ability comes at a cost. You could build, say, a Haskell compiler that would pay that cost and translate the language to a machine representation (or, speaking more abstractly, a TM could simulate, say, System Fω — at a computational cost), or you can use an abstract language model without any underlying machine, but the same cost must be paid regardless. This shows that the concept of a type requires actual computational work rather than just a matter of “free” perspective. Your mere presentation of a function as an inhabitant of a type creates a computationally harder problem than presenting a function as a mapping between sets. Put differently, when a typed language model computes a function (Nat -> Nat) -> Nat, it does more work, and solves a harder problem than necessary to compute that function in the normal set-theory sense. You can choose to solve that problem on a TM by simulating type checking if you like, but you can’t compare “compute a function in the set-theory sense” and “compute a function in the type theory sense”, because those are two different problems with two radically different computational complexity costs. You can decide to do that extra work or not (you may want to because you gain benefit from it), but you can’t compare a model that always does — and pays handsomely for it — with one that doesn’t. Otherwise, I could create a language model that solves all NP problems in polynomial time by defining my language as requiring a proof certificate with every input problem, which my model would then check in polynomial time. No one would believe my language actually really solves a computational problem: it simply pushes the difficulty to the collaborator. Equality is also an internal question. Define any relation between two sets (your definition of equality), and all models would be equally able (or unable) to decide it.
tome 10y ago
> They do use the word function, just not in terms of the language itself, but in the same sense of saying that a falling apple integrates the function from its mass to acceleration That's the same sense in which Neel means it.
- pron 10y ago
  No, he doesn't. In the type view, the computation is asked to do two things: compute the output and check a proof that the output belongs to a set. Each of these questions has its own computational complexity. You may say that the first question comes from free by deciding how to think of the apple; the second certainly doesn't. See also https://news.ycombinator.com/item?id=12403508 https://news.ycombinator.com/item?id=12403508
  - tome 10y ago
    Yes he does. If by "Which functions nat -> nat are computable" he meant "functions written in some typed language" then the answer is vacuously "all of them".
    - pron 10y ago
      Not all functions of type nat -> nat are computable in any formalism. You can write plenty of programs that are really of type nat -> nat in say, Haskell, that try to compute a non-computable natural function. They just can't do it and they'll never terminate for some inputs. But they're still perfectly well-formed.