La pregunta es si es posible modelar en lógica lineal dos modos de acceso a un recurso. Sé que son posibles dos modos de recursos, es decir:
r está infinitamente disponible r solo está disponible una vez
Pero, ¿y si no quiero decidir si r es infinita o solo una vez disponible? Y la consulta, es decir, el acceso, debe decidir, entonces:
r solo está marcado (¡como si fuera! r) r se consume (como si fuera r solo)
¿Puedo modelar un consumo (r) y un acceso r normal en lógica lineal? Del mismo modo, me gustaría tener el operador produce (r), que luego afirma la forma * r de un recurso.
lo.logic
linear-logic
Kaveh
fuente
fuente
Respuestas:
Con la lógica lineal no conmutativa (véase Retoré 1997, para la lógica de pomset), puede modelar la secuencialidad de la verificación de recursos y evitar que la verificación de recursos ocurra dentro del alcance del operador de elección que desee utilizar.
Por ejemplo, podría modelar su consulta para que:
Puede interpretar esto como diciendo: si puedo tomar y luego consumir , entonces puedo proporcionar y luego libre . ¿Esa es la semántica que quieres?r a∨b c r
Desafortunadamente, parece que no se puede combinar la lógica lineal no conmutativa con la lógica lineal habitual en el cálculo posterior y mantener las propiedades teóricas de prueba necesarias para planificar el modelo mediante la búsqueda de pruebas. Puede hacer esto es el cálculo de estructuras, ver (Strassburger, 2003), que se ha utilizado para la planificación (Kahramanogullari 2009).
Si desea seguir la ruta de tener una modalidad de decoración solo , bueno, eso podría ser complicado porque esencialmente desea poder mirar sin consumirlo y sin tenerlo disponible para un uso ilimitado, lo cual no es una actitud proposicional de lógica lineal regular. Puedes intentar ver sit r
funciona para usted, pero probablemente no, porque es más barato que : es un poco como tener una referencia ; y, por lo tanto, no garantiza que pueda poner sus manos en . podría funcionar mejor, y es la base de las dos codificaciones utilizadas para modelar la lógica clásica en lógica lineal, pero tener no significa que pueda proporcionar . Mirar uno de los diversos exponenciales débiles para la lógica lineal podría ayudar aquí.?r r r r ?!r r ?!r
Referencias
fuente