¿Qué son las categorías κappa?

Question

Hola,

Tengo una simple pregunta:

¿Qué son $\kappa$ -¿Categorías?

¿Tiene algo relacionado para seguir leyendo?

Gracias y saludos,

frosch03

editar: En realidad hay un artículo llamado "Closed Freyd- and kappa-categories" de A. John Power y Hayo Thielecke (portal.acm.org/citation.cfm?id=646229.681558)

Answer 1

La explicación intuitiva es que $\kappa$ -Las categorías son para las funciones de primer orden lo que las categorías cerradas cartesianas son para las funciones de orden superior.

Todo esto comenzó con el trabajo de Lambek sobre las categorías polinómicas; la mejor referencia para ello es J. Lambek. Completitud funcional de las categorías cartesianas. Annals of Mathematical Logic, 6:251-292, 1973 . Ese documento introdujo la elección de la letra $\kappa$ . Una categoría polinómica es lo que se obtiene cuando se toma una categoría con un objeto terminal, se elige un objeto $X$ y luego adjuntar libremente un nuevo morfismo $f:1\to X$ y cerrar bajo la composición. Esto es muy parecido al anillo de polinomios $R[X]$ sobre un anillo $R$ Se llega a ella adhiriendo un elemento indeterminado y cerrando bajo las operaciones del anillo. Lambek muestra que esta propiedad puede enunciarse en términos universales, como la única categoría que admite un tipo particular de functor desde la categoría original. Esto es formalmente más satisfactorio, pero no es el mejor camino para los principiantes.

Más tarde, Hasegawa desarrolló esta idea mucho más en M. Hasegawa. Decomponiendo el cálculo lambda tipado en un par de lenguajes de programación categóricos. Lecture Notes in Computer Science, 953, 1995. Demostró que al igual que el $\lambda$ -puede utilizarse como una "sintaxis" para especificar morfismos en una categoría cerrada cartesiana, también puede utilizarse el $\kappa$ -Cálculo -- aproximadamente el $\lambda$ -cálculo sin funciones de primera clase- ser utilizado como una "sintaxis" para especificar morfismos. Recomiendo estudiar la figura que aparece inmediatamente después del primer párrafo de la sección 3 de su artículo (con mucha atención). Transmite tanto la esencia de estas categorías como su relevancia para el estudio de los lenguajes de programación.

Para terminar, las categorías cerradas cartesianas han sido una herramienta inmensamente útil para entender los lenguajes de programación con funciones de primera clase. Lamentablemente, sólo pueden utilizarse para estudiar lenguajes con la propiedad de que para cada par de tipos $B$ y $C$ también hay un tipo de funciones de $B\Rightarrow C$ y las formas de conseguir un $B\Rightarrow C$ de un $A$ están en correspondencia uno a uno con las formas de conseguir un $C$ a partir de un par (cartesiano) de un $A$ y un $B$ . Lambek-Hasegawa $\kappa$ -Las categorías son una forma elegante de extender estas técnicas a los lenguajes en los que esta suposición no se cumple.

Por último, como postdata, tanto Lambek como Hasegawa asumen que la estructura monoidal subyacente de sus categorías es cartesiana. Algunos de los resultados más fascinantes surgen cuando se repiten sus construcciones en categorías que son meramente binoidales o premonoidales -- se sorprendería de las pocas modificaciones que se requieren.