Que pouvons-nous prouver avec des graphes infinis que nous ne pouvons pas prouver sans eux?

Il s'agit d'une question complémentaire à celle-ci concernant les graphiques infinis.

Les réponses et commentaires à cette question énumèrent des objets et des situations qui sont naturellement modélisés par des graphiques infinis. Mais il existe également de nombreux théorèmes sur les graphes infinis (voir chapitre 8 du livre de Diestel) dont, par exemple, le lemme de Koenig à l'infini est très célèbre.

Maintenant, j'ai la question suivante: que pouvons-nous prouver avec des graphes infinis que nous ne pouvons pas prouver sans eux? Ou plus précisément, quel est un exemple où nous modélisons quelque chose comme un graphe infini, puis invoquons un théorème sur les graphes infinis, et à la fin avons prouvé quelque chose sur le problème d'origine - sans savoir comment le prouver autrement?

Voici un exemple de l'informatique distribuée:

1. Origines

1.1 Modèle de mémoire partagée asynchrone

Prenons un ensemble de nœuds distribués qui communiquent à l'aide de variables de mémoire partagée. Il y a un adversaire qui contrôle quand un nœud prend des mesures et quand remettre des messages. Le calcul est asynchrone , c'est-à-dire que l'adversaire peut retarder les pas des nœuds pendant n'importe quelle durée (finie).
Vous pouvez considérer une étape d'un nœud comme une transition d'état de son automate local (selon l'algorithme) où l'état suivant est déterminé par l'état actuel et les observations du nœud depuis la dernière étape.

1.2 Sécurité et vitalité

Lorsque nous raisonnons formellement sur les propriétés d'un algorithme asynchrone, nous distinguons les propriétés de sécurité et de vivacité. De manière informelle, une propriété de sécurité peut être interprétée comme une garantie que quelque chose de «mauvais» ne se produit jamais. (Par exemple, pour l'exclusion mutuelle, une propriété de sécurité serait que deux nœuds ne pénètrent pas simultanément dans la section critique.) La vitalité , d'autre part, peut être interprétée comme "quelque chose de bien finira par arriver", par exemple: chaque nœud se termine finalement.

Pour formaliser la sécurité, nous considérons l'ensemble infini de toutes les exécutions possibles de tous les algorithmes possibles, en tenant compte de tous les choix possibles de l'adversaire. Une exécution est une séquence infinie d'étapes. Nous pouvons définir une métrique sur M en prenant la distance entre deux parcours distincts α , β ∈ M comme étant 2 - n où n est le premier indice où α et β diffèrent.${M}$$M$$\alpha,\beta \in M$$2^{-n}$$n$$\alpha$$\beta$

Une propriété de sécurité correspond à un ensemble non vide P ⊆ M qui est fermé en ce sens que la limite d'une suite infinie de points en P ne peut pas être en M ∖ P . Donc, une fois que nous savons qu'une propriété est une propriété de sécurité, il suffit de montrer que cette propriété tient sur des préfixes finis .$S$$P\subseteq M$$P$$M\setminus P$

Application du lemme infini de Koenig

Il n'est pas toujours simple de voir si une propriété spécifique est une propriété de sécurité: pensez à l'implémentation d'objets atomiques en lecture / écriture au-dessus des variables de mémoire partagée de base. Une telle implémentation doit gérer les demandes et leurs réponses de manière à ce qu'elles semblent se produire à un instant donné et ne violent pas leur ordre d'invocation. (En raison de l'opération asynchrone, la durée réelle entre la demande et la réponse peut être différente de zéro.) L'atomicité est également connue sous le nom de linéarisation . L'article 13.1 de [A] donne la preuve que l'atomicité est une propriété de sécurité. La preuve utilise le lemme de Koenig pour montrer que la limite de toute séquence infinie d'exécutions (dont chacune satisfait l'atomicité) satisfait également l'atomicité.

[A] N. Lynch. Algorithmes distribués. Morgan Kaufmann, 1996.