Jtdylktuy

I recently asked myself a question concerning a constructivist reading of the Church-Turing thesis. Let us give the latter in the following formulation: put $EC(f)$ for "$f$ is effectively computable" and $R(f)$ for "$f$ is recursive", then $EC(f) rightarrow R(f)$.

Now, in a constructivist reading, $EC(f) rightarrow R(f)$ holds iff we have a total constructive function $h(x, y)$ such that, for every effectively computable $f$, for every $pi$ proof of $EC(f)$, $h(f, pi)$ is a proof of $R(f)$. However, it is generally admitted that "total constructive function" means nothing but "effectively computable function". So, if $h(x, y)$ is a total constructive function, it is an effectively computable function, and hence it should be, so to say, auto-applicable, i.e., it should be able to prove of itself that, if it is an effectively computable function, then it is a recursive function, i.e. again, for every $pi$ proof of $EC(h(x, y))$, $h(h(x, y), pi)$ is a proof of $R(h(x, y))$.

I was wondering if an auto-applicability of this kind, together with what $h(x, y)$ is supposedly expected to do, may create some problematic diagonalizations. What would you think about that?

Ok, so, as far as I understand, there seems to be two arguments that may concern my question. The first stems from the observation that, in an extensional approach, a Church function $(N to N) to N$ is injective and, provided it also is surjective or decidable, one easily derive a contradiction. However, this argument fails in that there are models providing an injective function $(N to N) to N$.

The second is instead based on the fact that, thanks to Kleene $T$ predicate, one can encode an algorithm $h(x, x) : (N to N) to N$ deciding whether programs halt or not. One can then define a diagonal function $$[lambda x : N. neg h(x, x)] : N to N$$ for which the Church function would give us a code, say $n$. But then, we have a contradiction when we consider $$h(n, n)$$ However, I can't see how the contradiction is derived here, it maybe is $$h(n, n) = 1 leftrightarrow d(n) text{halts} leftrightarrow neg h(n, n) = 1 leftrightarrow h(n, n) = 0$$ is that correct?

However, the problem with Church's thesis here does not really derive from the fact that computable functions are proved to be recursive by an auto-applicable computable function. It derives from the decidability of function equality, which, again if I am not wrong, implies that one can encode a decision algorithm.

This still isn't a definite answer to your question, but a comment would not cut it.

The source of issues (I think) in the presentation of "Church's law" above is that is a statement about functions:

$$∀ f : ℕ → ℕ. R(f)$$

where:

$$R(f) = ∃ n. ∀ m. T(n,m,f(m))$$

or something of that sort. Interpreted in the usual propositions-as-types way, this kind of says that 'source code' must be recoverable from a function. This is easy if $ℕ → ℕ$ just is source code (i.e. $ℕ$), and you just give it back. But this does not validate extensional equality, because there may be many pieces of source that compute the same extensional function. If you want to have extensionality, you are forced to pick a canonical implementation for each function, which leads to decidability of functions.

However, you have not stated Church's thesis this way. You said:

$$h : ∀f. EC(f) → R(f)$$

and further, something like:

$$w_h : EC(h)$$

(Imagining that we've worked out exactly how to make that well-typed.) And these aren't necessarily subject to the same pitfalls. First, Church's law has extra 'evidence' in play, the proof of $EC(f)$. We don't need to map functions to their (recursive) source code, we need to map justifications of their 'effective computability' to their source code. But the justification of effective computability might just be a different sort of source code, so this isn't as far fetched. In fact, there might be multiple ways of proving $EC(f)$ that translate to different proofs of $R(f)$, even though we don't care about the difference since they're "propositions." So we might have:

$$f : ℕ → ℕ, w_f : EC(f)$$
$$g : ℕ → ℕ, w_g : EC(g)$$

with:

$$∀ m. f(m) = g(m)$$

but:

$$w_f neq w_g$$

which is fine. We can only decide equality of $Σ_{f:ℕ→ℕ}EC(f)$ with this way of writing Church's thesis.

Also, I think the idea behind having $w_h$ is all right. If you don't mind my switching things around, one way of presenting all this might be with a modality. The idea is that $square A$ is like the 'effectively computable' subcollection of $A$, or maybe an internal reflection of the 'source code' of $A$ values. So $square(ℕ → ℕ)$ is the collection of things that we know can be used to compute a function, but we may be at more liberty to introspect them. One thing we expect to have is:

$$u : square A → A$$

which allows us to apply our source code (and serves the role of $T$). But also we might have your Church's thesis, which might be like:

$$h : square(ℕ → ℕ) → ℕ$$

which gives us some concrete way of looking at the particular function definition we're dealing with (without having to come up with some way of saying how you can inspect a $square$ type). Maybe we could even be more general and say:

$$h_A : square A → ℕ$$

and then also:

$$w_A : square(square A → ℕ)$$

with:

$$u(w_A) = h_A$$

I'm not certain this all works out with an ability to still have extensional equality of functions, but observe 'source code' of boxed functions, etc. But it is very similar to actual structure that arises in realizability and modest sets.

In this format, the problematic "Church's law" is:

$$(ℕ → ℕ) → square(ℕ → ℕ)$$

which is like a modal collapse, and not something we'd normally expect.

So, I think if you are careful enough, you may be able to have the structure you propose without paradox (and I think something like it is an exciting idea with potential applications), and maintain nice extensional principles where desired. But I don't have a proof, and it's possible someone who knows more (like Bauer) could look at this and immediately give an example of how it's wrong.