Listobjekt
Inom kategoriteorin , en abstrakt gren av matematiken , och i dess tillämpningar på logik och teoretisk datavetenskap , är ett listobjekt en abstrakt definition av en lista , det vill säga en ändligt ordnad sekvens .
Formell definition
Låt C vara en kategori med ändliga produkter och ett terminalobjekt 1. Ett listobjekt över ett objekt A av C är:
- ett föremål L A ,
- a morfism o A : 1 → LA , och
- a morfism s A : A × L A → L A
så att det för alla objekt B i C med kartor b : 1 → B och t : A × B → B finns ett unikt f : L A → B så att följande diagram pendlar :
där〈id A , f 〉betecknar pilen som induceras av produktens universella egenskap när den appliceras på id A (identiteten på A ) och f . Notationen A * ( à la Kleene stjärna ) används ibland för att beteckna listor över A .
Motsvarande definitioner
I en kategori med ett terminalobjekt 1, binära samprodukter (betecknade med +) och binära produkter (betecknade med ×), kan ett listobjekt över A definieras som den initiala algebra för endofunktorn som verkar på objekt med X ↦ 1 + ( A × X ) och på pilarna med f ↦ [id 1 ,〈id A , f 〉].
Exempel
- I Set , kategorin för mängder , är listobjekt över en mängd A helt enkelt ändliga listor med element ritade från A . I det här fallet väljer o A ut den tomma listan och s A motsvarar att lägga till ett element till listans huvud.
- I kalkylen för induktiva konstruktioner eller liknande typteorier med induktiva typer (eller heuristiskt sett till och med starkt typade funktionsspråk som Haskell ) är listor typer som definieras av två konstruktorer, noll och nackdelar , som motsvarar o A respektive s A . Rekursionsprincipen för listor garanterar att de har den förväntade universella egendomen.
Egenskaper
Liksom alla konstruktioner som definieras av en universell egenskap är listor över ett objekt unika upp till kanonisk isomorfism .
Objektet L 1 (listor över terminalobjektet) har den universella egenskapen för ett naturligt talobjekt . I vilken kategori som helst med listor kan man definiera längden på en lista L A som den unika morfismen l : L A → L 1 som gör att följande diagram pendlar:
- Johnstone, Peter T. (2002). Sketcher of an Elephant: a Topos Theory Compendium . Oxford: Oxford University Press. ISBN 0198534256 . OCLC 50164783 .
Se även
|
 |
|||||||||||||||||
| ||||||||||||||||||
