CALC-AGREG

Au début, nous avons construit l'ensemble des fonctions primitives récursives. On a introduit les schémas primitifs. Avec tout cela, on peut exprimer plein de choses : sommes, produits, minimisation bornée. Cette classe de fonctions correspond à tout ce qu'on peut exprimer en Bucle (un langage avec des boucles "répéter f(n) fois" et des définitions de fonctions, mais on n'a pas le droit à la récursivité). Les algorithmes écrits terminent tous.
On a vu que l'on peut simuler de la récursivité multiple (Fibonacci). On peut aussi simuler des structures de données pour des listes. Les opérations de base (extraire la tête, la queue etc. sont récursives primitives).

Avec le procédé de diagonalisation de Cantor, et en utilisant une énumération que l'on peut effectivement mécaniser, on construit une fonction qui a l'air calculable, mais qui n'est pas primitive.

On introduit alors les fonctions récursives partielles via la minimisation non bornée. Le seule moyen de les rendre totales est d'utiliser des prédicats sûrs. Au niveau langage de programmation, on peut introduire le Mucle (en rajoutant des boucles mu). Les fonctions récursives totales sont les fonctions Mucle dont on a une garantie qu'elle termine et les fonctions récursives partielles correspondent à toutes les fonctions que l'on peut écrire en Mucle.
Si on réapplique le diagonalisation de Cantor aux fonctions récursives totales, on obtient une fonction... mais qui n'a pas l'air calculable. Peut-on décider si un prédicat est sûr ? Avec quel formalisme le prouver ? On a l'impression que l'on a atteint les limites.
C'est la thèse de Church-Turing : c'est l'hypothèse qu'il y ait une correspondance entre les fonctions récursives totales et ce que l'on peut calculer avec une machine réelle (ordinateur, cerveau etc.).