Technische Samenvatting: Eindige Observaties, Oneindig Gedrag

Probleemstelling

Tijdsafhankelijke systemen, zoals signaalstroomgrafieken, stochastische processen en kwantumkanalen met geheugen, worden vaak gemodelleerd als staat-afhankelijke processen (bijv. Mealy-machines) die een intern geheugen bijhouden. Hoewel het gedrag van deterministische systemen goed begrepen wordt via coinductieve vaste punten, stort deze karakterisering in wanneer processen partieel, niet-deterministisch, probabilistisch of kwantum-achtig zijn. In dergelijke settings bestaat het coinductieve vaste punt mogelijk niet, en falen standaarddefinities van gedragsequivalentie.

De centrale vraag die aan dit werk ten grondslag ligt is: Wanneer produceren twee staat-afhankelijke processen hetzelfde oneindige gedrag? De auteurs zoeken naar een denotioneel antwoord dat uitsluitend steunt op eindige, lokale observaties in plaats van a priori globale beperkingen. De uitdaging is om een semantische constructie te definiëren waarbij twee processen equivalent zijn als zij dezelfde beperkingen opleggen aan hun inputs en outputs, zoals bepaald door eindige observaties, onafhankelijk van de interne staat.

Methodologie

1. Structurele Fundering: Discard Bicategorieën

De auteurs introduceren een structureel kader genaamd een discard bicategorie. Dit is een preorder-verrijkte symmetrische monoidale categorie uitgerust met een "discard"-morfisme ($\top_X: X \to I$) voor elk object, wat de mogelijkheid vertegenwoordigt om informatie te negeren.

• Preorder-verrijking: Hom-sets zijn uitgerust met een preorder ($\subseteq$) waardoor processen vergeleken kunnen worden op basis van hun informatieve densiteit (benadering).
• Lax Natuurlijkheid van Discard: De discard-operatie is compatibel met benadering ($\top_Y \circ f \subseteq \top_X$), wat betekent dat het uitvoeren van een proces en vervolgens weggooien minder informatief is dan het direct weggooien van de input.
• Scope: Deze structuur verenigt diverse proces-theorieën, waaronder partiële functies (restrictie-orde), relaties (verzameling inclusie), probabilistische kernels (conditionele orde) en kwantumkanalen (purificatie-orde).

2. Semantische Constructie: De Categorie van Gedragingen

De kernbijdrage is de constructie van een discard bicategorie van gedragingen, aangeduid als $\text{Obs}_{I,J}(\mathcal{C})$.

• Contexten: De constructie is geparametriseerd door een indexverzameling $I$ (vertegenwoordigt tijd of ruimte) en een collectie $J$ van eindige deelverzamelingen van $I$ (contexten).
• Monotoon Families: Een gedrag wordt gedefinieerd als een "monotoon familie" van observaties. Dit is een familie van morfismen $\{f_j\}_{j \in J}$, waarbij elke $f_j$ het proces beschrijft beperkt tot een eindige context $j$.
• Consistentievoorwaarde: De familie moet consistent zijn: observaties in een grotere context $j'$ moeten die in een kleinere context $j$ verfijnen (formeel: $(1 \otimes \top) \circ f_{j'} \subseteq f_j \otimes \top$).
• Observational Equivalentie: Twee processen worden geïdentificeerd als zij observationeel equivalent zijn: elke observatie van de een kan worden geverifieerd door een observatie van de ander, mogelijk in een grotere context. Dit wordt geformaliseerd als wederzijdse benadering ($f \subseteq g$ en $g \subseteq f$).
• Quotientering: De categorie van gedragingen wordt verkregen door de categorie van monotone netten te quotienteren door deze observational equivalentie-relatie.

3. Integratie met Staat-afhankelijke Processen

De auteurs demonstreren dat deze constructie een functoriele semantiek biedt voor staat-afhankelijke processen:

