Ce document est le résumé en français de l’article Lopez (2023) présenté à la conférence FoSSaCS 2023, dont le pdf, les slides de présentations, ainsi que le fichier bibtex associé sont disponibles sur ma page web.

Résumé

Les espaces Nœthériens sont une famille d’espaces topologiques qui généralisent la notion de beau préordre, et qui peuvent être utilisés afin de démontrer la terminaison de programmes. En particulier, les espaces Nœthériens ont été utilisés pour vérifier des systèmes de transitions dont la description topologique est plus adaptée qu’une présentation en terme d’ordres partiels. L’objectif de l’article est de décrire une topologie Nœthérienne sur des espaces définis par induction. Cet objectif est atteint au moyen d’un théorème plus général de points fixe, lui-même basé sur un argument de mauvaise séquence minimale topologique.

Contextualisation

Beaux préordres, terminaison, et systèmes de transitions

Soit \((Q, \leq)\) un ensemble muni d’un préordre, c’est-à-dire d’une relation transitive et symétrique. Une séquence \((x_n)_{n \in \mathbb{N}}\) est bonne lorsqu’il existe une paire \(i < j\) d’indices, tels que \(x_i \leq x_j\). Au contraire, une séquence est dite mauvaise lorsqu’elle n’est pas bonne.

Exemple: la séquence \((n)_{n \in \mathbb{N}}\) est bonne dans \((\mathbb{Z},\leq)\).

Exemple: la séquence \((-n)_{n \in \mathbb{N}}\) est mauvaise dans \((\mathbb{Z}, \leq)\).

Un beau préordre est un ensemble \((Q, \leq)\) tel que toute séquence \((x_n)_{n \in \mathbb{N}}\) d’éléments dans \(Q\) est bonne. On peut par exemple déduire des exemples précédents que \((\mathbb{Z}, \leq)\) n’est pas un beau préordre, et prouver séparément que \((\mathbb{N}, \leq)\) est un beau préordre.

Une notion similaire, qui apparaît fréquemment en informatique est la notion d’ordre bien fondé, dont la définition est la suivante : un préordre \((Q, \leq)\) est bien fondé lorsque toute séquence (strictement) décroissante stationne. C’est-à-dire, pour toute séquence \((x_n)_{n \in \mathbb{N}}\) d’éléments de \(Q\), telle que \(x_n \leq x_m\) lorsque \(m \leq n\), il existe un \(n_0 \in \mathbb{N}\) à partir duquel \(x_n = x_{n_0}\) pour tout \(n \geq n_0\). Une autre formulation est qu’il n’existe pas de séquences infinies décroissantes.¹¹

La différence entre les beaux préordres et les ordres bien fondés peut se comprendre en regardant les implications suivantes pour un ensemble préordonné fixé \((Q, \leq)\) :²²

\[\begin{align*} & Q \text{ bien fondé } \land Q \text{ totalement ordonné } \\ \implies & Q \text{ beau préordre } \\ \implies & Q \text{ bien fondé } \quad . \end{align*}\]

Cette généralisation des ordres bien fondés peut servir à prouver la terminaison de certains programmes. Par exemple, prenons l’algorithme récursif suivant :

def program(a : int, b : int, c : int):
  if a < 0 or b < 0 or c < 0:
    return
  c = random.choice(["r", "l"])
  if c == "r":
    a,b,c = a - 1, b, 2*c
  elif c == "l":
    a,b,c = 2*c, b-1, 1
  program(a,b,c)

On peut montrer que ce programme termine sur toute instance en utilisant le fait que \((\mathbb{N}^3, \leq)\) est un beau préordre où les inégalités se calculent point à point. En effet, imaginons une exécution infinie du programme et regardons l’évolution des valeurs du triplet \((a_n,b_n,c_n)_{n \in \mathbb{N}}\), en fonction du nombre d’appels récursif. Cette séquence est mauvaise dans \((\mathbb{N}^3, \leq)\), car si \(n < m\), soit la branche \(r\) a été prise au moins une fois, auquel cas \(b_n > b_m\), ou bien seulement la branche \(r\) a été prise, auquel cas \(a_n > a_m\). Comme \((\mathbb{N}^3, \leq)\) est un beau préordre, il n’y a pas de mauvaise séquence infinie. Ainsi, ce programme termine bien sur toute entrée.

