Según lo definido por Wikipedia,
(La correspondencia de Curry-Howard) es una generalización de una analogía sintáctica entre sistemas de lógica formal y cálculos computacionales que fue descubierta por primera vez por el matemático estadounidense Haskell Curry y el lógico William Alvin Howard.
Relacionado con él está el cubo λ, que es una representación gráfica de los posibles ejes de refinamiento desde tipos simples hasta el cálculo de construcciones, que tiene una interpretación lógica:
Hasta donde sé, la correspondencia de Curry-Howard es una conexión entre la teoría de tipos y la lógica clásica. Mi pregunta es: ¿hay alguna correspondencia analógica entre sistemas de tipos y lógicas lineales ?
logic
type-theory
functional-programming
MaiaVictor
fuente
fuente
Respuestas:
Puede imponer requisitos similares dentro de su sistema de tipos, lo que equivale a requerir que los objetos nunca se destruyan ni se dupliquen. Para ver un ejemplo de una aplicación práctica, vea Tipos lineales puede cambiar el mundo. por Philip Wadler, que especifica las reglas de escritura para esto. También muestra cómo un sistema de tipos puede combinar tipos lineales y no lineales.
Para una aplicación práctica de esto, eche un vistazo a
std::unique_ptr
C ++. Aquí, la linealidad asegura que la desasignación siempre ocurra exactamente una vez.En un lenguaje funcional, la linealidad también ofrece la posibilidad de actualizaciones destructivas (que parecen ser puras para el programador). Sin embargo, en la práctica parece que las mónadas son un enfoque más común para resolver este problema.
Actualización : me di cuenta de que en la tabla de trinitarismo computacional de NLab la ausencia de contracción en una lógica (es decir, no poder duplicar una suposición) corresponde al teorema de no clonación de la mecánica cuántica. (Desafortunadamente) no entiendo las implicaciones de esto, pero pensé que podría resultarle interesante.
fuente
La lógica lineal corresponde a un sistema de tipos para un cálculo de proceso (una variante del cálculo interno π ), donde:
Esta es un área de investigación bastante activa. Si bien la gente esperaba una correspondencia entre la lógica lineal y algún modelo de concurrencia desde el inicio de la lógica lineal por Girard [1987] , encontrar algo que sea satisfactorio tanto desde la perspectiva lógica como de la concurrencia ha sido algo difícil de alcanzar.
Aquí hay un resumen de los desarrollos clave hasta ahora.
Si está buscando un par de documentos para comenzar, comenzaría desde [Wadler, 2014] y luego [Kokke et al., 2019] (para ver el último sistema).
fuente