Théorème d'itération

La fonction d'itération est un des points fondamentaux de l'évaluation partielle. En effet, dans ${\displaystyle \varphi _{s(\mathbf {e} ,x)}(y)=\varphi _{\mathbf {e} }(x,y)}$, le programme ${\displaystyle s(\mathbf {e} ,x)}$ peut être vu comme la spécialisation du programme ${\displaystyle \mathbf {e} }$ pour l'entrée ${\displaystyle x~}$, en d'autres termes, le programme ${\displaystyle \mathbf {e} }$ dont la première entrée a été fixée pour la valeur ${\displaystyle x~}$. Pour cette notion, on pourra se référer aux travaux de N. Jones.

Par ${\displaystyle s(x,x)~}$, ce théorème permet de construire des programmes faisant référence à leurs propres codes puisque ${\displaystyle \varphi _{s(x,x)}(y)=\varphi _{x}(x,y)}$. En particulier, ${\displaystyle s(x,x)~}$ est fondamental dans la construction d'une machine de Turing dont l'arrêt est indécidable ou dans la preuve du théorème de récursion de Kleene.

Le programme Python suivant implémente la fonction s₁₁ pour une fonction quelconque f et une variable x :

def S11(f,x):
    return lambda y: f(x,y)

Appliqué à la fonction d'addition entre deux nombres :

def addition(x,y):
    return x+y
def g(x):
    return S11(addition,x)
print(g(4)(3)) # affiche le résultat de addition(4,3) = 4+3 = 7

Dans l'exemple précédent, g s'écrit autrement ${\displaystyle g:x\mapsto (y\mapsto x+y)}$.