• Staat Reparametrisatie: De constructie identificeert staat-afhankelijke processen die enkel verschillen door een dinatuurlijke reparametrisatie van hun interne staat.
• Tijdvertraging: De tijdvertraging-operatie wordt getoond als een natuurlijke transformatie. In compact-gesloten settings wordt dit een natuurlijke isomorfisme, waardoor de constructie een feedback-categorie vormt in de zin van Katis, Sabadini en Walters.
• Propagatie van Inconsistentie: In tegenstelling tot eerdere stream-semantics (bijv. coalgebraische streams of extensionele streams), propageert deze constructie inconsistentie globaal. Als een proces inconsistent is in een enkele eindige context, is het gehele gedrag de nul-morfisme.

Belangrijkste Resultaten

1. Uniformiteit en Functorialiteit

De constructie is uniform toepasbaar op partiële, niet-deterministische, probabilistische en kwantum-processen. Het is functorieel met betrekking tot basisverandering, wat betekent dat een morfisme tussen onderliggende proces-theorieën een morfisme induceert tussen hun respectieve categorieën van gedragingen.

2. De Categorified Compactness Theorem

Met de focus op de niet-deterministische setting (relaties), bewijzen de auteurs een categorified compactness theorem (Theorem 5.5).

• Stelling: Voor de categorie van gesloten relaties tussen compacte Hausdorff-ruimten, breidt elke compatibele familie van eindige observaties (een monotone net) zich uniek en functorieel uit naar een enkel oneindig gesloten relatie.
• Significantie: Dit vestigt dat lokale consistentie impliceert dat er globale existentie en uniciteit is in deze specifieke setting, wat effectief eindige observaties "lijmt" tot een globaal gedrag.

3. Herstel van Willems' Gedragingen

Wanneer beperkt tot affine relaties over eindige velden, herstelt het compactheidstheorema Willems' begrip van gedrag voor lineaire tijd-invariante (LTI) systemen.

• De auteurs tonen aan dat hun tijd-domein semantiek voor ongeïnitialiseerde LTI-systemen precies de gedragingen vangt die door Willems zijn gedefinieerd als de kernel van een systeem van constant-coëfficiënt verschilvergelijkingen.
• Dit biedt een compositionele tijd-domein semantiek voor signaalstroomgrafieken die voorheen ongrijpbaar was in categorische behandelingen, die grotendeels hadden geleund op frequentie-domein (z-domein) interpretaties.

4. Vergelijking met Bestaande Semantiek

Het artikel betoogt dat bestaande benaderingen (stateful morphism sequences, coalgebraic streams, causal sequences) niet alle gewenste eigenschappen tegelijkertijd kunnen vervullen:

• Stateful morphism sequences zijn puur lokaal en falen in het globaal propageren van inconsistentie.
• Coalgebraic streams storten in bij de aanwezigheid van partialiteit of nul-morfismen (worden indiscreet).
• Causale/monotone sequenties identificeren geen dinatuurlijk equivalente streams.
  De voorgestelde constructie lost deze problemen op door de nadruk te leggen op de consistentie van eindige observaties.

Significantie en Claims

Het artikel claimt een proces-theoretische oplossing te bieden voor het probleem van het definiëren van oneindig gedrag voor staat-afhankelijke systemen zonder te vertrouwen op coinductieve vaste punten die mogelijk niet bestaan. Door de focus te verschuiven van de interne staat naar eindige beperkingen, bieden de auteurs een robuust semantisch kader dat:

1. Generaliseert: Het gedrags-equivalentie over diverse proces-theorieën (deterministisch, partieel, probabilistisch, kwantum).
2. Verenigd: Het lokaliseert en globaliseert de visies op gedrag, waarbij bewezen wordt dat onder specifieke topologische condities (compact Hausdorff-ruimten) lokale observaties uniek een globaal gedrag bepalen.
3. Reconcilieert: De categorische semantiek met klassieke systeemtheorie, waarbij Willems' benadering van gedrag voor LTI-systemen over eindige velden wordt hersteld binnen een compositioneel tijd-domein framework.

De auteurs positioneren hun werk als een fundamentele stap, waarbij zij opmerken dat hoewel zij de existentie en eigenschappen van deze gedragingen hebben vastgesteld, de volledigheid van grafische talen voor deze gedragingen (axiomatisering) een openstaand probleem blijft voor toekomstig onderzoek. Zij suggereren ook dat het generaliseren van het compactheidstheorema naar probabilistische en kwantum-settings een natuurlijke volgende stap is.