2
$\begingroup$

I came across the following MO question https://mathoverflow.net/questions/461426/church-turing-thesis-for-higher-order-functions and got confused. The author asks for references of Church-Turing-thesis in higher order context.

As I have understood, the model of computability that is widely accepted is Turing machine and other equivalent formulations. Now, if we move to higher order functions, I fail to see how the C-T thesis could possibly change. Yes, we have different context, but is there a different notion of computability defined in that context? If yes, what is it? If not, how would the higher order settings change what Turing machines can compute? What would it even mean? For example, we (can) have higher order functions in Turing-complete languages, which, in my mind, in a way voids the question, doesn't it?

Yes, there are some trivialities as choosing the domain in the case of $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$, but if we are looking for a computable functional, aren't we referring to some formalisation of computability in the first place, and the C-T thesis is about that, isn't it?

What am I missing?

$\endgroup$
2
  • 1
    $\begingroup$ I think you would do far better to raise a comment on the MO question. I think that the issues is that are there different ways of thinking about the $\Bbb{N} \to \Bbb{N}$ argument of a function $(\Bbb{N}\to\Bbb{N})\to\Bbb{N}$: it could be an oracle, or a code of a Turing machine or an encoding of a set of pairs of natural numbers or ... The experts on MO should be able to help you. $\endgroup$
    – Rob Arthan
    Commented Jan 3 at 22:26
  • $\begingroup$ @RobArthan You are probably correct. I placed a comment in one of the answers and might put out a separate question if the comment leads nowhere. $\endgroup$
    – Jii
    Commented Jan 4 at 7:34

1 Answer 1

1
$\begingroup$

$\newcommand{\Bool}{\mathsf{Bool}}$Higher order cases are more complicated because the details of the 'calling convention' for functions can vary. Consider these two cases:

  1. Turing machines
    • Functions $f : ℕ → ℕ$ are represented by machines $M$ that, when provided with an encoding of a natural number, always halt with an encoding of a natural number
    • Functions $f : (ℕ → ℕ) → ℕ$ are represented by machines $M$ that, when provided with the code of a machine meeting the above specification, always halt with an encoding of a natural number, and when machines $F_1$ and $F_2$ compute the same function $f : ℕ → ℕ$, $M$ yields the same number for both
    • This pattern continues
  2. Lambda calculus
    • Functions $f : ℕ → ℕ$ are represented by lambda terms that, when applied to Church numerals, reduce to Church numerals (or, use Scott numerals instead)
    • Functions $f : (ℕ → ℕ) → ℕ$ are represented by lambda terms that reduce to Church numerals when applied to terms that meet the above criteria
    • The pattern continues

These two methods of representing functions are clearly inequivalent (at least, when generalized in a way I'll explain later).

  1. Turing machines for higher order functions are provided with code for their input, and can do whatever they want with that code as long as they respect extensional equality of the functions that code computes
  2. Lambda terms for higher-order functions are provided with an argument that can be supplied with an input to get a corresponding output. But there is no mechanism to inspect the argument the way a Turing machine can inspect the code.

So, the Turing machine convention allows certain operations that are not possible with the lambda convention. For instance, a Turing machine for a function of type $(ℕ → ℕ) → (ℕ → ℕ) → ℕ$ can interleave the execution of its two arguments. This actually doesn't matter for total functions, but if we consider partial functions $ℕ \rightharpoonup ℕ$, then it allows us to do operations like 'racing' two partial functions. There's no operation for racing the reduction of two lambda terms.

You can do something like the Turing machine convention in lambda calculus, because (the code for) lambda terms can be lambda encoded. Then you can write a term that interleaves the reduction of two encoded terms just like interleaved simulation of two Turing machines. But it isn't the most obvious or convenient way to represent higher order functions in the lambda calculus.

The lambda convention has some nice aspects as well. For instance, I didn't need to add any extensionality condition there. Since the lambda convention just gives a 'black box' that can only be applied to get an output, it's impossible for a representative of a higher-order function to not be extensional. I've seen some arguments that this makes it possible to compute certain things in the lambda setting that cannot be computed in the TM setting, but I can't think of any examples off hand. I think possibly such arguments only apply to non-extensional 'higher order' TMs (or similar, due to Rice's theorem and the like). That is, some problems on non-extensional, higher order computations are undecidable, but are easily checkable about extensional computations.

$\endgroup$
5
  • $\begingroup$ Thank you, but I'm afraid this doesn't answer the question. When talking about the C-T thesis the actual practicalities and conventions don't matter. The thesis is about the expressive power of the model of computation whereas the conventions in each model are just ways to handle the dirty details. But if there really are ways to compute something in lambda-calculus that is not computable in Turing settings, that would be interesting. To best of my knowledge the models are equivalent, even if lambda calculus is enriched with new types. $\endgroup$
    – Jii
    Commented Jan 4 at 3:30
  • $\begingroup$ What exactly is your mathematically precise statement of the Church-Turing thesis? The simple English explanation usually given is too vague to even begin talking about its proof or truth. I think the things you are dismissing as, "just ways to handle the dirty details," are actually essential to having a meaningful mathematical statement. And in the higher order cases, they make the difference between the statement being true or false, as I explained. $\endgroup$
    – Dan Doel
    Commented Jan 4 at 17:28
  • $\begingroup$ That is, a mathematically precise instance of the Church-Turing thesis must talk not just about 'models of computation,' but about objects to be represented and ways of representing in those models. The basic choice is to talk about representing (finite tuples of) natural numbers, in which case it turns out that all models and (reasonable) ways of representing in those models give equivalent results. But there are other choices of objects to be represented where not all ways of representing allow equivalent sets of operations to be computed. $\endgroup$
    – Dan Doel
    Commented Jan 4 at 17:37
  • $\begingroup$ As you stated, there is no precise formulation of the C-T thesis. I guess this makes the discussion difficult. However, I studied this a bit and I start to see what you mean. There seem to be earlier discussion in TCS about the topic cstheory.stackexchange.com/questions/1117/… $\endgroup$
    – Jii
    Commented Jan 4 at 18:58
  • $\begingroup$ Maybe I should add that Turing machines and lambda-calculus compute the same number-theoretical functions. There is just difference on how they can do it. My view is that the "how" is irrelevant on what comes to the C-T thesis. I don't the realizability relevant here, but it could be that I'm just not seeing something (hence the question..). $\endgroup$
    – Jii
    Commented Jan 4 at 19:06

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .