Théorie des fonctions récursives

I/ Monade Maybe

Dans cette partie, on va étudier cet algorithme de calcul du nombre d'or, considéré comme fonction de la valeur approchée de départ :

def tau(x):
    for k in range(80):
        x = 1/x
        x += 1
    return x

En effet, à chaque répétition des opérations

• inverser la variable x
• incrémenter la variable x

le contenu de la variable x se rapproche du nombre d'or, comme on le constate sur les représentations graphiques après 1 à 6 itérations :

La fonction tau(x) semble être constante, égale à τ (le nombre d'or). En fait ce n'est pas le cas : si on essaye de calculer tau(0) on obtient, au lieu de τ, le message ZeroDivisionError: division by zero. Cela amène à modéliser les calculs n'aboutissant pas et les flottants non définis.

1) None n'a pas de type

L'objet indéfini est noté ⊥ en général mais il lui correspond None en Python. Mais None n'est ni un booléen, ni un entier, ni un flottant etc.

Pour créer un booléen indéfini ou un entier indéfini, on le place dans une monade qui s'appelle Maybe. Par exemple, voici le flottant 2,5 (qui est défini) et, à côté de lui, le flottant indéfini (boîte vide) :

2) En Haskell

Maybe, comme toutes les monades, est une fonction. Il y a plusieurs façons de l'implémenter. Dans le prélude d'Haskell, il y a

data Maybe x = Nothing | Just x

qu'on peut dessiner ainsi (x est un flottant) :

Noter qu'en français, Just est un prénom :

En utilisant l'approche de cet article, on définit

inverser :: Float -> Maybe Float
inverser x
         | x == 0 = Nothing
         | otherwise = Just (1/x)

augmenter:: Float -> Maybe Float
augmenter x = Just (x + 1)

Alors

(Just 2.5) >>= inverser >>= augmenter

s'évalue à Just 1.4 (car l'inverse de Just 2.5 est Just 0.4 qui, une fois augmenté, donne Just 1.4), et les deux expressions

(Just 0.0) >>= inverser >>= augmenter
Nothing >>= inverser >>= augmenter

s'évaluent toutes deux à Nothing : la fonction tau n'est définie ni en 0, ni en ⊥ et c'est précisément ce qu'on veut modéliser.

3) En Python

Dans la version Python, Maybe n'est pas une fonction mais une classe :

from oslash import *

def inverser(x):
    if x!=0:
        return Just(1/x)
    else:
        return Nothing()

def augmenter(x):
    return Just(x+1)

x = Just(2.5)

x | inverser | augmenter

Le caractère pipe ("|") représente un tuyau (à imaginer tourné de 90°) comme en bash, il permet de brancher les fonctions entre elles. Ainsi les deux lignes suivantes sont équivalentes :

x | inverser | augmenter

x.bind(inverser).bind(augmenter)

En fait il y a deux objets en lice : Just et Nothing :

class Just(Maybe):
    def __init__(self, val):
        self.val = val

    def bind(self, func):
        return func(self.val)

    ...

class Nothing(Maybe):
    def bind(self, func):
        return Nothing()

    ...

Les classes Just et Nothing dérivent d'une classe unique Maybe. Le diagramme UML correspondant a un air de déjà vu :

Les flèches représentent la relation dérive de la classe.

II/ Objets partiels

L'idée, remontant à Dana Scott au début des années 1970, est de rajouter à chaque type une valeur particulière ⊥ qui signifie indéfini et de définir une relation d'ordre est moins défini que, notée ⊑. En Python on utilisera None pour désigner l'objet indéfini.

1) Booléens partiellement définis

En ajoutant à True et False le booléen None (considéré ici comme un booléen), on peut effectuer des calculs en logique trivalente, et plus particulièrement celle de Łukasiewicz.

On a

• None⊑False
• None⊑True
• False⊑False, None⊑None et True⊑True
• mais ni False⊑True, ni True⊑False

Ce qui se représente par ce graphe orienté :

On convient de ne pas représenter les flèches allant d'un sommet à lui-même (puisque de toute manière x⊑x) et la forme simplifiée du graphe orienté est

En notant a⊓b la borne inférieure de a et b (c'est-à-dire m⊑a et m⊑b et pour tout c tel que c⊑a et c⊑b on a c⊑m) alors False⊓True=None. De façon similaire on peut définir une borne supérieure a⊔b mais elle ne sert pas dans cette partie.

a) Négation ternaire

Une fonction partielle f est dite croissante si, dès que x⊑y, on a f(x)⊑f(y). Dana Scott utilise aussi le mot continue pour désigner ces fonctions qui revêtent une importance fondamentale dans la théorie de la récursivité. Un exemple est la négation de Łukasiewicz :

b) Conjonction ternaire

Łukasiewicz définit and ainsi :

c) Disjonction ternaire

Note : Kleene a, indépendamment de Łukasiewicz, défini les mêmes opérations mais avec une autre signification : au lieu de indéfini, ⊥ veut dire chez Kleene indéterminé. On reparlera de Kleene plus bas à propos de la définition des fonctions récursives.

2) Entiers partiellement définis

De même, None peut être considéré comme l'entier indéfini. On a None⊑0, None⊑1, None⊑2 etc mais pas 0⊑1 etc :

3) Flottants partiellement définis

De même, on peut considérer un flottant indéfini. Ceci dit, au lieu de None, ⊥ peut aussi être modélisé par un objet qui est reconnu de type float, il s'agit de float('nan').

4) Listes partiellement définies

