Начальная алгебра

В математике исходная алгебра — это исходный объект в категории алгебр $F$ - данного эндофунктора $F.$ для Эта первоначальность обеспечивает общую основу для индукции и рекурсии .

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

Функтор $X\mapsto 1+X$ [ редактировать ]

Рассмотрим эндофунктор $F : Set \to Set,$ отправляющий $X$ в $1 + X$ , где $1$ — одноточечный ( одиночный ) набор , терминальный объект в категории. Алгеброй для этого эндофунктора является множество $X$ (называемое носителем алгебры) вместе с функцией $f : (1 + X) \to X$ . Определение такой функции равносильно определению точки $x\in X$ функция $X \to X.$ и Определять

{\begin{aligned}\operatorname {zero} \colon 1&\longrightarrow \mathbf {N} \\*&\longmapsto 0\end{aligned}}

и

{\begin{aligned}\operatorname {succ} \colon \mathbf {N} &\longrightarrow \mathbf {N} \\n&\longmapsto n+1.\end{aligned}}

Тогда множество $N$ натуральных чисел вместе с функцией $[zero,succ]: 1 + N \to N$ является исходной $F$ -алгеброй. Первоначальность ( универсальное свойство для этого случая) установить нетрудно; единственный гомоморфизм произвольной $F$ -алгебры $(A, [e, f])$ , для $e : 1 \to A$ — элемент $A$ и $f : A \to A$ — функция на $A$ , — это функция, отправляющая натуральное число $n$ в $f н (e)$ , то есть $f (f (\dots(f (e))\dots))$ , $n$ -кратное применение $f$ к $e$ .

Множество натуральных чисел является носителем исходной алгебры для этого функтора: точка равна нулю, а функция является функцией-последователем .

Оператор $1 + N \times (-)$ [ править ]

В качестве второго примера рассмотрим эндофунктор $1 + N \times (-)$ в категории множеств, где $N$ — множество натуральных чисел. Алгеброй для этого эндофунктора является множество $X$ вместе с функцией $1 + N \times X \to X$ . Для определения такой функции нам нужна точка $x\in X$ и функция $N \times X \to X$ . Множество конечных списков натуральных чисел является исходной алгеброй для этого функтора. Точка — это пустой список, а функция — cons , берущая число и конечный список и возвращающая новый конечный список с числом в начале.

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

Окончательная коалгебра [ править ]

Двойственным образом финальная коалгебра является терминальным объектом в категории $F$ -коалгебр . Завершенность обеспечивает общую основу для коиндукции и корекурсии .

Например, используя тот же функтор $1 + (-),$ что и раньше, коалгебра определяется как множество $X$ вместе с функцией $f : X \to (1 + X)$ . Определение такой функции равнозначно определению частичной функции $f' : X ⇸ X,$ определения которой область образована теми $x\in X$ для которого $f (x)$ не принадлежит $1$ . Имея такую структуру, мы можем определить цепочку множеств: $X 0$ — подмножество $X$ , на котором $f'$ не определено, $X 1$ , элементы которого отображаются в $X 0$ посредством $f'$ , $X 2$ , элементы которого отображаются в $X 1$ посредством $f .'$ и т. д., а $X ω$ содержит остальные элементы $X$ . С учетом этого набор $\mathbf {N} \cup \{\omega \}$ , состоящий из множества натуральных чисел, расширенного новым элементом $ω$ , является носителем итоговой коалгебры, где $f'$ является функцией-предшественником ( обратной функции-последователя) для положительных натуральных чисел, но действует как тождество на новом элементе $ω$ : $f (n + 1) = n$ , $f (ω) = ω$ . Этот набор $\mathbf {N} \cup \{\omega \}$ то есть носитель конечной коалгебры $1 + (-),$ известен как набор натуральных чисел.

В качестве второго примера рассмотрим тот же функтор $1 + N \times (-)$ , что и раньше. В этом случае носитель конечной коалгебры состоит из всех списков натуральных чисел, как конечных, так и бесконечных . Операции представляют собой проверочную функцию, проверяющую, является ли список пустым, и функцию деконструкции, определенную для непустых списков, возвращающую пару, состоящую из головы и хвоста входного списка.

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

Исходные алгебры минимальны (т. е. не имеют собственной подалгебры).
Финальные коалгебры просты (т. е. не имеют собственных частных).

Использование в информатике [ править ]

Различные конечные структуры данных , используемые в программировании , такие как списки и деревья , могут быть получены как исходные алгебры конкретных эндофункторов.Хотя для данного эндофунктора может существовать несколько начальных алгебр, они уникальны с точностью до изоморфизма , что неформально означает, что «наблюдаемые» свойства структуры данных могут быть адекватно зафиксированы, определив ее как исходную алгебру.

Чтобы получить тип $List(A)$ списков, элементы которых являются членами множества $A$ , учтите, что операции формирования списков следующие:

$\mathrm {nil} \colon 1\to \mathrm {List} (A)$
$\mathrm {cons} \colon A\times \mathrm {List} (A)\to \mathrm {List} (A)$

Объединенные в одну функцию, они дают:

$[\mathrm {nil} ,\mathrm {cons} ]\colon (1+A\times \mathrm {List} (A))\to \mathrm {List} (A),$

что делает эту $F$ -алгебру для эндофунктора $F$ переводящим $X$ в $1 + (A \times X)$ . По сути, это исходная F $-$ алгебра. Инициальность устанавливается функцией, известной какfoldr в языках функционального программирования, таких как Haskell и ML .

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

$[\mathrm {tip} ,\mathrm {join} ]\colon A+(\mathrm {Tree} (A)\times \mathrm {Tree} (A))\to \mathrm {Tree} (A).$

Типы, полученные таким способом, известны как алгебраические типы данных .

Типы, определенные с использованием конструкции наименьшей неподвижной точки с функтором $F,$ можно рассматривать как исходную $F$ -алгебру при условии, что параметричность . для типа сохраняется ^[1]

Аналогичная связь существует двояким образом между понятиями наибольшей неподвижной точки и терминальной $F$ -коалгеброй с приложениями к коиндуктивным типам. Их можно использовать для разрешения потенциально бесконечных объектов, сохраняя при этом строгое свойство нормализации . ^[1] В языке программирования Charity со строгой нормализацией (каждая программа завершается) коиндуктивные типы данных могут использоваться для достижения неожиданных результатов, например, для определения конструкций поиска для реализации таких «сильных» функций, как функция Аккермана . ^[2]

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

Примечания [ править ]

^ Jump up to: Перейти обратно: ^а ^б Филип Вадлер: Рекурсивные типы бесплатно! Университет Глазго, июль 1998 г. Проект.
^ Робин Кокетт : Благотворительные мысли ( ps.gz )

Внешние ссылки [ править ]

Категориальное программирование с индуктивными и коиндуктивными типами Вармо Вене.
Рекурсивные типы бесплатно! Филип Уодлер, Университет Глазго, 1990–2014 гг.
Начальная алгебра и окончательная семантика коалгебры для параллелизма, авторы Дж.Дж.М.Руттен и Д.Тури.
Начальность и окончательность от CLiki
Финальные переводчики печатного текста без тегов от Олега Киселева

[free-rectypes-1] Jump up to: Перейти обратно: ^а ^б Филип Вадлер: Рекурсивные типы бесплатно! Университет Глазго, июль 1998 г. Проект.

[2] Робин Кокетт : Благотворительные мысли ( ps.gz )

[1]

[2]