Коалгебры в теории категорий и их применение в информатике.
F-coalgebra
Коалгебра в теории категорий: определение, свойства, связь с алгебрами и ковариетами. Применение в информатике: ленивые вычисления, потоки данных, системы переходов.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
В математике, в частности в теории категорий, коалгебра — это структура, определяемая согласно функтору, с определенными свойствами, как указано ниже. Для алгебр и коалгебр функтор является удобным и общим способом организации сигнатуры. Это находит применение в информатике: примеры коалгебр включают ленивые вычисления, бесконечные структуры данных, такие как потоки, а также системы переходов. Коалгебры двойственны алгебрам. Подобно тому, как класс всех алгебр для данной сигнатуры и теории уравнений образует вариацию, класс всех коалгебр, удовлетворяющих данной теории уравнений, образует ковариацию, где сигнатура задается .
In mathematics, specifically in category theory, an coalgebra is a structure defined according to a functor , with specific properties as defined below. For both algebras and coalgebras, a functor is a convenient and general way of organizing a signature. This has applications in computer science: examples of coalgebras include lazy evaluation, infinite data structures, such as streams, and also transition systems. coalgebras are dual to algebras. Just as the class of all algebras for a given signature and equational theory form a variety, so does the class of all coalgebras satisfying a given equational theory form a covariety, where the signature is given by .
Примеры
Рассмотрим эндофунктор, который отображает множество в его дизъюнктное объединение с одноэлементным множеством. Коалгебра этого эндофунктора задается выражением , где – так называемые конатуральные числа, состоящие из неотрицательных целых чисел и бесконечности, а функция задается как , для и . Фактически, это терминальная коалгебра этого эндофунктора. В более общем случае, зафиксируем некоторое множество , и рассмотрим функтор, который отображает в . Тогда -коалгебра – это конечный или бесконечный поток над алфавитом , где – множество состояний, а – функция перехода между состояниями. Применение функции перехода к состоянию может дать два возможных результата: либо элемент вместе со следующим состоянием потока, либо элемент одноэлементного множества, определяющий отдельное "конечное состояние", указывающее на отсутствие дальнейших значений в потоке. Во многих практических приложениях функция перехода состояния такой коалгебры может иметь вид , которая легко факторизуется на множество "селекторов", "наблюдателей", "методов". Особые случаи, представляющие практический интерес, включают наблюдателей, возвращающих значения атрибутов, и методы-мутаторы вида , принимающие дополнительные параметры и возвращающие состояния. Это разложение является двойственным к разложению начальных алгебр на суммы "конструкторов". Пусть P – построение множества мощностей на категории множеств, рассматриваемое как ковариантный функтор. P-коалгебры находятся в биективном соответствии с множествами, снабженными бинарным отношением. Теперь зафиксируем другое множество, A. Тогда коалгебры для эндофунктора P(A×( )) находятся в биективном соответствии с помеченными системами переходов, а гомоморфизмы между коалгебрами соответствуют функциональным бисимуляциям между помеченными системами переходов.
Consider the endofunctor that sends a set to its disjoint union with the singleton set A coalgebra of this endofunctor is given by , where is the so called conatural numbers, consisting of the nonnegative integers and also infinity, and the function is given by , for and In fact, is the terminal coalgebra of this endofunctor. More generally, fix some set , and consider the functor that sends to Then an coalgebra is a finite or infinite stream over the alphabet , where is the set of states and is the state transition function. Applying the state transition function to a state may yield two possible results: either an element of together with the next state of the stream, or the element of the singleton set as a separate "final state" indicating that there are no more values in the stream. In many practical applications, the state transition function of such a coalgebraic object may be of the form , which readily factorizes into a collection of "selectors", "observers", "methods" Special cases of practical interest include observers yielding attribute values, and mutator methods of the form taking additional parameters and yielding states. This decomposition is dual to the decomposition of initial algebras into sums of 'constructors'. Let P be the power set construction on the category of sets, considered as a covariant functor. The P coalgebras are in bijective correspondence with sets with a binary relation. Now fix another set, A. Then coalgebras for the endofunctor P(A×( )) are in bijective correspondence with labelled transition systems, and homomorphisms between coalgebras correspond to functional bisimulations between labelled transition systems.
Приложения
В информатике, коалгебра стала удобным и достаточно общим способом спецификации поведения систем и структур данных, которые потенциально бесконечны, например, классы в объектно-ориентированном программировании, потоки и системы переходов. В то время как алгебраическая спецификация описывает функциональное поведение, обычно используя индуктивные типы данных, генерируемые конструкторами, коалгебраическая спецификация занимается поведением, моделируемым коиндуктивными типами процессов, которые наблюдаются посредством селекторов, во многом в духе теории автоматов. Важную роль здесь играют финальные коалгебры, представляющие собой полные множества, возможно, бесконечных поведений, таких как потоки. Естественной логикой для выражения свойств таких систем является коалгебраическая модальная логика.
In computer science, coalgebra has emerged as a convenient and suitably general way of specifying the behaviour of systems and data structures that are potentially infinite, for example classes in object oriented programming, streams and transition systems. While algebraic specification deals with functional behaviour, typically using inductive datatypes generated by constructors, coalgebraic specification is concerned with behaviour modelled by coinductive process types that are observable by selectors, much in the spirit of automata theory. An important role is played here by final coalgebras, which are complete sets of possibly infinite behaviours, such as streams. The natural logic to express properties of such systems is coalgebraic modal logic.