Initial algebra

Inom matematiken är en initial algebra ett initialobjekt i kategorin $F$ -algebror för en given endofunctor F $.$ Denna initialitet ger en allmän ram för induktion och rekursion .

Exempel

Funktion $1 + (-)$

Betrakta endofunktorn $F : Set \to Ställ in$ att skicka $X$ till $1 + X$ , där $1$ är enpunktsuppsättningen ( singleton ) , terminalobjektet i kategorin. En algebra för denna endofunctor är en mängd $X$ (kallad algebras bärare ) tillsammans med en funktion $f : (1 + X) \to X$ . Att definiera en sådan funktion motsvarar att definiera en punkt $x\in X$ och en funktion $X \to X$ . Definiera

{\begin{aligned}\operatörsnamn {noll} \colon 1&\longrightarrow \mathbf {N} \\*&\longmapsto 0\end{aligned}}

och

{\begin{aligned}\operatörsnamn {succ} \colon \mathbf {N} &\longrightarrow \mathbf {N} \\n&\longmapsto n+1.\ end{aligned}}

Då är mängden $N$ av naturliga tal tillsammans med funktionen $[noll,succ]: 1 + N \to N$ en initial $F$ -algebra. Initialiteten (den universella egenskapen för detta fall) är inte svår att fastställa; den unika homomorfismen till en godtycklig $F$ -algebra $(A, [e, f] )$ , för $e : 1 \to A$ ett element av $A$ och $f : A \to A$ en funktion på $A$ , är funktionen som skickar det naturliga talet $n$ till $f n (e)$ , det vill säga $f (f (\dots(f (e))...))$ , den $n$ -faldiga tillämpningen av $f$ till $e$ .

Mängden naturliga tal är bäraren för en initial algebra för denna funktion: punkten är noll och funktionen är efterföljande funktion .

Funktion $1 + N \times (-)$

För ett andra exempel, betrakta endofunktorn $1 + N \times (-)$ i kategorin mängder, där $N$ är mängden naturliga tal. En algebra för denna endofunctor är en mängd $X$ tillsammans med en funktion $1 + N \times X \to X$ . För att definiera en sådan funktion behöver vi en punkt $x\in X$ och en funktion $N \times X \to X$ . Uppsättningen av ändliga listor av naturliga tal är en initial algebra för denna funktion. Poängen är den tomma listan, och funktionen är cons , tar ett tal och en finit lista och returnerar en ny finit lista med numret i spetsen.

I kategorier med binära samprodukter motsvarar de nyss angivna definitionerna de vanliga definitionerna av ett naturligt talobjekt respektive ett listobjekt .

Sista koalgebra

Dualt är en slutlig koalgebra ett terminalobjekt i kategorin $F$ -koalgebra . Finaliteten ger en allmän ram för koinduktion och corecursion .

Till exempel, med samma funktion $1 + (-)$ som tidigare, definieras en koalgebra som en mängd $X$ tillsammans med en funktion $f : X \to (1 + X)$ . Att definiera en sådan funktion motsvarar att definiera en partiell funktion $f' : X ⇸ Y$ vars domän bildas av de $x\in X$ för vilka $f (x)$ hör till $1$ . En sådan struktur kan ses som en kedja av mängder, $X 0$ på vilken $f'$ inte är definierad, $X 1$ vilka element mappar till $X 0$ med $f'$ , $X 2$ vilka element mappar till $X 1$ med $f'$ , etc. och $X ω$ som innehåller de återstående elementen i $X$ . Med detta i sikte är mängden $\mathbf {N} \cup \{\omega \}$ bestående av mängden naturliga tal utökade med ett nytt element $ω$ bäraren av den slutliga koalgebra i kategorin, där $f'$ är föregångarens funktion ( inversen av efterföljarfunktionen) på de positiva naturliga, men fungerar som identiteten på det nya elementet $ω$ : $f (n + 1) = n$ , $f (ω) = ω$ . Denna mängd $\mathbf {N} \cup \{\omega \}$ som är bäraren för den slutliga koalgebran av $1 + (-)$ är känd som uppsättningen av konaturliga tal.

