next up previous contents
Next: La thèse de Church Up: La thèse de Church Previous: La thèse de Church

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 suivante :
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 LA (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 LA un débogueur ou un traceur capable d'évaluer par étapes successives les LB-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 LB, alors un débogueur de LB, écrit en LA, 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 LB.
next up previous contents
Next: La thèse de Church Up: La thèse de Church Previous: La thèse de Church

Bruno Marchal
Thu Apr 1 00:14:24 CEST 1999