Оглавление
Начальная алгебра
-
Определение исходной алгебры
- Исходная алгебра – это объект в категории F-алгебр, который служит основой для индукции и рекурсии.
- Примеры включают алгебру натуральных чисел и конечные списки натуральных чисел.
-
Инициализация и универсальность
- Для каждого эндофунктора F существует единственная функция, которая является гомоморфизмом для произвольной F-алгебры.
- Множество натуральных чисел является носителем исходной алгебры для функтора 1 + N.
-
Конечная коалгебра
- Конечная коалгебра – это конечный объект в категории F-коалгебр, который обеспечивает основу для коиндукции и корекурсии.
- Множество натуральных чисел с добавлением элемента ω является носителем конечной коалгебры для функтора 1 + (−).
-
Теоремы и использование в информатике
- Исходные алгебры минимальны и не имеют собственной подалгебры.
- Конечные коалгебры просты и не имеют собственных частных.
- Исходные алгебры могут быть использованы для определения типов данных в программировании, таких как списки и деревья.
-
Примеры алгебраических типов данных
- Списки могут быть получены как исходная F-алгебра для эндофунктора, отправляющего X в 1 + (A × X).
- Бинарные деревья могут быть получены как исходная алгебра для эндофунктора, отправляющего X в A + (T × T).
-
Связь с коиндуктивными типами
- Коиндуктивные типы данных могут быть получены как исходные F-алгебры при условии параметризации типа.
- Коиндуктивные типы данных могут использоваться для создания потенциально бесконечных объектов с сохранением свойства строгой нормализации.