Résumé technique : Observations finies, comportement infini

Énoncé du problème

Les systèmes dépendants du temps, tels que les graphes de flux de signaux, les processus stochastiques et les canaux quantiques avec mémoire, sont souvent modélisés comme des processus à état (par exemple, des machines de Mealy) qui maintiennent une mémoire interne. Bien que le comportement des systèmes déterministes soit bien compris via les points fixes coinductifs, cette caractérisation s'effondre lorsque les processus sont partiels, non déterministes, probabilistes ou quantiques. Dans ces configurations, le point fixe coinductif peut ne pas exister, et les définitions standards d'équivalence comportementale échouent.

La question centrale qui motive ce travail est la suivante : Quand deux processus à état produisent-ils le même comportement infini ? Les auteurs chercheent une réponse dénotationnelle qui repose uniquement sur des observations finies et locales plutôt que sur des contraintes globales a priori. Le défi consiste à définir une construction sémantique où deux processus sont équivalents s'ils imposent les mêmes contraintes sur leurs entrées et sorties, déterminées par des observations finies, indépendamment de leur état interne.

Méthodologie

1. Fondement structurel : Bicatégories de rejet (Discard Bicategories)

Les auteurs introduisent un cadre structurel appelé bicatégorie de rejet, qui est une catégorie symétrique monoïdale enrichie par un préordre, équipée d'un morphisme de « rejet » ($\top_X: X \to I$) pour chaque objet, représentant la capacité d'ignorer l'information.

• Enrichissement par préordre : Les ensembles de morphismes sont équipés d'un préordre ($\subseteq$) permettant de comparer les processus par leur caractère informatif (approximation).
• Naturalité lax de rejet : L'opération de rejet est compatible avec l'approximation ($\top_Y \circ f \subseteq \top_X$), ce qui signifie que l'exécution d'un processus suivie d'un rejet est moins informative que le rejet direct de l'entrée.
• Portée : Cette structure unifie diverses théories de processus, incluant les fonctions partielles (ordre de restriction), les relations (inclusion d'ensembles), les noyaux probabilistes (ordre conditionnel) et les canaux quantiques (ordre de purification).

2. Construction sémantique : La catégorie des comportements

La contribution centrale est la construction d'une bicatégorie de rejet des comportements, notée $\text{Obs}_{I,J}(\mathcal{C})$.

• Contextes : La construction est paramétrée par un ensemble d'indices $I$ (représentant le temps ou l'espace) et une collection $J$ de sous-ensembles finis de $I$ (contextes).
• Familles monotones : Un comportement est défini comme une « famille monotone » d'observations. Il s'agit d'une famille de morphismes $\{f_j\}_{j \in J}$, où chaque $f_j$ décrit le processus restreint à un contexte fini $j$.
• Condition de cohérence : La famille doit être cohérente : les observations dans un contexte plus large $j'$ doivent affiner celles d'un contexte plus petit $j$ (formellement, $(1 \otimes \top) \circ f_{j'} \subseteq f_j \otimes \top$).
• Équivalence observationnelle : Deux processus sont identifiés s'ils sont observationnellement équivalents : toute observation de l'un peut être vérifiée par une observation de l'autre, éventuellement dans un contexte plus large. Cela est formalisé par une approximation mutuelle ($f \subseteq g$ et $g \subseteq f$).
• Quotientage : La catégorie des comportements est obtenue en quotientant la catégorie des réseaux monotones par cette relation d'équivalence observationnelle.

3. Intégration avec les processus à état

Les auteurs démontrent que cette construction fournit une sémantique foncteurielle pour les processus à état :

• Reparamétrage d'état : La construction identifie les processus à état qui diffèrent uniquement par un reparamétrage dinatural de leur état interne.
• Retard temporel : L'opération de retard temporel est montrée comme étant une transformation naturelle. Dans les contextes compacts-fermés, elle devient un isomorphisme naturel, permettant à la construction de former une catégorie de rétroaction (feedback category) au sens de Katis, Sabadini et Walters.
• Propagation de l'incohérence : Contrairement aux sémantiques de flux (streams) précédentes (ex: flux coalgebraiques ou flux extensifs), cette construction propage l'incohérence de manière globale. Si un processus est incohérent dans un seul contexte fini, son comportement entier est le morphisme nul.

Résultats clés

1. Uniformité et fonctorialité

La construction s'applique uniformément aux processus partiels, non déterministes, probabilistes et quantiques. Elle est fonctorielle par rapport au changement de base, ce qui signifie qu'un morphisme entre les théories de processus sous-jacentes induit un morphisme entre leurs catégories de comportements respectives.

2. Le théorème de compacité catégorifié

En se concentrant sur le cadre non déterministe (relations), les auteurs prouvent un théorème de compacité catégorifié (Théorème 5.5).

• Énoncé : Pour la catégorie des relations fermées entre espaces de Hausdorff compacts, toute famille compatible d'observations finies (un réseau monotone) se prolonge de manière unique et fonctorielle en une relation fermée infinie unique.
• Signification : Cela établit que la cohérence locale implique l'existence et l'unicité globales dans ce cadre spécifique, « collant » efficacement les observations finies en un comportement global.

3. Récupération des comportements de Willems

Lorsqu'elle est restreinte aux relations affines sur des corps finis, le théorème de compacité récupère la notion de comportement de Willems pour les systèmes linéaires invariants dans le temps (LTI).

• Les auteurs montrent que leur sémantique temporelle pour les systèmes LTI non initialisés capture précisément les comportements définis par Willems comme le noyau d'un système d'équations aux différences à coefficients constants.
• Cela fournit une sémantique temporelle compositionnelle pour les graphes de flux de signaux, ce qui était auparavant difficile à obtenir par des traitements catégoriques qui reposaient largement sur des interprétations dans le domaine fréquentiel (domaine z).

4. Comparaison avec les sémantiques existantes

L'article soutient que les approches existantes (séquences de morphismes à état, flux coalgebraiques, séquences causales/monotones) ne parviennent pas à satisfaire toutes les propriétés désirables simultanément :

• Les séquences de morphismes à état sont purement locales et ne parviennent pas à propager l'incohérence à l'infini.
• Les flux coalgebraiques s'effondrent en présence de partialité ou de morphismes nuls (devenant indiscrets).
• Les séquences causales/monotones n'identifient pas les flux équivalents de manière dinaturale.
  La construction proposée résout ces problèmes en privilégiant la cohérence des observations finies.

Signification et affirmations

L'article prétend fournir une solution théorique des processus au problème de la définition du comportement infini pour les systèmes à état sans dépendre de points fixes coinductifs qui pourraient ne pas exister. En déplaçant l'attention de l'état interne vers les contraintes finies, les auteurs proposent un cadre sémantique robuste qui :

1. Généralise l'équivalence comportementale à travers diverses théories de processus (déterministes, partielles, probabilistes, quantiques).
2. Unifie les vues locales et globales du comportement, en prouvant que sous des conditions topologiques spécifiques (espaces de Hausdorff compacts), les observations locales déterminent de manière unique le comportement global.
3. Réconcilie la sémantique catégorique avec la théorie des systèmes classique, en récupérant notamment le approche comportementale de Willems pour les systèmes LTI sur des corps finis dans un cadre compositionnel temporel.

Les auteurs positionnent ce travail comme une étape fondamentale, notant que bien qu'ils aient établi l'existence de ces comportements et leurs propriétés, la complétude des langages graphiques pour ces comportements (axiomatisation) reste un problème ouvert pour des travaux futurs. Ils suggèrent également que la généralisation du théorème de compacité aux contextes probabilistes et quantiques constitue une étape naturelle suivante.