Liste nesnesi - List object

İçinde kategori teorisi soyut bir dalı matematik ve uygulamalarında mantık ve teorik bilgisayar bilimi, bir liste nesnesi a'nın soyut bir tanımıdır liste, Bu bir sonlu sipariş sıra.

Resmi tanımlama

İzin Vermek C olmak kategori sonlu Ürün:% s ve bir terminal nesnesi 1 A liste nesnesi bir nesne Bir nın-nin C dır-dir:

  1. bir obje LBir,
  2. a morfizm ÖBir : 1 → LBir, ve
  3. bir morfizm sBir : Bir × LBir → LBir

öyle ki herhangi bir nesne için B nın-nin C haritalarla b : 1 → B ve t : Bir × B → Bbenzersiz bir f : LBir → B öyle ki aşağıdaki diyagram işe gidip gelme:

Bir liste nesnesinin tanımındaki denklemleri ifade eden değişmeli bir diyagram

nerede 〈idBir, f〉 Tarafından indüklenen oku gösterir. evrensel mülkiyet kimliğe uygulandığında ürününBir (üzerinde kimlik Bir) ve f. Gösterim Bir* (à la Kleene yıldızı ) bazen listeleri belirtmek için kullanılır Bir.[1]

Eşdeğer tanımlar

Terminal nesnesi 1 olan bir kategoride, ikili ortak ürünler (+ ile gösterilir) ve ikili ürünler (× ile gösterilir), üzerinde bir liste nesnesi Bir olarak tanımlanabilir ilk cebir of endofunktor nesnelere etki eden X ↦ 1 + (Bir × X) ve oklar üzerinde f ↦ [kimlik1,<İDBir, f〉].[2]

Örnekler

  • İçinde Ayarlamak, kümeler kategorisi, bir küme üzerindeki nesneleri listeleyin Bir basitçe sonlu listelerdir elementler çekilmek Bir. Bu durumda, ÖBir boş listeyi seçer ve sBir listenin başına bir öğe eklemeye karşılık gelir.
  • İçinde endüktif yapılar hesabı veya benzeri tip teorileri endüktif türlerle (veya sezgisel olarak, hatta şiddetle yazılmış işlevsel gibi diller Haskell ), listeler iki kurucu tarafından tanımlanan türlerdir, sıfır ve Eksilerikarşılık gelen ÖBir ve sBir, sırasıyla. Listelerin yineleme ilkesi, beklenen evrensel özelliğe sahip olmalarını garanti eder.

Özellikleri

A ile tanımlanan tüm yapılar gibi evrensel mülkiyet, bir nesnenin üzerindeki listeler benzersizdir. kanonik izomorfizm.

Nesne L1 (terminal nesnesi üzerindeki listeler), bir doğal sayı nesnesi. Listeli herhangi bir kategoride, uzunluk bir listenin LBir eşsiz morfizm olmak l : LBir → L1 Bu, aşağıdaki diyagramı işe gidip gelmesini sağlar:[3]

Bir liste nesnesinin uzunluğunun tanımındaki denklemleri ifade eden değişmeli bir diyagram

Referanslar

  1. ^ Johnstone 2002, A2.5.15.
  2. ^ Philip Wadler: Yinelemeli türler ücretsiz! Glasgow Üniversitesi, Temmuz 1998. Taslak.
  3. ^ Johnstone 2002, s. 117.
  • Johnstone, Peter T. (2002). Bir Filin Eskizleri: Bir Topos Teorisi Özeti. Oxford: Oxford University Press. ISBN  0198534256. OCLC  50164783.

Ayrıca bakınız