Cálculo kappa

Subconjunto del cálculo lambda

En lógica matemática , teoría de categorías y ciencia informática , el cálculo kappa es un sistema formal para definir funciones de primer orden .

A diferencia del cálculo lambda , el cálculo kappa no tiene funciones de orden superior ; sus funciones no son objetos de primera clase . El cálculo kappa puede considerarse como "una reformulación del fragmento de primer orden del cálculo lambda tipificado". ^[1]

Debido a que sus funciones no son objetos de primera clase, la evaluación de expresiones de cálculo kappa no requiere cierres .

Definición

La definición que aparece a continuación ha sido adaptada de los diagramas de las páginas 205 y 207 de Hasegawa. ^[1]

Gramática

El cálculo kappa consta de tipos y expresiones, dados por la gramática siguiente:

${\displaystyle \tau =1\mid \tau \times \tau \mid \ldots }$

${\displaystyle e=x\mid id_{\tau }\mid !_{\tau }\mid \operatorname {lift} _{\tau }(e)\mid e\circ e\mid \kappa x:1{\to }\tau .e}$

En otras palabras,

• 1 es un tipo
• Si y son tipos entonces es un tipo. ${\displaystyle \tau _{1}}$ ${\displaystyle \tau _{2}}$ ${\displaystyle \tau _{1}\times \tau _{2}}$
• Cada variable es una expresión
• Si τ es un tipo entonces es una expresión ${\displaystyle id_{\tau }}$
• Si τ es un tipo entonces es una expresión ${\displaystyle !_{\tau }}$
• Si τ es un tipo y e es una expresión, entonces es una expresión ${\displaystyle \operatorname {lift} _{\tau }(e)}$
• Si y son expresiones entonces es una expresión ${\displaystyle e_{1}}$ ${\displaystyle e_{2}}$ ${\displaystyle e_{1}\circ e_{2}}$
• Si x es una variable, τ es un tipo y e es una expresión, entonces es una expresión ${\displaystyle \kappa x{:}1{\to }\tau \;.\;e}$

Los subíndices y de id , ! , y a veces se omiten cuando pueden determinarse de forma inequívoca a partir del contexto. ${\displaystyle :1{\to }\tau }$ ${\displaystyle \operatorname {lift} }$

La yuxtaposición se utiliza a menudo como abreviatura de una combinación y composición: ${\displaystyle \operatorname {lift} }$

${\displaystyle e_{1}e_{2}\ {\overset {\operatorname {def} }{=}}\ e_{1}\circ \operatorname {lift} (e_{2})}$

Reglas de mecanografía

En la presentación que se presenta aquí se utilizan secuencias ( ) en lugar de juicios hipotéticos para facilitar la comparación con el cálculo lambda de tipo simple. Esto requiere la regla Var adicional, que no aparece en Hasegawa ${\displaystyle \Gamma \vdash e:\tau }$^[1].

En el cálculo kappa, una expresión tiene dos tipos: el tipo de su fuente y el tipo de su destino . La notación se utiliza para indicar que la expresión e tiene tipo de fuente y tipo de destino . ${\displaystyle e:\tau _{1}{\to }\tau _{2}}$ ${\displaystyle {\tau _{1}}}$ ${\displaystyle {\tau _{2}}}$

A las expresiones en el cálculo kappa se les asignan tipos de acuerdo con las siguientes reglas:

En otras palabras,

• Var: suponiendo que te permite concluir que ${\displaystyle x:1{\to }\tau }$ ${\displaystyle x:1{\to }\tau }$
• Id: para cualquier tipo τ , ${\displaystyle id_{\tau }:\tau {\to }\tau }$
• Bang: para cualquier tipo τ , ${\displaystyle !_{\tau }:\tau {\to }1}$
• Comp: si el tipo de destino coincide con el tipo de origen, se pueden componer para formar una expresión con el tipo de origen y el tipo de destino. ${\displaystyle e_{1}}$ ${\displaystyle e_{2}}$ ${\displaystyle e_{2}\circ e_{1}}$ ${\displaystyle e_{1}}$ ${\displaystyle e_{2}}$
• Ascensor: si , entonces ${\displaystyle e:1{\to }\tau _{1}}$ ${\displaystyle \operatorname {lift} _{\tau _{2}}(e):\tau _{2}{\to }(\tau _{1}\times \tau _{2})}$
• Kappa: si podemos concluir que bajo el supuesto de que , entonces podemos concluir sin ese supuesto que ${\displaystyle e:\tau _{2}\to \tau _{3}}$ ${\displaystyle x:1{\to }\tau _{1}}$ ${\displaystyle \kappa x{:}1{\to }\tau _{1}\,.\,e\;:\;\tau _{1}\times \tau _{2}\to \tau _{3}}$