För ett andra exempel, betrakta samma funktor $1 + N \times (-)$ som tidigare. I detta fall består bäraren av den slutliga koalgebra av alla listor av naturliga tal, finita såväl som oändliga . Operationerna är en testfunktion som testar om en lista är tom, och en dekonstruktionsfunktion definierad på icke-tomma listor som returnerar ett par bestående av huvudet och svansen av inmatningslistan.

Satser

Initiala algebror är minimala (dvs. har ingen riktig subalgebra).
Slutliga koalgebras är enkla (dvs. har inga korrekta kvoter).

Används inom datavetenskap

Olika finita datastrukturer som används i programmering , såsom listor och träd , kan erhållas som initiala algebror för specifika endofunctors. Även om det kan finnas flera initiala algebror för en given endofunctor, är de unika upp till isomorfism , vilket informellt betyder att de "observerbara" egenskaperna hos en datastruktur kan fångas adekvat genom att definiera den som en initial algebra.

För att erhålla typen $List(A)$ av listor vars element är medlemmar i uppsättning $A$ , tänk på att de listbildande operationerna är:

$\mathrm {noll} \colon 1\to \mathrm {List} (A)$
$\mathrm {cons} \colon A\times \mathrm {List} (A)\to \mathrm {List} (A)$

Kombinerade till en funktion ger de:

$[\mathrm {noll} ,\mathrm {cons} ]\ kolon (1+A\ gånger \mathrm {List} (A))\till \mathrm {List} (A),$

vilket gör detta till en $F$ -algebra för endofunktorn $F$ som skickar $X$ till $1+ (A \times X)$ . Det är faktiskt den initiala $F$ -algebra. Initialitet etableras av funktionen som kallas foldr i funktionella programmeringsspråk som Haskell och ML .

Likaså kan binära träd med element vid bladen erhållas som initial algebra

$[\mathrm {tip} ,\mathrm {join} ]\colon A+(\mathrm {Träd} (A)\ gånger \mathrm {Träd} (A))\till \mathrm {Träd} (A).$

Typer som erhålls på detta sätt är kända som algebraiska datatyper .

Typer definierade genom att använda minst fixpunktskonstruktion med funktion $F$ kan betraktas som en initial $F$ -algebra, förutsatt att parametrisiteten gäller för typen.

På ett dubbelt sätt finns ett liknande förhållande mellan föreställningar om största fixpunkt och terminal $F$ -koalgebra, med tillämpningar på koduktiva typer. Dessa kan användas för att tillåta potentiellt oändliga objekt samtidigt som en stark normaliseringsegenskap bibehålls . I det starkt normaliserande (varje program avslutas) Charity-programmeringsspråket kan koduktiva datatyper användas för att uppnå överraskande resultat, t.ex. definiera uppslagskonstruktioner för att implementera sådana " starka" funktioner som Ackermann-funktionen .

Se även

Anteckningar

^ ^a ^b Philip Wadler: Rekursiva typer gratis! University of Glasgow, juli 1998. Utkast.
^ Robin Cockett: Välgörande tankar ( ps.gz )

externa länkar

Kategorisk programmering med induktiva och koduktiva typer av Varmo Vene
Rekursiva typer gratis! av Philip Wadler, University of Glasgow, 1990-2014.
Initial Algebra och Final Coalgebra Semantics for Concurrency av JJMM Rutten och D. Turi
Initialitet och finalitet från CLiki
Maskinskrivna etikettlösa sluttolkar av Oleg Kiselyov

[free-rectypes-1] Philip Wadler: Rekursiva typer gratis! University of Glasgow, juli 1998. Utkast.

[2] Robin Cockett: Välgörande tankar ( ps.gz )