Полиномиальный функтор (теория типов) - Polynomial functor (type theory)

Эта статья является сирота, как никакие другие статьи ссылка на это. Пожалуйста ввести ссылки на эту страницу из Статьи по Теме; попробуйте Инструмент поиска ссылок для предложений. (Март 2018 г.)

В теория типов, а полиномиальный функтор (или же контейнерный функтор) является своего рода эндофунктор из категория типов, которые тесно связаны с концепцией индуктивный и коиндуктивный типы. В частности, все W-типы (соответственно M-типы) (изоморфны) начальные алгебры (соотв. финальные коалгебры ) таких функторов.

Полиномиальные функторы изучались в более общем контексте претопы с Σ-типами,^[1] в данной статье рассматриваются только приложения этой концепции внутри категории типов Теория типов стиля Мартина-Лёфа.

Определение

Позволять U быть вселенная типов, пусть А : U, и разреши B : А → U быть семейством типов, индексируемых А. Пара (А, B) иногда называют подпись^[2] или контейнер.^[3] В полиномиальный функтор связанный с контейнером (А, B) определяется следующим образом:^[4][5][6]

$${ displaystyle { begin {align} P: U & longrightarrow U X & longmapsto sum _ {a: A} (B (a) to X) end {выравнивается}}.}$$

Любой функтор, естественно изоморфный п называется контейнерный функтор.^[7] Действие п на функциях определяется

$${ displaystyle { begin {align} P ^ {*} :( X to Y) & longrightarrow (P ^ {*} X to P ^ {*} Y) (f, (a, g) ) & longmapsto (a, g circ f) end {align}}.}$$

Обратите внимание, что это присвоение действительно функториально не только в теориях экстенсионального типа (см. #Характеристики ).

Характеристики

В теориях интенсионального типа такие функции на самом деле не являются функторами, потому что тип вселенной не является строго категорией (областью теория гомотопического типа посвящен изучению того, как тип вселенной ведет себя больше как высшая категория ). Однако он функториален с точностью до пропозициональных равенств, то есть населяют следующие типы идентичности:

$${ displaystyle { begin {align} P ^ {*} (f circ g) & = P ^ {*} f circ P ^ {*} g P ^ {*} ({ mathsf {id} } _ {X}) & = { mathsf {id}} _ {PX} end {align}}.}$$

для любых функций ж и грамм и любого типа Икс, куда ${ displaystyle { mathsf {id}} _ {X}}$ это функция идентичности по типу Икс.^[8]

Встроенные цитаты

Рекомендации

• Программа Univalent Foundations (2013 г.). Теория гомотопических типов: однолистные основы математики. Институт перспективных исследований. п. 159.
• Awodey, Стив; Гамбино, Никола; Соякова, Кристина (18.01.2012). «Индуктивные типы в теории гомотопических типов». arXiv:1201.3898 [math.LO ].
• Awodey, Стив; Гамбино, Никола; Соякова, Кристина (21.04.2015). «Гомотопически-начальные алгебры в теории типов». arXiv:1504.05531 [math.LO ].
• Аренс, Бенедикт; Каприотти, Паоло; Спадотти, Режис (12 апреля 2015 г.). «Необоснованные деревья в теории гомотопических типов». arXiv:1504.02949. Дои:10.4230 / LIPIcs.TLCA.2015.17. Цитировать журнал требует | журнал = (помощь)
• Эбботт, Майкл; Альтенкирх, Торстен; Гани, Нил (2005). «Контейнеры: конструирование строго положительных типов». Теоретическая информатика. 342 (1): 4. Дои:10.1016 / j.tcs.2005.06.002.

внешняя ссылка

• Обширная коллекция Замечания о полиномиальных функторах