Igualdades

El cálculo kappa obedece a las siguientes igualdades:

• Neutralidad: Si entonces y ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$ ${\displaystyle f{\circ }id_{\tau _{1}}=f}$ ${\displaystyle f=id_{\tau _{2}}{\circ }f}$
• Asociatividad: Si , , y , entonces . ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$ ${\displaystyle g:\tau _{2}{\to }\tau _{3}}$ ${\displaystyle h:\tau _{3}{\to }\tau _{4}}$ ${\displaystyle (h{\circ }g){\circ }f=h{\circ }(g{\circ }f)}$
• Terminalidad: Si y entonces ${\displaystyle f{:}\tau {\to }1}$ ${\displaystyle g{:}\tau {\to }1}$ ${\displaystyle f=g}$
• Reducción de elevación: ${\displaystyle (\kappa x.f)\circ \operatorname {lift} _{\tau }(c)=f[c/x]}$
• Reducción kappa: si x no es libre en h ${\displaystyle \kappa x.(h\circ \operatorname {lift} _{\tau }(x))=h}$

Las dos últimas igualdades son reglas de reducción para el cálculo, reescribiéndose de izquierda a derecha.

Propiedades

El tipo1 puede considerarse como el tipo de unidad . Debido a esto, dos funciones cualesquiera cuyo tipo de argumento sea el mismo y cuyo tipo de resultado sea1 debe ser igual, ya que solo hay un único valor de tipo1 ambas funciones deben devolver ese valor para cada argumento ( Terminalidad ).

Las expresiones con tipo pueden considerarse como "constantes" o valores de "tipo básico"; esto se debe a que ${\displaystyle 1{\to }\tau }$1 es el tipo de unidad, por lo que una función de este tipo es necesariamente una función constante. Nótese que la regla kappa permite abstracciones solo cuando la variable que se está abstrayendo tiene el tipo de algún τ . Este es el mecanismo básico que garantiza que todas las funciones sean de primer orden. ${\displaystyle 1{\to }\tau }$

Semántica categórica

El cálculo kappa pretende ser el lenguaje interno de categorías contextualmente completas .

Ejemplos

Las expresiones con múltiples argumentos tienen tipos de origen que son árboles binarios "desequilibrados a la derecha". Por ejemplo, una función f con tres argumentos de tipos A, B y C y un tipo de resultado D tendrá tipo

${\displaystyle f:A\times (B\times (C\times 1))\to D}$

Si definimos la yuxtaposición asociativa por la izquierda como una abreviatura de , entonces, suponiendo que , y , podemos aplicar esta función: ${\displaystyle f\;c}$ ${\displaystyle (f\circ \operatorname {lift} (c))}$ ${\displaystyle a:1{\to }A}$ ${\displaystyle b:1{\to }B}$ ${\displaystyle c:1{\to }C}$

${\displaystyle f\;a\;b\;c\;:\;1\to D}$

Dado que la expresión tiene tipo de fuente ${\displaystyle f\;a\;b\;c}$1 , es un "valor base" y puede pasarse como argumento a otra función. Si , entonces ${\displaystyle g:(D\times E){\to }F}$

${\displaystyle g\;(f\;a\;b\;c)\;:\;E\to F}$

Al igual que una función currificada de tipo en el cálculo lambda, es posible una aplicación parcial: ${\displaystyle A{\to }(B{\to }(C{\to }D))}$

${\displaystyle f\;a\;:\;B\times (C\times 1)\to D}$