Notons qu’un argument utilisant un ordre bien fondé est aussi possible, mais nécessite de faire un choix en donnant une importance plus grande à certaines composantes. L’utilisation de beaux préordres a été rendue très simple par le fait que ceux-ci peuvent se construire aisément par composition pour étudier des configurations plus complexes. Dans ce cas précis, démontrer que \((\mathbb{N}^3, \leq)\) est un beau préordre est une conséquence du lemme de Dickson : le produit de deux beaux préordres, avec l’ordre produit, est un beau préordre.

Il est possible de systématiser l’approche utilisée pour prouver la terminaison de notre programme exemple, en étudiant les mauvaises séquences de configurations du programme, et même d’en déduire des bornes sur le temps d’exécution (Figueira et al. 2011; Schmitz 2017).

En tant qu’objet combinatoire, les beaux préordres apparaissent régulièrement (Kruskal 1972) dans des domaines variés de l’informatique, allant de la théorie des graphes avec le théorème de Robertson et Seymour (Robertson and Seymour 2004), la théorie des nombres (Higman 1952). Néanmoins, ce qui va motiver notre étude est l’application des beaux préordres aux preuves de terminaison d’algorithmes, qui ont eu un succès notable dans leur application aux “Systèmes de Transitions Bien Structurés” (WSTS) (Abdulla et al. 1996; Abdulla and Jonsson 1998; Finkel and Schnoebelen 2001; Goubault-Larrecq et al. 2016). L’article d’Abdulla et al. (1996) a reçu en 2016 le prestigieux “LICS Test-of-Time Award” avec la description suivante :

The LICS-1996 paper “General decidability theorems for infinite-state systems” authored by Abdulla, Cerans, Jonsson and Tsay showed that various verification problems are decidable for well-structured transition systems (WSTS). WSTS is a general class of infinite systems that subsumes a number of important computation models such as Petri nets and lossy channel systems. While the notion of WSTS was introduced in 1990 by Finkel with a slightly restricted format, the present paper proved the decidability of the coverability problem for the general class introduced there by describing a backward algorithm. This powerful technique has been quite influential in the field, and cited ever since as a standard reference on WSTS.

Un beau préordre pathologique, et des espaces topologiques

Un problème de taille limite l’utilisation des beaux préordres, particulièrement dans l’étude de systèmes de transitions infinis : l’ensemble \(\mathcal{P}(X)\) des parties d’un beau préordre \(X\), muni de son ordre naturel \(\leq_{\mathsf{hoare}}\) (Rado 1954).³³ Cela est problématique car cette construction est utile, par exemple pour déterminiser un système (Jančar 1999; Segoufin and Figueira 2017; Abdulla et al. 1996). Afin de rendre précis les considérations qui suivent, écrivons désormais \(\mathcal{P}_{\mathsf{ord}}\colon \mathsf{Préordres}\to \mathsf{Préordres}\) l’opération qui associe à un préordre \((X, \leq)\), le préordre \((\mathcal{P}(X), \leq_{\mathsf{hoare}})\). Le problème soulevé par Rado peut se reformuler ainsi : il existe un beau préordre \((X, \leq)\), tel que \(\mathcal{P}_{\mathsf{ord}}(X,\leq)\) n’est pas un beau préordre. Ce problème a été contourné de trois manières différentes :

1. Une première solution est de contourner subtilement le besoin d’avoir des parties infinies, et se ramener à l’étude des sous-ensembles finis (qui lui est un beau préordre). Cette technique est ad-hoc.
2. Une seconde solution est de travailler avec des beaux préordres qui ne sont pas pathologiques, c’est-à-dire, avec des pré-meilleurs-ordres (Pouzet 1972; Milner 1985).
3. Une troisième et dernière approche a été proposée par Goubault-Larrecq (2007), qui a remarqué que la notion mathématique d’espace topologique Nœthérien \((X, \tau)\) pouvait jouer le rôle d’une généralisation des beaux préordres à un cadre topologique, dans lequel la construction de l’ensemble des parties n’est pas problématique.

