En la lógica lineal (LL), es indemostrable pero al considerar la interpretación de los recursos me parece que de los recursos $A, B$ podemos producir los recursos $A, B$ .
Por $A, B \vdash A, B$ Es decir $A \otimes B \vdash A \wp B$
Respuesta
¿Demasiados anuncios?
Boris Eng
Puntos
20
Según ¿Cuál es la intuición detrás del operador "par" en la lógica lineal? que parece ser una interpretación bastante coherente y agradable.
Desde $A_1, ..., A_n \vdash B_1, ..., B_n$ es $A_1 \otimes ... \otimes A_n \vdash B_1 \wp ... \wp B_n$
- La parte izquierda $\vdash$ debe verse como un espacio de recursos que tenemos y podemos utilizar simultáneamente.
- La parte derecha de $\vdash$ debe verse como un espacio de recursos que no podemos utilizar simultáneamente.
Cuando se utiliza la formulación monolateral $\vdash A, A^\bot$ de $A \vdash A$ para conseguir $\vdash A_1^\bot \wp ... \wp A_n^\bot, B_1 \wp ... \wp B_n$ podemos ver claramente que no podemos utilizar simultáneamente los recursos en la parte derecha de $\vdash$ . Consideremos que la regla del axioma es una forma de "activar" el proceso de consumo.
Dado que los recursos de la derecha no pueden ser utilizados simultáneamente (viven en paralelo), no podemos conectar las ocurrencias por consumo por lo que el secuente se vuelve indemostrable.
