Categoría cerrada cartesiana

Una categoría cerrada cartesiana  es una categoría que admite curry , es decir, contiene para cada clase de morfismos algún objeto que la represente. Las categorías cerradas cartesianas ocupan, en cierto sentido, una posición intermedia entre las categorías abstractas y los conjuntos , ya que permiten operar correctamente con funciones , pero no permiten, por ejemplo, operar con subobjetos.

Desde el punto de vista de la programación , las categorías cerradas cartesianas implementan la encapsulación de argumentos de función: cada argumento está representado por un objeto de categoría y se utiliza como una caja negra . Al mismo tiempo, la expresividad de las categorías cerradas cartesianas es suficiente para operar con funciones en la forma adoptada en el cálculo λ . Esto los convierte en modelos categóricos naturales del cálculo λ tipado .

Definición

Una categoría C se denomina cerrada cartesiana [1] si cumple tres condiciones:

• C tiene un objeto terminal ;
• dos objetos cualesquiera X , Y en C tienen el producto X × Y ;
• Cualquier dos objetos Y , Z en C tienen exponencial Z Y .

Una categoría tal que para cualquiera de sus objetos la categoría de objetos sobre ella es cartesiana cerrada se denomina localmente cartesiana cerrada .

Ejemplos de categorías cerradas cartesianas

• La categoría de conjuntos es naturalmente una categoría cerrada cartesiana, ya que las funciones de un conjunto a otro son un conjunto y, por lo tanto, un objeto. También contiene productos (productos cartesianos ) y objetos terminales: singletons .

• La categoría Cat de todas las categorías pequeñas (y funtores como morfismos) es cartesiana cerrada; la exponencial C D  es la categoría de funtores de D a C con transformaciones naturales como morfismos. También hay una categoría de producto y un objeto terminal: categoría 1 de un objeto y un morfismo.

• Un topos elemental es una categoría cerrada cartesiana por definición.

• El álgebra de Heyting es también un  ejemplo estándar de una categoría cerrada cartesiana. Dado que el álgebra booleana es un caso especial, también es siempre cerrado cartesiano.

Aplicación

En una categoría cerrada cartesiana, una "función de dos variables" (morfismo f : X × Y → Z ) siempre se puede representar como una "función de una variable" (morfismo λ f : X → Z Y ). En programación, esta operación se conoce como curry ; esto permite que el cálculo lambda simplemente tipeado se interprete en cualquier categoría cerrada cartesiana. Las categorías cerradas cartesianas sirven como modelo de categoría para el cálculo tipificado y la lógica combinatoria .

La correspondencia de Curry-Howard proporciona un isomorfismo entre la lógica intuicionista, el cálculo lambda simplemente tipificado y las categorías cerradas cartesianas. Ciertas categorías cartesianas cerradas ( topoi ) se han propuesto como los principales objetos de fundamentos alternativos de las matemáticas en lugar de la teoría de conjuntos tradicional .

Notas

1. ↑ McLane S. Capítulo 4. Funtores adjuntos // Categorías para el matemático en activo / Per. De inglés. edición V. A. Artamonova. - M. : Fizmatlit, 2004. - S. 95-128. — 352 págs. — ISBN 5-9221-0400-4 .

Literatura

• Curien P.-L. Lógica combinatoria categórica.-- LNCS, 194, 1985, pp.~139-151.
• Roy L. Crole , Categorías de tipos, Cambridge University Press, 1994.