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 recursividad .
Ejemplos de
Functor 1 + X
Considere la endofunctor F : Set → Set envío de X a 1 + X , donde 1 es la de un punto ( singleton ) conjunto , el objeto terminal en la categoría. Un álgebra para este endofunctor es un conjunto X (llamado el portador de la álgebra) junto con una función f : (1 + X ) → X . Definir tal función equivale a definir un puntoy una función de X → X . Definir
y
Entonces el conjunto N de números naturales junto con la función [cero, succ]: 1 + N → N es una F -álgebra inicial . La inicialidad (la propiedad universal para este caso) no es difícil de establecer; el único homomorfismo a un arbitrario F -algebra ( A , [ e , f ]) , para e : 1 → A un elemento de A y f : A → A una función en A , es la función de enviar el número natural n a f n ( e ) , es decir, f ( f (… ( f ( e ))…)) , la aplicación n- veces de f a e .
El conjunto de números naturales es el portador de un álgebra inicial para este funtor: el punto es cero y la función es la función sucesora .
Functor 1 + N × (-)
Para un segundo ejemplo, considere el endofunctor 1 + N × (-) en la categoría de conjuntos, donde N es el conjunto de números naturales. Un álgebra para este endofunctor es un conjunto X junto con una función de 1 + N × X → X . Para definir tal función, necesitamos un puntoy una función de N × X → X . El conjunto de listas finitas de números naturales es un álgebra inicial para este funtor. El punto es la lista vacía y la función es contras , tomando un número y una lista finita, y devolviendo una nueva lista finita con el número al principio.
En 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
Dualmente , una coalgebra final es un objeto terminal en la categoría de F -coalgebras . La finalidad proporciona un marco general para la coinducción y la correcursión .
Por ejemplo, usando el mismo functor 1 + (-) que antes, una coalgebra se define como un conjunto X junto con una función f : X → (1 + X ) . Definir tal función equivale a definir una función parcial f ' : X ⇸ Y cuyo dominio está formado por aquellospara lo cual f ( x ) pertenece a 1 . Tal estructura se puede ver como una cadena de conjuntos, X 0 en el que f ′ no está definido, X 1 qué elementos se asignan a X 0 por f ′ , X 2 qué elementos se asignan a X 1 por f ′ , etc., y X ω que contiene los elementos restantes de X . Con esto en vista, el conjuntoque consiste en el conjunto de números naturales extendidos con un nuevo elemento ω es el portador de la coalgebra final en la categoría, dondees 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 conjuntoque es el portador de la coalgebra final de 1 + (-) se conoce como el conjunto de números naturales.
Para un segundo ejemplo, considere el mismo functor 1 + N × (-) que antes. En este caso, el portador de la coalgebra final consta de todas las listas de números naturales, tanto finitos como infinitos . Las operaciones son una función de prueba que prueba si una lista está vacía y una función de deconstrucción definida en listas no vacías que devuelven un par que consta de la cabeza y la cola de la lista de entrada.
Teoremas
- Las álgebras iniciales son mínimas (es decir, no tienen una subálgebra adecuada).
- Las coalgebras finales son simples (es decir, no tienen cocientes adecuados).
Uso en informática
Varias estructuras de datos finitas utilizadas en programación , como listas y árboles , se pueden obtener como álgebras iniciales de endofunctores específicos. Si bien puede haber varias álgebras iniciales para un endofunctor dado, son únicas hasta el 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 Lista ( A ) de listas cuyos elementos son miembros del conjunto A , considere que las operaciones de formación de listas son:
Combinados en una función, dan:
lo que hace que esta sea una F -álgebra para el endofunctor F que envía X a 1 + ( A × X ) . De hecho, es el F -álgebra 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.
Los tipos obtenidos de esta manera se conocen como tipos de datos algebraicos .
Los tipos definidos mediante el uso de la construcción de punto mínimo fijo con el functor F pueden considerarse como un F- álgebra inicial , siempre que la parametricidad sea válida para el tipo. [1]
De manera dual, existe una relación similar entre las nociones de punto fijo mayor y F -coalgebra terminal , con aplicaciones a tipos coinductivos . Estos pueden usarse para permitir objetos potencialmente infinitos mientras se mantiene una fuerte propiedad de normalización . [1] En el lenguaje de programación Charity fuertemente normalizado (cada programa termina), los tipos de datos coinductivos se pueden usar para lograr resultados sorprendentes, por ejemplo, definir construcciones de búsqueda para implementar funciones tan “fuertes” como la función Ackermann . [2]
Ver también
- Tipo de datos algebraicos
- Catamorfismo
- Anamorfismo
Notas
- ^ a b Philip Wadler: ¡ Tipos recursivos gratis! Universidad de Glasgow, julio de 1998. 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.
- Semántica de Álgebra Inicial y Coalgebra Final para Concurrencia por JJMM Rutten y D. Turi
- Inicialidad y finalidad de CLiki
- Intérpretes finales sin etiquetas mecanografiados por Oleg Kiselyov