Sin embargo, no hay tipos superiores (es decir, ). Tenga en cuenta que debido a que el tipo de origen de fa no es ${\displaystyle (\tau {\to }\tau ){\to }\tau }$1 , la siguiente expresión no puede tipificarse correctamente bajo los supuestos mencionados hasta ahora:

${\displaystyle h\;(f\;a)}$

Debido a que la aplicación sucesiva se utiliza para múltiples argumentos, no es necesario conocer la aridad de una función para determinar su tipo; por ejemplo, si sabemos que entonces la expresión ${\displaystyle c:1{\to }C}$

yo c

está bien tipificado siempre que j tenga tipo

${\displaystyle (C\times \alpha ){\to }\beta }$para algunos α

y β . Esta propiedad es importante al calcular el tipo principal de una expresión, algo que puede resultar difícil cuando se intenta excluir funciones de orden superior de los cálculos lambda tipados restringiendo la gramática de los tipos.

Historia

Barendregt introdujo originalmente ^[2] el término "completitud funcional" en el contexto del álgebra combinatoria. El cálculo kappa surgió de los esfuerzos de Lambek ^[3] por formular un análogo apropiado de la completitud funcional para categorías arbitrarias (véase Hermida y Jacobs, ^[4] sección 1). Hasegawa desarrolló posteriormente el cálculo kappa en un lenguaje de programación utilizable (aunque simple) que incluye aritmética sobre números naturales y recursión primitiva. ^[1] Las conexiones con flechas fueron investigadas posteriormente ^[5] por Power, Thielecke y otros.

Variantes

Es posible explorar versiones del cálculo kappa con tipos subestructurales como lineales , afines y ordenados . Estas extensiones requieren eliminar o restringir la expresión. En tales circunstancias, el operador de tipo × no es un verdadero producto cartesiano y generalmente se escribe ⊗ para dejarlo en claro. ${\displaystyle !_{\tau }}$

Referencias

1. Hasegawa, Masahito (1995). "Descomposición del cálculo lambda tipado en un par de lenguajes de programación categóricos". En Pitt, David; Rydeheard, David E.; Johnstone, Peter (eds.). Category Theory and Computer Science . Apuntes de clase en informática. Vol. 953. Springer-Verlag Berlin Heidelberg. págs. 200–219. CiteSeerX 10.1.1.53.715 . doi :10.1007/3-540-60164-3_28. ISBN  978-3-540-60164-7. ISSN  0302-9743.
   • Adam (31 de agosto de 2010). "¿Qué son las categorías κappa?". MathOverflow .
2. Barendregt, Hendrik Pieter, ed. (1 de octubre de 1984). El cálculo lambda: su sintaxis y semántica. Estudios de lógica y fundamentos de las matemáticas. Vol. 103 (edición revisada). Ámsterdam, Holanda Septentrional: Elsevier Science. ISBN 978-0-444-87508-2.
3. Lambek, Joachim (1 de agosto de 1973). "Completitud funcional de categorías cartesianas". Annals of Mathematical Logic . 6 (3–4) (publicado en marzo de 1974): 259–292. doi :10.1016/0003-4843(74)90003-5. ISSN  0003-4843.
   • Adam (31 de agosto de 2010). "¿Qué son las categorías κappa?". MathOverflow .
4. Hermida, Claudio; Jacobs, Bart (diciembre de 1995). "Fibraciones con indeterminados: completitud contextual y funcional para cálculos lambda polimórficos". Estructuras matemáticas en informática . 5 (4): 501–531. doi :10.1017/S0960129500001213. ISSN  1469-8072. S2CID  3428512.
5. Poder, Juan; Thielecke, Hayo (1999). "Categorías cerradas Freyd y κ". En Wiedermann, Jiří; van Emde Boas, Peter ; Nielsen, Mogens (eds.). Autómatas, Lenguajes y Programación . Apuntes de conferencias sobre informática. vol. 1644. Springer-Verlag Berlín Heidelberg. págs. 625–634. CiteSeerX 10.1.1.42.2151 . doi :10.1007/3-540-48523-6_59. ISBN  978-3-540-66224-2. ISSN  0302-9743.