Список объектов
 | Эта статья нуждается в дополнительных цитатах для проверки . ( декабрь 2017 г. ) |
В теории категорий , абстрактной отрасли математики , и в ее приложениях к логике и теоретической информатике , объект-список представляет собой абстрактное определение списка , то есть конечной упорядоченной последовательности .
Формальное определение
[ редактировать ]Пусть C с — категория конечными произведениями и терминальным объектом 1. Объект списка над объектом A из C :
- объект L A ,
- морфизм → o A : 1 L A и
- морфизм 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 * ( ля звезда Клини ) иногда используется для обозначения списков над A. а - [1]
Эквивалентные определения
[ редактировать ]В категории с терминальным объектом 1, двоичными копроизведениями (обозначаемыми +) и двоичными произведениями (обозначаемыми ×), объект списка над A может быть определен как исходная алгебра эндофунктора , который действует на объекты посредством X ↦ 1 + ( A × X ) и на стрелках посредством f ↦ [id 1 ,〈id A , f 〉]. [2]
Примеры
[ редактировать ]- В Set , категории множеств , объекты-списки в множестве A представляют собой просто конечные списки с элементами взятыми из A. , В этом случае o A выбирает пустой список, а s A соответствует добавлению элемента в начало списка.
- В исчислении индуктивных конструкций или подобных теориях типов с индуктивными типами (или, с эвристической точки зрения, даже в строго типизированных функциональных языках, таких как Haskell ), списки — это типы, определяемые двумя конструкторами, nil и cons , которые соответствуют o A и s A соответственно. Принцип рекурсии для списков гарантирует, что они обладают ожидаемым универсальным свойством.
Характеристики
[ редактировать ]Как и все конструкции, определяемые универсальным свойством , списки над объектом уникальны с точностью до канонического изоморфизма .
Объект L 1 (перечисляет объект-терминал) обладает универсальным свойством объекта натурального числа . В любой категории со списками можно определить длину списка L A как уникальный морфизм l : L A → L 1 , который делает следующую диаграмму коммутирующей: [3]
Ссылки
[ редактировать ]- ^ Джонстон 2002 , A2.5.15.
- ^ Филип Вадлер : Рекурсивные типы бесплатно! Университет Глазго, июль 1998 г. Проект.
- ^ Джонстон 2002 , с. 117.
- Джонстон, Питер Т. (2002). Зарисовки слона: сборник теории топоса . Оксфорд: Издательство Оксфордского университета. ISBN 0198534256 . OCLC 50164783 .
См. также
[ редактировать ]
|  | |||||||||||||||||
