Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

В теории категории , абстрактная ветви математики , так и в ее приложениях к логике и теоретической информатике , объект списка является абстрактным определением списка , то есть конечный упорядоченной последовательности .

Формальное определение [ править ]

Пусть C будет категорией с конечными продуктами и конечным объектом 1. Объект списка над объектом A из C :

  1. объект L A ,
  2. морфизм о А  : 1 → L A , и
  3. морфизм s A  : A × L A → L A

такое, что для любого объекта B из C с отображениями b  : 1 → B и t  : A × B → B существует единственное f  : L A → B такое, что следующая диаграмма коммутирует :

Коммутативная диаграмма, выражающая уравнения в определении объекта списка

где 〈id A , f〉 обозначает стрелку, индуцированную универсальным свойством продукта при применении к id A (тождество на A ) и f . Обозначения * ( а - ля звезда Клини ) иногда используется для обозначения списков над A . [1]

Эквивалентные определения [ править ]

В категории с терминальным объектом 1, бинарные копроизведения (обозначаются +), и бинарные продукты (обозначается ×), объект списка над А могут быть определены как исходная алгебра в endofunctor , который действует на объекты по X ↦ 1 + ( A × X ), а на стрелках - f ↦ [id 1 , 〈id A , f〉]. [2]

Примеры [ править ]

  • В комплекте , в категории множеств , список объекты по множеству А просто конечные списки с элементами взяты из A . В этом случае o A выбирает пустой список, а s A соответствует добавлению элемента в заголовок списка.
  • В исчислении индуктивных конструкций или аналогичных теорий типов с индуктивными типами (или эвристически даже строго типизированных функциональных языков, таких как Haskell ) списки - это типы, определяемые двумя конструкторами, nil и cons , которые соответствуют o A и s A , соответственно. Принцип рекурсии для списков гарантирует, что они обладают ожидаемым универсальным свойством.

Свойства [ править ]

Как и все конструкции, определяемые универсальным свойством , списки над объектом уникальны с точностью до канонического изоморфизма .

Объект L 1 (списки над конечным объектом) обладает универсальным свойством объекта натурального числа . В любой категории со списками можно определить длину списка L A как уникальный морфизм l  : L A → L 1, который коммутирует следующую диаграмму: [3]

Ссылки [ править ]

  1. ^ Джонстон 2002 , A2.5.15.
  2. ^ Филип Вадлер : Рекурсивные типы бесплатно! Университет Глазго, июль 1998 г. Проект.
  3. ^ Джонстон 2002 , стр. 117.
  • Джонстон, Питер Т. (2002). Эскизы слона: Сборник теории топоса . Оксфорд: Издательство Оксфордского университета. ISBN 0198534256. OCLC  50164783 .

См. Также [ править ]

  • Объект натурального числа
  • F-алгебра
  • Начальная алгебра