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 recursión .

Ejemplos

Functor incógnita ↦ 1 + incógnita {\displaystyle X\mapsto 1+X}

Consideremos el endofunctor F  : ConjuntoConjunto que envía 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 el 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 [zero,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 para una 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 -vez de f a e .

El conjunto de 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 .

Functor1 + N × (−)

Para un segundo ejemplo, considere el endofuntor 1 + N × (−) en la categoría de conjuntos, donde N es el conjunto de números naturales. Un álgebra para este endofuntor es un conjunto X junto con una función 1 + N × XX . Para definir dicha 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 , que toma un número y una lista finita y devuelve una nueva lista finita con el número a la cabeza.

En categorías con coproductos binarios , las definiciones recién dadas son equivalentes a las definiciones habituales de un objeto de número natural y un objeto de lista , respectivamente.

Coálgebra 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 correcursión .

Por ejemplo, utilizando el mismo funtor 1 + (−) que antes, una coalgebra se define como un conjunto X junto con una función f  : X → (1 + X ) . Definir una función de este tipo equivale a definir una función parcial f' : XX cuyo dominio está formado por aquellas para las que f ( x ) no pertenece a 1 . Teniendo una estructura de este tipo, podemos definir una cadena de conjuntos: X 0 siendo 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 ω conteniendo los elementos restantes de X . Con esto en vista, el conjunto , consistente en el conjunto de los números naturales ampliados con un nuevo elemento ω , es el portador de la coalgebra final, donde es la función predecesora (la inversa de la función sucesora) sobre los naturales positivos, pero actúa como la identidad sobre el nuevo elemento ω : f ( n + 1) = n , f ( ω ) = ω . Este conjunto que es portador de la coalgebra final de 1 + (−) se conoce como el 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 consiste en 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 consiste en la cabeza y la cola 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 endofuntores específicos. Si bien puede haber varias álgebras iniciales para un endofuntor dado, son únicas hasta el isomorfismo , lo que informalmente significa que las propiedades "observables" de una estructura de datos se pueden capturar 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 sola función, dan como resultado:

lo que la convierte en una F -álgebra para el endofunctor F que envía X a 1 + ( A × X ) . Es, de hecho, la F -álgebra inicial . La inicialidad la establece la función conocida como foldr en lenguajes de programación funcional como Haskell y ML .

De la misma manera, los árboles binarios con elementos en las hojas se pueden obtener como el á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 del punto mínimo fijo con el funtor F pueden considerarse como un F -álgebra inicial, siempre que se cumpla la parametricidad para el tipo. [1]

De manera dual, existe una relación similar entre las nociones de máximo punto fijo y F -coálgebra terminal, con aplicaciones a los tipos coinductivos . Estos pueden usarse para permitir objetos potencialmente infinitos mientras se mantiene la propiedad de normalización fuerte . [1] En el lenguaje de programación Charity, fuertemente normalizador (cada programa termina), los tipos de datos coinductivos pueden usarse para lograr resultados sorprendentes, por ejemplo, definiendo construcciones de búsqueda para implementar funciones tan “fuertes” como la función de Ackermann . [2]

Véase también

Notas

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

Enlaces externos