Dans cet article, on s’intéresse à l’approche topologique proposée par les espaces Nœthériens. Dans ce cadre, les analogues topologiques des WSTS possèdent des propriétés similaires en terme de décidabilité, et on peut même construire un équivalent de méthodes avancées comme l’analyse en avant de Karp et Miller sur des réseaux de Pétri (Goubault-Larrecq 2010). Par ailleurs, la nature topologique de ces espaces permet de capturer des arguments de terminaison provenant aussi bien de la théorie des beaux préordres, que d’arguments algébriques sur des idéaux de polynômes, ce qui a permis, par exemple, la vérification de “programmes polynomiaux concurrents sur canaux avec perte” par Goubault-Larrecq (2010). Les polynômes sont intégrés dans le cadre des espaces Nœthériens au travers de résultats de géométrie algébrique et la notion de clôture de Zariski (voir l’Exercice 9.7.53 de Goubault-Larrecq 2013).

En résumé, il y a deux solutions concurrentes pour résoudre de manière systématique le problème posé par l’ensemble de Rado. Le premier est de restreindre l’ensemble des beaux préordres d’intérêts à une classe laissée stable par \(\mathcal{P}_{\mathsf{ord}}\) (les pré-meilleurs-ordres). Une seconde est de généraliser les ensembles considérés, de manière à conserver les propriétés de décidabilité désirées, tout en incluant l’ensemble de Rado et son ensemble des parties (les espaces Nœthériens). Il faut comprendre que, dans cette seconde approche, on ne peut se contenter de restreindre l’opération \(\mathcal{P}_{\mathsf{ord}}\), il faut inventer une nouvelle opération, \(\mathcal{P}_{\mathsf{top}}\), qui opère sur des espaces topologiques, et coïncide avec \(\mathcal{P}_{\mathsf{ord}}\) sur les préordres. Ainsi, \(\mathcal{P}_{\mathsf{top}}\colon \mathsf{E.Topologiques}\to \mathsf{E.Topologiques}\) appliqué à l’ensemble de Rado produit un espace topologique Nœthérien, qui ne correspond pas à un beau préordre.

Les limites de l’approche Nœthérienne

À chaque topologie \(\tau\) sur un espace \(Q\), on peut associer son préordre de spécialisation \(\leq_\tau\) sur \(Q\). Les topologies Nœthériennes généralisent les beaux préordres dans le sens où, pour chaque beau préordre, il existe une topologie Nœthérienne dont il est le préordre de spécialisation.⁴⁴⁵⁵ Au contraire, plusieurs topologies peuvent avoir le même préordre de spécialisation.

Tout l’intérêt des espaces Nœthériens réside dans le fait qu’il existe des topologies Nœthériennes dont le préordre de spécialisation n’est pas un beau préordre. Cependant, cette liberté pose la question de la validité de la généralisation, dans un sens que nous allons décrire maintenant. Le lemme de Dickson prouve que si \((X, \leq_X)\) et \((Y, \leq_Y)\) sont des beaux préordres, alors leur produit \(X \times Y\), muni de l’ordre produit \((x_1, y_1) \leq (x_2, y_2)\) si et seulement si \(x_1 \leq x_2\) et \(y_1 \leq y_2\) est un beau préordre. Un analogue topologique de ce lemme est le fait que, pour deux espaces Nœthériens \((X, \tau_X)\) et \((Y,\tau_Y)\), le produit \(X \times Y\) est Nœthérien … pour une certaine topologie. Pour prétendre que le lemme topologique est une généralisation du lemme de Dickson, on peut proposer les conditions suivantes

1. Si \(\tau_X\) a pour préordre de spécialisation \(\leq_X\) et \(\tau_Y\) a pour préordre de spécialisation \(\leq_Y\), alors la topologie choisie pour le produit devrait avoir pour préordre de spécialisation l’ordre produit \(\leq_{X \times Y}\).
2. Si \(\tau_X\) est la topologie la plus fine associée à \(\leq_X\), \(\tau_Y\) est la topologie la plus fine associée à \(\leq_Y\), et que \(\leq_X\) et \(\leq_Y\) sont des beaux préordres, alors \(\tau_{X \times Y}\) est la topologie la plus fine associée à \(\leq_{X \times Y}\), qui est un beau préordre.

