La thèse de Church intensionnelle

Afin d'éviter une confusion, je précise tout de suite que la thèse de Church intensionnelle que je considère concerne toujours les fonctions pensées extensionnellement. La thèse de Church extensionnelle habituelle TC peut être reformulée de la façon suivan$te\; :$

Toute machine universelle est capable de calculer toute fonction calculable par n'importe quelle machine universelle.

La thèse de Church intensionnelle TCI est apparemment plus forte. Elle énonce que

Toute machine universelle est capable de calculer toute fonction calculable par n'importe quelle machine universelle, et cela de la même façon, c'est-à-dire avec le même algorithme (on fait abstraction du temps d'exécution).

La thèse de Church extensionnelle entraîne la thèse de Church intensionnelle. Preuve (informelle). Cela découle directement de la discrétisation de la procédure de calcul. Une machine universelle travaille en effet par étapes successives. Le passage d'une étape à une autre est récursif, de même que la reconnaissance d'une condition d'arrêt, et donc ce passage et cette reconnaissance d'arrêt peuvent être codés ``extensionnellement" par des fonctions récursives et sont donc calculables par n'importe quelle machine universelle. Une autre façon de se convaincre de ce résultat est de réaliser que non seulement on peut écrire dans un langage de programmation $L$_A (c'est-à-dire le langage d'une machine universelle $A$) le code d'une machine universelle quelconque $B$, mais on peut écrire dans tout langage de programmation $L$_A un débogueur ou un traceur capable d'évaluer par étapes successives les $L$_B-programmes, en simulant les étapes successives de la machine universelle $B$. En particulier si une fonction $F$ est calculée par un certain algorithme décrit dans $L$_B, alors un débogueur de $L$_B, écrit en $L$_A, permet à la machine $A$ de calculer $F$ de la même façon que le fait la machine $B$ avec l'algorithme décrit par $L$_B.