Estoy tratando de entender la lógica lineal para comprender mejor los sistemas de tipo lineal. Sin embargo, cuando leí las reglas, no llego a tener una intuición detrás de él como lo he hecho en la lógica modal - significa un se requiere como en los marcos de Kripke A es necesaria para todos los mundos accesibles [ ◊ A es A es posible , mutatis mutandis]. Pero no puedo encontrar ninguna explicación intuitiva para la dualidad y cuál de los pares de conjunción / disyunción (si corresponde) corresponde a ∧ y ∨ .
lo.logic
type-theory
linear-logic
Maciej Piechotka
fuente
fuente
Respuestas:
No estoy seguro de que esta pregunta sea ideal para CSTheory, pero dado que ya está reuniendo votos a favor, aquí hay una respuesta que alguien podría haber dado si la pregunta se hubiera publicado en cs.stackexchange .
En esta lectura es el proceso que se comunica con .A⊥⅋B⊥ A⊗B
El equivalente de la disyunción de la lógica lineal puede recibir una lectura teórica de proceso similar. La formula
También debe verse como dos procesos y en paralelo, pero en lugar de enviar mensajes activamente, esperan que el entorno decida qué ejecutar. Así que se sienta allí, esperando en su canal para un bit de información que decide si debe funcionar como o como . Esta es una versión 'paralela' del en lenguajes secuenciales de programación. El dual de esA B A&B A&B A B if/then/else (A&B)⊥ A&B
puede verse como un proceso que envía 1 bit de información a , a saber: "continuar como " o "continuar como ". Esto es similar a evaluando a mientras evaluando a , excepto que la elección entre y ahora es hecha por el entorno.A&B A B if true then P else Q P if false then P else Q Q A B
El operador! También tiene una interpretación teórica del proceso: si se lee como un proceso, entonces se puede leer como ejecutando infinitos procesos en paralelo.En esta lectura el axiomas de la lógica convertido en simples 'cables' lineales que reenviar mensajes de procesos a procesos . Esta interpretación de los axiomas ya está en las redes de prueba de Girard (3).A⊢A A⊥ A
Esta interpretación teórica del proceso ha sido influyente y ha dado lugar a una gran cantidad de trabajo de seguimiento como, por ejemplo, (2) para los tipos de sesión. Sin embargo, hay algunos casos extremos que lo hacen un poco incómodo, y que yo sepa, no se ha hecho que funcione perfectamente para una lógica lineal completa incluso en 2017.
1. S. Abramsky, Interpretaciones computacionales de la lógica lineal .
2. P. Wadler, Propuestas como sesiones .
3. Wikipedia, Prueba de red .
fuente