Lista obiektów
W teorii kategorii , abstrakcyjnej gałęzi matematyki oraz w jej zastosowaniach w logice i informatyce teoretycznej , obiekt listy jest abstrakcyjną definicją listy , czyli skończonej uporządkowanej sekwencji .
Definicja formalna
Niech C będzie kategorią z produktami skończonymi i obiektem końcowym 1. Obiekt listy nad obiektem A z C to:
- obiekt LA , _
- morfizm o A : 1 → LA , i
- morfizm s A : A × L A → LA A
takie, że dla dowolnego obiektu B z C z odwzorowaniami b : 1 → B i t : A × B → B , istnieje jednoznaczna f : LA → B taka, że następujący diagram komutuje :
gdzie〈id A , f 〉oznacza strzałkę wywołaną przez uniwersalną właściwość iloczynu po zastosowaniu do id A (tożsamość na A ) i f . Notacja A * ( gwiazda à la Kleene ) jest czasami używana do oznaczenia list nad A .
Równoważne definicje
W kategorii z obiektem końcowym 1, binarnymi koproduktami (oznaczonymi przez +) i iloczynami binarnymi (oznaczonymi przez × ) , obiekt listy nad A można zdefiniować jako początkową algebrę endofunktora , który działa na obiekty przez X ↦ 1 + ( A × X ) i na strzałkach przez f ↦ [id 1 ,〈id A , f 〉].
Przykłady
- W Set , kategorii zbiorów , listy obiektów nad zbiorem A są po prostu skończonymi listami z elementami wylosowanymi z A . W tym przypadku o A wybiera pustą listę, a s A odpowiada dołączeniu elementu do nagłówka listy.
- W rachunku konstrukcji indukcyjnych lub podobnych teoriach typów z typami indukcyjnymi (lub heurystycznie, nawet silnie typowanymi językami funkcyjnymi , takimi jak Haskell ), listy są typami zdefiniowanymi przez dwa konstruktory, nil i cons , które odpowiadają odpowiednio o A i s A . Zasada rekurencji dla list gwarantuje, że mają one oczekiwaną właściwość uniwersalną.
Nieruchomości
Jak wszystkie konstrukcje zdefiniowane przez uniwersalną właściwość , listy nad obiektem są unikalne aż do kanonicznego izomorfizmu .
Obiekt L 1 (listy nad obiektem końcowym) ma uniwersalną właściwość obiektu liczby naturalnej . W dowolnej kategorii z listami można zdefiniować długość listy L A jako unikalny morfizm l : LA → L 1 , który powoduje komutację następującego diagramu:
- Johnstone, Peter T. (2002). Szkice słonia: kompendium teorii toposu . Oksford: Oxford University Press. ISBN 0198534256 . OCLC 50164783 .
Zobacz też
|
 |
|||||||||||||||||
| ||||||||||||||||||
