stringtranslate.com

Á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 recursividad .

Ejemplos

Funtor X ↦ 1 + X {\displaystyle X\mapsto 1+X}

Considere el endofunctor F  : ConjuntoConjunto enviando X a 1 + X , donde 1 es un conjunto de un punto ( singleton ) , 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 ) → X . Definir una función de este tipo equivale a definir un punto y una función XX . Definir

y

Entonces el conjunto N de números naturales junto con la función [cero,succ]: 1 + NN es una F -álgebra inicial . La inicialidad (la propiedad universal para este caso) no es difícil de establecer; el homomorfismo único de un F -álgebra arbitraria ( A , [ e , f ] ) , para e : 1 → A un elemento de A y f : AA 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 (…( f ( e ))…)) , la aplicación n veces de f a e .

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

Funtor 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 1 + N × XX . Para definir tal función, necesitamos un punto y una función N × XX . 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 cons , 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 -coálgebras . La finalidad proporciona un marco general para la coinducción y la corecursión .

Por ejemplo, usando el mismo funtor 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' : XX cuyo dominio está formado por aquellos para los cuales f ( x ) no pertenece a 1 . Teniendo tal estructura, podemos definir una cadena de conjuntos: siendo X 0 un subconjunto de X en el que f no está definido, X 1 cuyos elementos se asignan a X 0 por f , X 2 cuyos elementos se asignan a X 1 por f , etc., y X ω que contiene los elementos restantes de X . Teniendo esto en cuenta, el conjunto , formado por el conjunto de números naturales ampliado con un nuevo elemento ω , es el portador de la coalgebra final, donde está la función predecesora (la inversa de la función sucesora) sobre los naturales positivos, pero actúa como la identidad del nuevo elemento ω : f ( n + 1 ) = n , f ( ω ) = ω . Este conjunto que es portador de la coalgebra final de 1 + (-) se conoce como conjunto de los números connaturales.

Para un segundo ejemplo, considere el mismo funtor 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 devuelve un par que consta del principio y el final de la lista de entrada.

Teoremas

Uso en informática

Varias estructuras de datos finitos 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 determinado, 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 álgebra F inicial . La inicialidad la establece la función conocida como foldr en lenguajes de programación funcionales 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 una construcción de punto mínimo fijo con funtor F pueden considerarse como un álgebra F inicial , siempre que la parametricidad sea válida para el tipo. [1]

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

Ver también

Notas

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

enlaces externos