Álgebra inicial

En matemáticas , un álgebra inicial es un objeto inicial en la categoría de $F$ -álgebras para un endofunctor $F$ dado . Esta inicialidad proporciona un marco general para la inducción y la recursión .

Ejemplos

Functor $1 + (-)$

Consideremos el endofunctor $1 + (-)$ , es decir $F : Conjunto \to Conjunto$ que envía $X$ a $1 + X$ , donde $1 es un$ conjunto de un punto ( conjunto único ) , un objeto terminal en la categoría. Un álgebra para este endofunctor es un conjunto $X$ (llamado portador del álgebra) junto con una función $f$ $: (1 +$ $X$ $) \to$ $X$ . Definir dicha función equivale a definir un punto $x$ $\in$ $X$ y una función $X$ $\to$ $X$ . Definir

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

y

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

Entonces, el conjunto $N$ de números naturales junto con la función $[zero,succ]: 1 + N \to N$ es un álgebra $F$ inicial . La inicialidad (la propiedad universal para este caso) no es difícil de establecer; el homomorfismo único a un álgebra $F arbitraria$ $(A, [e, f])$ , para $e : 1 \to A$ un elemento de $A$ y $f : A \to A$ una función en $A$ , es la función que envía el número natural $n$ a $f n (e)$ , es decir, $f (f (\dots(f (e))\dots))$ , la aplicación $n -ésima de$ $f$ a $e$ .

El conjunto de los números naturales es el portador de un álgebra inicial para este functor: el punto es cero y la función es la función sucesora .

Functor $1 + N \times (-)$

Como segundo ejemplo, consideremos el endofunctor $1 + N \times (-)$ en la categoría de conjuntos, donde $N$ es el conjunto de los números naturales. Un álgebra para este endofunctor es un conjunto $X$ junto con una función $1 + N \times X \to X.$ Para definir dicha función, necesitamos un punto $x \in X$ y una función $N \times X \to X.$ El conjunto de listas finitas de números naturales es un álgebra inicial para este functor. El punto es la lista vacía, y la función es cons , que toma un número y una lista finita, y devuelve una nueva lista finita con el número en la cabecera.

En las categorías con coproductos binarios , las definiciones que se acaban de dar son equivalentes a las definiciones habituales de un objeto de número natural y un objeto de lista , respectivamente.

Coalgebra final

De manera similar , una coálgebra final es un objeto terminal en la categoría de $F$ -coálgebras . La finalidad proporciona un marco general para la coinducción y la correcursión .

Por ejemplo, usando el mismo functor $1 + (-)$ que antes, una coálgebra se define como un conjunto $X$ junto con una función $f : X \to (1 + X)$ . Definir tal función equivale a definir una función parcial $f' : X ⇸ X$ cuyo dominio está formado por esos $x\in X$ para el cual $f (x)$ no pertenece a $1$ . Teniendo tal estructura, podemos definir una cadena de conjuntos: $X 0$ siendo un subconjunto de $X$ en el cual $f'$ no está definido, $X 1$ cuyos elementos se mapean en $X 0$ por $f'$ , $X 2$ cuyos elementos se mapean en $X 1$ por $f'$ , etc., y $X ω$ conteniendo los elementos restantes de $X$ . Con esto en mente, el conjunto $\mathbf {N} \cup \{\omega \}$ , que consiste en el conjunto de números naturales extendido con un nuevo elemento $ω$ , es el portador de la coálgebra final, donde $f'$ es la función predecesora (la inversa de la función sucesora) en los naturales positivos, pero actúa como la identidad en el nuevo elemento $ω$ : $f (n + 1) = n$ , $f (ω) = ω$ . Este conjunto $\mathbf {N} \cup \{\omega \}$ que es el portador de la coálgebra final de $1 + (-)$ se conoce como el conjunto de números conaturales.

Como segundo ejemplo, consideremos el mismo functor $1 + N \times (-)$ que antes. En este caso, el portador de la coálgebra final consiste en todas las listas de números naturales, tanto finitas como infinitas . Las operaciones son una función de prueba que verifica si una lista está vacía y una función de deconstrucción definida sobre listas no vacías que devuelve un par formado por la cabeza y la cola de la lista de entrada.

Teoremas

Las álgebras iniciales son mínimas (es decir, no tienen subálgebra propia).
Las coálgebras finales son simples (es decir, no tienen cocientes propios).

Uso en informática

Diversas estructuras de datos finitas utilizadas en programación , como listas y árboles , pueden obtenerse como álgebras iniciales de endofuntores específicos. Si bien puede haber varias álgebras iniciales para un endofuntor dado, son únicas salvo isomorfismo , lo que informalmente significa que las propiedades "observables" de una estructura de datos pueden capturarse adecuadamente definiéndola como un álgebra inicial.

Para obtener el tipo $List(A)$ de listas cuyos elementos son miembros del conjunto $A$ , considere que las operaciones de formación de listas son:

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

Combinadas en una sola función, dan como resultado:

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

lo que convierte a esta en un álgebra $F$ para el endofunctor $F$ que envía $X$ a $1 + (A \times X)$ . De hecho, es el álgebra $F$ inicial . La inicialidad se establece mediante la función conocida como foldr en lenguajes de programación funcional como Haskell y ML .

Asimismo, se pueden obtener árboles binarios con elementos en las hojas como álgebra inicial.

$[\mathrm {tip} ,\mathrm {unirse} ]\colon A+(\mathrm {Árbol} (A)\times \mathrm {Árbol} (A))\to \mathrm {Árbol} (A).$

Los tipos obtenidos de esta manera se conocen como tipos de datos algebraicos .

Los tipos definidos mediante la construcción de punto fijo mínimo con functor $F$ pueden considerarse como un álgebra $F inicial, siempre que se cumpla$ la parametricidad para el tipo. ^{[ 1 ]}

De manera dual, existe una relación similar entre las nociones de punto fijo máximo y $F$ -coalgebra terminal, con aplicaciones a los tipos coinductivos . Estos pueden usarse para permitir objetos potencialmente infinitos manteniendo la propiedad de normalización fuerte . ^{[ 1 ]} En el lenguaje de programación Charity, que normaliza fuertemente (cada programa termina), los tipos de datos coinductivos pueden usarse para lograr resultados sorprendentes, por ejemplo, definir construcciones de búsqueda para implementar funciones "fuertes" como la función de Ackermann . ^{[ 2 ]}

Véase también

Notas

1 2 Philip Wadler: ¡ Tipos recursivos gratis! Universidad de Glasgow, julio de 1990. Borrador.
↑ Robin Cockett : Pensamientos caritativos ( ps.gz )

Enlaces externos

Programación categórica con tipos inductivos y coinductivos por Varmo Vene
¡Tipos recursivos gratis! por Philip Wadler, Universidad de Glasgow, 1990-2014.
Álgebra inicial y semántica de coalgebra final para la concurrencia por JJMM Rutten y D. Turi
Inicialidad y finalidad de CLIki
Intérpretes finales sin etiquetas, escritos por Oleg Kiselyov

[free-rectypes-1] 1 2 Philip Wadler: ¡ Tipos recursivos gratis! Universidad de Glasgow, julio de 1990. Borrador.

[2] Robin Cockett : Pensamientos caritativos ( ps.gz )

[ 1 ]

[ 2 ]