Argument diagonal, point fixe, théorie des combinateurs
La théorie des combinateurs d’Haskell Curry fournit un calcul simple, construit à partir de deux combinateurs propres (S et K) et des règles de réduction suivantes:
S X Y Z ::= X Z (Y Z)
K A B ::= A
Cette maigre base suffit à construire les booléens, les entiers, les listes, toutes les fonctions effectivement calculables… ce qui en fait déjà un langage extraordinairement expressif pour sa concision. Il permet même de définir un opérateur de point fixe Y ; quelque soit le combinateur F, Y (F) est solution de l’équation F (X) = X.
Pourtant, cette équation n’a pas toujours une solution. Ainsi, quel est le point fixe de Y ? Cette question n’a pas de réponse dans ce calcul, le terme correspondant n’étant pas réductible. On retrouve ici un argument diagonal classique, introduit originellement par Cantor, à la source de l’antinomie de Russel et des théorèmes d’incomplétude de Gödel.
De sorte que ce langage, tout minimal qu’il soit, semble déjà trop expressif, puisqu’il permet de construire des paradoxes. Cette tension sera le moment qui m’intéressera.