В математике , начальная алгебра является исходным объектом в категории из F -алгебр для данного endofunctor F . Это начальное значение обеспечивает общую основу для индукции и рекурсии .
Примеры
Функтор 1 + X
Рассмотрим эндофунктор F : Set → Set отправка X равным 1 + X , где 1 - это одноточечный ( одноэлементный ) набор , конечный объект в категории. Алгебра для этого endofunctor представляет собой набор Х ( так называемый носитель алгебры) вместе с функцией F : (1 + Х ) → Х . Определение такой функции равносильно определению точкии функция Х → Х . Определять
а также
Тогда множество N натуральных чисел вместе с функцией [zero, succ]: 1 + N → N является исходной F -алгеброй. Первоначальность ( универсальное свойство в данном случае) установить нетрудно; единственный гомоморфизм произвольной F -алгебры ( A , [ e , f ]) для e : 1 → A - элемента A и f : A → A - функции на A , - это функция, переводящая натуральное число n в f n ( e ) , то есть f ( f (… ( f ( e ))…)) , n- кратное применение f к e .
Набор натуральных чисел является носителем исходной алгебры для этого функтора: точка равна нулю, а функция является функцией- преемником .
Функтор 1 + N × (-)
В качестве второго примера рассмотрим эндофунктор 1 + N × (-) в категории множеств, где N - множество натуральных чисел. Алгебра для этого endofunctor представляет собой набор X вместе с функцией 1 + N × X → X . Чтобы определить такую функцию, нам понадобится точкаи функция Н × Х → Х . Набор конечных списков натуральных чисел является начальной алгеброй для этого функтора. Точка - это пустой список, а функция - cons , беря число и конечный список и возвращая новый конечный список с числом во главе.
В категориях с бинарными копроизведениями , определения только данные эквивалентны обычными определениями природного объекта номера и список объектов , соответственно.
Заключительная коалгебра
Двойственно , окончательный коалгебра является терминальным объектом в категории F -коалгебр . Окончательность обеспечивает общую основу для коиндукции и коркурсии .
Например, с использованием того же функтора 1 + (-), что и раньше, коалгебра определяется как множество X вместе с функцией f : X → (1 + X ) . Определение такой функции сводится к определению частичной функции f ' : X ⇸ Y , область определения которой образована этимидля которых f ( x ) принадлежит 1 . Такую структуру можно рассматривать как цепочку множеств: X 0, на котором f ' не определено, X 1, элементы которого отображаются в X 0 с помощью f ' , X 2, какие элементы отображаются в X 1 с помощью f ' и т. Д., И Х ω , содержащий остальные элементы X . С учетом этого наборсостоящая из множества натуральных чисел, расширенных новым элементом ω, является носителем финальной коалгебры в категории, гдеявляется функцией-предшественником ( обратной функцией-последователем) на положительных натуральных числах, но действует как тождество на новом элементе ω : f ( n + 1) = n , f ( ω ) = ω . Этот наборто есть носитель окончательной коалгебры 1 + (-) известен как набор естественных чисел.
В качестве второго примера рассмотрим тот же функтор 1 + N × (-), что и раньше. В этом случае носитель окончательной коалгебры состоит из всех списков натуральных чисел, как конечных, так и бесконечных . Операции - это тестовая функция, проверяющая, является ли список пустым, и функция деконструкции, определенная для непустых списков, возвращающая пару, состоящую из головы и хвоста входного списка.
Теоремы
- Исходные алгебры минимальны (т. Е. Не имеют собственной подалгебры).
- Конечные коалгебры просты (т. Е. Не имеют собственных частных).
Использование в информатике
Различные конечные структуры данных, используемые в программировании , такие как списки и деревья , могут быть получены как начальные алгебры конкретных эндофункторов. Хотя для данного эндофунктора может быть несколько начальных алгебр, они уникальны с точностью до изоморфизма , что неформально означает, что «наблюдаемые» свойства структуры данных могут быть адекватно захвачены путем определения ее как начальной алгебры.
Чтобы получить список типа List ( A ) списков, элементы которых являются членами набора A , учтите, что операции формирования списка:
Объединенные в одну функцию, они дают:
что делает эту алгебру F -алгеброй для эндофунктора F, переводящего X в 1 + ( A × X ) . Фактически, это исходная F- алгебра. Первоначальность устанавливается функцией, известной как foldr в языках функционального программирования, таких как Haskell и ML .
Точно так же бинарные деревья с элементами на листьях могут быть получены как исходная алгебра
Полученные таким образом типы известны как алгебраические типы данных .
Типы, определенные с помощью конструкции с наименьшей фиксированной точкой с функтором F, можно рассматривать как исходную F -алгебру при условии, что для типа сохраняется параметричность . [1]
Схожая взаимосвязь существует между понятиями наибольшей фиксированной точки и терминальной F -коалгебры с приложениями к коиндуктивным типам. Их можно использовать для разрешения потенциально бесконечных объектов при сохранении строгого свойства нормализации . [1] В строго нормализующем (каждая программа завершается) языке программирования Charity коиндуктивные типы данных могут использоваться для достижения неожиданных результатов, например, для определения структур поиска для реализации таких «сильных» функций, как функция Аккермана . [2]
Смотрите также
- Алгебраический тип данных
- Катаморфизм
- Анаморфизм
Заметки
- ^ a b Филип Вадлер: Рекурсивные типы бесплатно! Университет Глазго, июль 1998 г. Проект.
- ^ Робин Кокетт: Благотворительные мысли ( ps.gz )
Внешние ссылки
- Категориальное программирование с индуктивными и коиндуктивными типами от Вармо Вен
- Рекурсивные типы бесплатно! Филип Вадлер, Университет Глазго, 1990–2014 гг.
- Начальная алгебра и финальная семантика коалгебры для параллелизма , JJMM Rutten и D. Turi
- Первоначальность и окончательность от CLiki
- Типизированные финальные переводчики без тегов - Олег Киселев