Dans le cas du produit, il existe une topologie naturelle (au sens catégorique) pour cet espace, la topologie produit. Cette topologie vérifie les points 1 et 2 précédents. Mais on peut imaginer d’autres topologies, beaucoup plus étranges, qui satisfont 1 et 2. En particulier, sur des espaces topologiques qui ne proviennent pas d’espaces préordonnés, le constructeur est extrêmement libre, puisqu’il existe de nombreuses topologies dont le préordre de spécialisation est un préordre donné.⁶⁶

Cette question de canonicité de la topologie associée à un constructeur peut sembler anecdotique, mais elle se retrouve de manière non triviale dans la généralisation de théorèmes plus poussés sur les beaux préordres, comme le fait que \(X^*\) est un beau préordre lorsqu’il est muni de la relation d’inclusion de sous mots de Higman, et que \(X\) était déjà lui-même un beau préordre (Higman 1952). Le lemme de Higman topologique, proposé par Goubault-Larrecq (2013), propose une définition ad-hoc de la topologie sous-mot, vérifiant les points 1 et 2. De même, la généralisation du théorème de Kruskal, qui traite d’un beau préordre sur les arbres (Kruskal 1972) au cadre topologique d passe par la construction d’une topologie bien choisie (Goubault-Larrecq 2013). Dans les deux cas, le cadre topologique proposé est une généralisation possible du cas des préordres.

Dans le cas des préordres, les preuves du lemme de Higman et du théorème de Kruskal reposent généralement sur un argument de mauvaise séquence minimale introduit par Nash-Williams (1965). Les preuves utilisant cette technique sont assez subtiles, et peuvent facilement s’avérer erronnées (voir par exemple l’erratum de Gallier 1997; et une preuve correcte par Singh, Shuaibu, and Ndayawo 2013). De plus, ces arguments ne sont pas compositionnels, pour chaque constructeur (mots, arbres, etc.) il faut construire un nouvel argument de mauvaise séquence minimale adapté (voir par exemple Dershowitz and Tzameret 2003; et Daligault, Rao, and Thomassé 2010).

Les analogues topologiques du lemme de Higman et du théorème de Kruskal obtenus pour les espaces Nœthériens reposent aussi sur des arguments de mauvaise séquence minimale, mais dans une version topologique (Goubault-Larrecq 2013, vol. 22, sec. 9.7). Il faut noter cependant que les définitions comme les preuves ont une complexité accrue par rapport à leurs homologues préordonnés, et que l’argument de mauvaise séquence topologique minimale est encore plus subtil (voir l’errata n. 26 de l’article de blog Goubault-Larrecq 2022b).

Constructions inductives

Il est possible d’argumenter que, déjà dans le cas des beaux préordres, le choix de l’ordre sur les mots finis ou les arbres a une grande importance, et qu’il comporte une part d’arbitraire. Cependant, les travaux de Hasegawa (2002) ont démontré que, dans un cadre assez générique, on peut définir de manière naturelle un beau préordre sur des constructions inductives. Pour fixer une notation, on considère un foncteur \(F \colon \mathsf{Préordres}\to \mathsf{Préordres}\), qui préserve les beaux préordres, et l’objectif est de définir un beau préordre sur le plus petit point fixe de \(F\) (qui existera grâce à des conditions supplémentaires posées sur \(F\)). Le cadre catégorique proposé par Hasegawa permet de retrouver les théorèmes de Kruskal et le lemme de Higman à partir de la définition inductive des mots et des arbres. On peut noter que, suivant des motivations différentes, le récent travail de Freund (2020) sur le théorème de Kruskal donne un autre cadre catégorique permettant de définir des beaux préordres sur des constructions inductives, qui coïncide bien avec les notions usuelles dans le cas des mots finis et des arbres finis. Ces deux résultats semblent relativement peu connus et utilisés par la communauté, ce qui peut s’expliquer par leur cadre théorique reposant sur des constructions non triviales en théories des catégories, et donc relativement hermétique.

