F -kolgebra

Inom matematiken , specifikt inom kategoriteorin , är en $F$ -koalgebra en struktur definierad enligt en funktion $F$ , med specifika egenskaper som definieras nedan. För både algebror och coalgebras ^{[ förtydligande behövs är} ] en funktor ett bekvämt och allmänt sätt att organisera en signatur . Detta har tillämpningar inom datavetenskap : exempel på coalgebras inkluderar lata , oändliga datastrukturer , såsom strömmar , och även övergångssystem .

$F$ -koalgebror är dubbla till $F$ -algebror . Precis som klassen för alla algebror för en given signatur och ekvationsteori bildar en varietet , så bildar klassen för alla $F$ -koalgebror som uppfyller en given ekvationsteori en samvarietet, där signaturen ges av ${\ displaystil F}$ .

Definition

Låta

F:{\mathcal {C}}\longrightarrow {\mathcal {C}}

vara en endofunctor på en kategori ${\mathcal {C}}$ . En $F$ -koalgebra är ett objekt $A$ av ${\mathcal {C}}$ tillsammans med en morfism

\alpha :A\longrightarrow FA

av ${\mathcal {C}}$ , vanligtvis skrivet som $(A,\alpha )$ .

En $F$ -coalgebra homomorfism från $(A,\alpha )$ till en annan $F$ -coalgebra $(B,\beta )$ är en morfism

f:A\longrightarrow B

i ${\mathcal {C}}$ så att

Ff\circ \alpha =\beta \circ f

.

Således utgör $F$ -koalgebran för en given funktion F en kategori.

Exempel

Betrakta endofunktorn $X\mapsto X\sqcup \{*\}:\mathbf {Set} \to \mathbf {Set}$ som skickar en uppsättning till dess disjunkta förening med singeluppsättningen $\{\ast \}$ . En koalgebra för denna endofunctor ges av $({\overline {\mathbb {N} }},\alpha )$ , där ${\displaystyle {\overline {\mathbb {N} }}=\{0,1,2,\ldots \}\sqcup \{\infty \}} är de så kallade$ konaturliga talen, som består av de icke-negativa heltalen och även oändlighet, och funktionen $\alpha$ ges av ${\displaystyle \alpha (0)=\ast } ,$ α $\displaystyle \alpha (n )=n-1}$ för $n=1,2,\ldots$ och $\alpha (\infty )=\infty$ . Faktum är att $({\overline {\mathbb {N} }},\alpha )$ är den terminala koalgebra för denna endofunctor.

Mer allmänt, fixa någon uppsättning $A$ , och överväga funktorn $F:\mathbf {Set} \longrightarrow \mathbf {Set}$ som skickar $X$ till $(X\times A)\cup \{1\}$ . Då en $F$ -coalgebra $\alpha :X\longrightarrow (X\times A)\cup \{1\}=FX$ är en ändlig eller oändlig ström över alfabetet $A$ , där $X$ är uppsättningen av tillstånd och $\alpha$ är tillståndsövergångsfunktionen. Att tillämpa tillståndsövergångsfunktionen på ett tillstånd kan ge två möjliga resultat: antingen ett element av $A$ tillsammans med nästa tillstånd i strömmen, eller elementet i singleton-uppsättningen { $\displaystyle \{1 \}}$ som ett separat "slutläge" som indikerar att det inte finns fler värden i flödet.

I många praktiska tillämpningar kan tillståndsövergångsfunktionen för ett sådant koalgebraiskt objekt ha formen $X\rightarrow f_{1}\times f_{2}\times \ldots \times f_{n}$ , som enkelt faktoriseras till en samling av "selektorer", "observatörer", "metoder" $X\rightarrow f_{ 1},\,X\högerpil f_{2}\,\ldots \,X\högerpil f_{n}$ . Särskilda fall av praktiskt intresse inkluderar observatörer som ger attributvärden och mutatormetoder av formen $X\rightarrow X^{A_{1}\times \ldots \times A_{n} }$ tar ytterligare parametrar och ger tillstånd. Denna nedbrytning är dubbel till nedbrytningen av initiala $F$ -algebror till summor av 'konstruktorer'.

Låt P vara effektmängdskonstruktionen för kategorin mängder, betraktad som en kovariansfunktion. P -koalgebran är i bijektiv överensstämmelse med mängder med en binär relation . Fixa nu en annan uppsättning, A . Sedan är koalgebras för endofunktorn P ( A ×(-)) i bijektiv överensstämmelse med märkta övergångssystem , och homomorfismer mellan koalgebran motsvarar funktionella bisimuleringar mellan märkta övergångssystem.

Ansökningar

Inom datavetenskap har koalgebra dykt upp som ett bekvämt och lämpligt allmänt sätt att specificera beteendet hos system och datastrukturer som är potentiellt oändliga, till exempel klasser i objektorienterad programmering , strömmar och övergångssystem . Medan algebraisk specifikation handlar om funktionellt beteende, vanligtvis med induktiva datatyper som genereras av konstruktörer, handlar koalgebraisk specifikation om beteende som modelleras av koduktiva processtyper som kan observeras av väljare, mycket i automatteorins anda . En viktig roll spelas här av slutliga coalgebras , som är kompletta uppsättningar av möjligen oändliga beteenden, såsom strömmar. Den naturliga logiken för att uttrycka egenskaper hos sådana system är koalgebraisk modal logik . ^{[ citat behövs ]}

Se även

externa länkar