Si L et M sont deux listes (de booléens, d'entiers, de flottants etc) alors, si pour tout indice k on a L[k]⊑M[k] on écrit L⊑M et on dit que la liste L est moins définie que la liste M. Voici un exemple de listes de booléens que Scott classe dans l'ordre croissant selon la relation ⊑ :

• [None,None,None,None]
• [True,None,None,None]
• [True,False,None,None]
• [True,False,True,None]

Une suite xn est dite croissante si pour tout n on a xn⊑xn+1. Scott démontre qu'une telle suite n'a qu'une borne supérieure, dite limite de la suite et notée x∞ ou ⊔(xn).

L'espace S des limites de suites croissantes est un ensemble inductif. C'est un objet mathématique très abstrait. Par exemple les tuples d'éléments dans S sont eux-mêmes des éléments de S.

En identifiant la liste [1,2,3] avec la liste [1,2,3,None], Scott définit une inclusion entre les listes de longueur n et les listes de longueur n+1. Comme l'inclusion est aussi une relation d'ordre, le passage à la limite permet à Scott de définir des fonctions sur les listes de longueur infinie. Il est d'ailleurs possible d'effectuer des calculs sur de telles listes en Haskell. Par exemple pour définir le ppcm de deux entiers a et b on peut construire la liste des multiples communs puis ne demander que le plus petit d'entre eux :

cm a b = [m | m <- [1..], m `mod` a == 0, m `mod` b == 0]
ppcm a b = head (cm a b)

III/ Fonctions partielles

1) Ordre

On dit que f est moins définie que g, et on note f⊑g, si pour tout x, f(x)⊑g(x). Par exemple, la fonction tau est moins définie que la constante τ car elle n'est définie que pour x non nul (alors que la constante τ est définie partout) et que pour tout x non nul, tau(x)==τ.

Si on arrive à définir des fonctions de mieux en mieux définies, c'est-à-dire des fonctions fn telles que pour tout n on a fn⊑fn+1, alors la suite fn est croissante et, d'après la théorie de Scott, elle a une limite f∞. C'est cela qui permet à Scott de modéliser la récursivité.

2) Sémantique du λ-calcul

On part d'un espace E et on considère dans un premier temps l'espace des fonctions de E dans E, qu'on note E→E ; on note

• S0 = E
• S1 = E→E ( fonctions de E dans E)
• S2 = S1→S1
• etc

Dans un second temps on considère donc les fonctionnelles (fonctions sur S1, qui, à une fonction sur E, associent une fonction sur E). Puis plus généralement l'espace des fonction(nelle)s sur Sn (soit Sn→Sn) est défini, et noté Sn+1.

Alors comme on peut identifier un élément de E (par exemple τ) à une fonction sur E (par exemple la fonction constante égale à τ), et plus généralement un élément de Sn à un cas particulier d'élement de Sn+1, on retrouve une suite croissante parce que pour tout n, Sn⊂Sn+1. La théorie de Scott prévoit donc l'existence d'un espace fonctionnel limite noté S∞ dans lequel se trouvent des éléments de E, des fonctions sur E, des fonctionnelles etc. On dit que dans S∞ les fonctions sont de première classe. Cela a permis à Scott de donner une sémantique au λ-calcul de Church et Kleene (années 1930) ce qui, dans les années 1970, était inédit.

Si on note S l'espace S∞ de Scott, alors

• Les tuples d'éléments de S sont les éléments de S.
• Les fonctions de S dans E (S→E) sont les éléments de S.
• Même les fonctions de S dans S (S→S) sont les éléments de S.

Ce dernier résultat est aussi surprenant que si Scott avait annoncé qu'une suite d'entiers et un entier reviennent à la même chose. Il signifie surtout que le degré d'abstraction requis pour comprendre S (et la récursivité) est bien plus élevé qu'on eût pu le soupçonner (infini ?).

3) Fonctionnelles

L'exemple du début peut être interprété également comme suit :

def T(f):
    def t(x):
        y = f(x)
        y = 1/y
        y += 1
        return y
    return t

On part d'une fonction quelconque (par exemple l'identité lambda x: x) puis on lui applique répétitivement la fonctionnelle T qui, à une fonction x↦f(x) associe la fonction x↦1/f(x)+1. Les fonctions obtenues aux différentes étapes sont représentées graphiquement au début de cet article. Au fur et à mesure des répétitions, les fonctions se rapprochent de plus en plus de la fonction constante x↦τ qui est un point fixe de la fonctionnelle T, c'est-à-dire que T transforme cette fonction constante en elle-même.

Une définition récursive d'une fonction f est une équation du type f = F(f,g) où F est une fonctionnelle. Le cas le plus classique est celui où f = F(f).

4) Théorème du point fixe de Kleene

On considère une équation du type f=F(f) où F est une fonctionnelle. On note ⊥ la fonction qui n'est définie nulle part. On construit la suite de fonctions suivantes :

• f0=⊥
• f1=F(f0)
• f2=F(f1)
• f3=F(f2)
• ...
• fn+1=F(fn)
• ...

Alors les fonctions fn sont de plus en plus définies : fn⊑fn+1 pour tout n. La théorie de Scott s'y applique donc, et permet de conclure que cette suite de fonctions admet une limite notée f∞ ou ⊔fn. Cette limite vérifie les deux propriétés suivantes :

• C'est un point fixe de la fonctionnelle F (autrement dit, F(f∞)=f∞).
• Tout autre point fixe de F est au moins aussi défini que f∞ (si F(g)=g alors f∞⊑g).

Ce qui fournit la preuve du théorème de Kleene :

Toute fonctionnelle F de l'espace S∞ de Scott possède un point fixe. Le plus petit point fixe de F est la limite des itérées de F.