Dans le cas des espaces Nœthériens, il n’existe pas de construction générique permettant de définir une topologie sur des espaces \(X\) construits comme des points fixes. De plus, les conditions placées dans les deux cadres catégoriques susmentionnés implique que les constructeurs \(F\) considérés doivent avoir un support fini, ce qui exclut d’office une grande famille de constructeurs pour les espaces Nœthériens. Le fait d’avoir un support fini revient à dire que, pour tout élément \(a \in F(X)\), il existe un sous ensemble fini \(Y \subseteq_{\mathsf{fin}}X\) tel que \(a\) est construit à partir des éléments de \(Y\). C’est bien le cas des mots et des arbres, mais cela exclut \(\mathcal{P}_{\mathsf{ord}}\) par exemple. De plus, de récents travaux sur les espaces Nœthériens ont démontré la possibilité (et l’intérêt) de placer des topologies Nœthériennes sur des espaces qui ne sont pas immédiatement obtenus comme des plus petits points fixes, comme les mots infinis (Goubault-Larrecq 2022a), ou les mots de longueur ordinale (Goubault-Larrecq, Halfon, and Lopez 2022).

Contributions de l’article

Cet article apporte deux contributions principales. La première est l’introduction d’un théorème de plus petit point fixe pour les topologies Nœthériennes, basé sur un argument de mauvaise séquence minimale topologique. La seconde est l’utilisation de ce théorème pour déduire une topologie Nœthérienne sur des espaces définis inductivement.

Notons que la première contribution dévie significativement des analogues proposés dans le cadre des préordres. En effet, au lieu de considérer une suite d’espaces topologiques définie par l’équation \(X_{n+1} = F(X_n)\), où le constructeur \(F\) fait varier simultanément l’ensemble des points de l’espace et sa topologie, on considère un ensemble \(X\) fixé de points et une fonction \(F\) qui raffine une topologie sur \(X\). Dans ce cadre la construction de l’espace \(X\) est découplée de la construction de la topologie sur \(X\). En particulier, l’espace \(X\) lui-même n’a pas besoin d’être défini par induction. Le théorème isole une condition suffisante très simple qui garantit que le plus petit point fixe est Nœthérien. En particulier, cela permet d’encapsuler toute la complexité des preuves par mauvaise séquence topologique minimale dans un théorème aux hypothèses simples (hors de tout cadre catégorique en particulier).

Dans le cas plus spécifique où l’espace \(X\) est lui-même défini par une équation de plus petit point fixe, une définition inductive d’une topologie sur \(X\) permet d’utiliser le théorème précédent et d’équiper \(X\) d’une topologie Nœthérienne, directement dérivée de sa construction inductive. Cela généralise la construction de Hasegawa (2002) au cadre topologique, au sens où, dans le cas des préordres, on retrouve exactement ce que donne le cadre proposé par Hasegawa (2002).

Tout au long de l’article, de nombreux exemples de constructions (mots finis, arbres finis, mots infinis, mots transfinis, arbres avec branchement ordinal, etc.) sont proposés afin d’illustrer comment le théorème de point fixe permet de généraliser les résultats déjà connus avec des preuves plus simples, en proposer de nouveaux, mais aussi montrer que cette approche uniforme donne une légitimité nouvelle aux généralisations topologiques des constructions sur les ordres : les topologies proposées, faute d’être les plus topologies Nœthériennes les plus fines sur un espace donné,⁷⁷ sont obtenues par un procédé uniforme.

Conclusion

Cet article propose une condition sémantique simple permettant de garantir qu’une topologie obtenue comme un plus petit point fixe est Nœthérienne. L’idée principale est de fixer l’espace et ne faire varier que la topologie, ce qui simplifie grandement les équations et évite l’introduction d’un cadre catégorique. Par la suite, il est possible d’utiliser ce théorème de point fixe sur les topologies pour en déduire un théorème de point fixes sur les espaces topologiques dans le cade catégorique idoine.

Le théorème de point fixe sur les topologies semble être la bonne abstraction des arguments de mauvaise séquence minimale topologique. Tout comme ces derniers, il ne fournit aucun contrôle sur les invariants ordinaux des topologies Nœthériennes ainsi construites. En ce sens, il manque encore à la théorie une manière de contrôler quantitativement les espaces Nœthériens définis par induction.

Références