¿Qué es la intuición detrás de la "par" operador en la lógica lineal?

Question

Estoy $\DeclareMathOperator{\par}{\unicode{8523}}$ tratando de envolver mi mente alrededor de la $\par$ ("par") operador de la lógica lineal.

Las otras conectivas han de recursos simples interpretaciones ($A\otimes B$ es "tienes tanto $A$ y $B$", $A\&B$ es "usted puede tener cualquiera de las $A$ o $B$", etc.).

Pero a pesar de las reglas de inferencia simple, he visto sólo menciona que $A\par B$ es "difícil de describir", en una interpretación de recursos, aparte del caso especial de $A\multimap B ~\equiv ~ A^\bot \par B$ ("usted puede convertir $A$$B$").

De cualquier manera, puedo entenderlo mejor?

Answer 1

⅋ también me tenía desconcertado por un largo tiempo. La intuición la que he llegado es esta: tiene una a y una B, pero no se pueden utilizar juntos.

Ejemplos de esto (consideradas como entidades en un programa de ordenador) incluyen:

• Un⊸A (= $A⅋A^⊥$) es un valor de la función; usted no puede deshacerse de él mediante la conexión de su entrada a su salida.
• $A⅋A^⊥$ es un canal de comunicación (futuro): usted puede poner un valor en uno de los extremos y a recuperar de los otros. Está prohibido, sin embargo, para hacer tanto desde el mismo hilo (riesgo de interbloqueo, que conduce a ⊥).

(El programa de ordenador analogía puede no tener sentido para todo el mundo, pero esta ha sido mi enfoque del tema, y mi base de intuiciones.)

Usted puede leer los axiomas en un arriba-derecha-abajo de la forma. El axioma de ⅋ introducción,

$$ \frac{ Δ_1,Un ⊢ Γ_1 \quad Δ_2,B ⊢ Γ_2 }{ Δ_1,Δ_2, Un⅋B \ ⊢ \ Γ_1,Γ_2 } $$

por lo tanto se puede leer como "dado un valor de Un tipo de⅋B, usted puede dividir los recursos restantes en dos, las transforman en otras nuevas, y se combinan los resultados." Y Un⅋B no puede ser dividido en cualquier otra forma - a y B debe convertirse en independiente y no puede tomar parte en las mismas transformaciones.

Answer 2

Por favor, consulte la Lógica Lineal en la wikipedia: el símbolo ⅋ ("par") se utiliza para denotar multipicative disyunción, mientras que ⊗ es utilizado para denotar el conjunto multiplicativo. Son duales de cada uno de los otros. También hay algo de debate de este conectivo.

De diversas maneras, uno puede denotar el "par" operación mediante el símbolo $ \sqcup $, el cual se describe en el documento (pdf) "la Lógica Lineal Muestra" como "unirse".

Las reglas lógicas para ⊗ y ⅋ son como sigue:

Si Γ: a: B Δ ⊢Θ, entonces Γ: A⊗B: Δ ⊢ Θ; por el contrario, si Γ ⊢ Δ: Una y ⊢ B: Θ, entonces Γ ⊢ Δ: A⊗B: Θ.

Dualmente, si Γ ⊢ Δ: a: B: Θ, entonces Γ ⊢ Δ: Un⅋B: Θ; por el contrario, si Un: Γ ⊢Δ y Θ: B ⊢, entonces Θ: Un⅋B: Γ ⊢ Δ.

La multiplicación distribuye sobre la suma si uno es una conjunción y una es una disyunción:

• Un⊗(B⊕C) ≡ (A⊗B)⊕(A⊗C) (y en el otro lado);

  (multiplicativo junto distribuye más de aditivo disyunción)

• Un⅋(B&C) ≡ (A⅋B)&(A⅋C) (y en el otro lado);

  (multiplicativo disyunción sobre aditivos conjunción)

También:

• Un⊗$0$ ≡ $0$ (y en el otro lado);
• Un⅋⊤≡⊤ (y en el otro lado).

Lineal implicación $A\multimap B$ corresponde a los hom interno, el cual puede ser definido como (a⊗$B^⊥)^⊥$. Hay una de Morgan doble de la del tensor de la llamada 'par', con Un⅋B=($A^⊥⊗B^⊥)^⊥$. Tensor y par son la 'multiplicación' conectivas, que a grandes rasgos representan el paralelo de la disponibilidad de recursos.

El "aditivo" conectivas & y ⊕, que corresponden en otra forma tradicional de la conjunción y la disyunción, se modelan como de costumbre por los productos y co-productos.

Para una buena exploración en la lógica lineal: ver esto:

---

(JUEGO SEMÁNTICA):

Juego semántica para la lógica lineal fue propuesto por primera vez por Andreas Blass (Blass (1992).) La semántica de aquí puede o no puede ser el mismo que el propuesto por Blass.

Podemos interpretar cualquier proposición lógica lineal como un juego entre dos jugadores: nosotros y ellos. Las normas generales son perfectamente simétricos entre nosotros y ellos, aunque no juego individual es. En cualquier momento dado en un juego, exactamente una de estas cuatro situaciones se obtiene: es nuestro turno, es su turno, que hemos ganado, o que han ganado; los dos últimos estados de continuar para siempre después (y el juego). Si es nuestro turno, entonces ellos están ganando; si es su turno, entonces estamos ganando. Así que hay dos formas de ganar: porque el juego es más (y un ganador se ha decidido), o porque es siempre la de otros jugadores de vuelta (ya sea porque no tienen mover, o porque cada movimiento que resulta en su sigue siendo su turno).

Esto es un poco complicado, pero es importante con el fin de ser capaz de distinguir las cuatro constantes:

En ⊤, es su turno, pero no se mueve; el juego no termina nunca, pero ganamos.

Doblemente, en 0, es nuestro turno, pero no nos mueve; el juego nunca termina, pero ellos ganan.

En contraste, en la 1, el juego termina inmediatamente, y hemos ganado.

Doblemente, en ⊥, el juego termina inmediatamente, y ellos han ganado.

Los operadores binarios mostrar cómo combinar los dos juegos en un mayor juego:

En A&B, es su turno, y se debe elegir para jugar, ya sea a o B. Una vez que hacen su elección, el juego continúa en el juego elegido, con final y las condiciones para ganar como en ese juego.

Doblemente, en Una⊕B, es nuestro turno, y debemos elegir para jugar ya sea en Una o B. una Vez que hagamos nuestra elección, el juego continúa en el juego elegido, con final y las condiciones para ganar como en ese juego.

En Un⊗B, el juego continúa con los dos partidos en paralelo. Si es nuestro turno en cualquiera de los juegos, entonces es nuestro turno general; si es su turno en ambos juegos, entonces es su turno general. Si el juego termina, entonces el juego continúa en el otro juego; si los dos juegos de la final, a continuación, en general el juego termina. Si hemos ganado los dos partidos, luego de haber ganado en general; si ellos han ganado cualquiera de los juegos, luego de haber ganado en general.

Doblemente, en Un⅋B, el juego continúa con los dos partidos en paralelo. Si es su turno en cualquiera de los juegos, entonces es su turno general; si es nuestra gire en ambos juegos, entonces es nuestro turno general. Si el juego termina, el juego continúa en el otro juego; si los dos juegos de la final, entonces la en general el juego termina. En caso de haber ganado los dos partidos, luego de haber ganado en general, si hemos ganado cualquiera de los juegos, luego de haber ganado en general.

Así, podemos clasificar las cosas de la siguiente manera:

En una conjunción, que elegir qué tipo de juego; en una disyunción, nos tiene el control. Quien tiene el control debe ganar al menos un juego para ganar en general.

En una adición, un juego debe ser jugado; en una multiplicación, todos los los juegos deben ser jugados.

Para aclarar la diferencia entre ⊤ y 1 (el aditivo y multiplicativa versiones de la verdad, ambos de los cuales ganamos); considerar la posibilidad de Un⅋⊤ y Un⅋1. En Un⅋⊤, es siempre su movimiento (ya que es su movimiento en ⊤, por lo tanto su movimiento en al menos un juego), así que ganar como ganamos ⊤. (De hecho, Un⅋⊤≡⊤.) Sin embargo, en Un⅋1, el juego 1 termina inmediatamente, por lo que el juego continúa como en A. Hemos ganado 1, por lo que sólo tenemos que terminar el juego para ganar en la general, pero no hay ninguna garantía de que esto suceda. De hecho, en 0⅋1, el juego nunca termina y siempre es nuestro turno, por lo que de ganar. (En ⊥⅋1, ambos juegos termina inmediatamente, y ganamos. En Un⊗1, debemos de ganar los dos partidos para ganar la general, por lo que esto se reduce a Una; de hecho, Un⊗1≡A.)

La negación es fácil: Para jugar Un ⊥, simplemente cambiar los roles y el juego A.

Un juego es válido si tenemos una estrategia para ganar (ya sea poniendo el juego en un estado donde hemos ganado o garantizando que es para siempre su turno). La solidez y la integridad de este la interpretación es el teorema que es un juego válido si y sólo si ⊢Un es válido el secuente. (Recordar que todas las cuestiones de validez de sequents puede ser reducido a la validez de una sola proposición.)

Answer 3

[No sé cómo hacer que la lógica lineal de símbolos aquí, perdona mi ineptitud].

Cuando estaba haciendo la investigación en la interacción de las redes y de la lógica lineal, mi intuición personal para las conectivas fue a través de un tradicional Hintikka juego semántica (pienso diferente de Blass).

Para mí, Un⅋B puede interpretarse en el sentido de que "Dada la refutación de Una, puedo demostrar B y dado una refutación de B I puede demostrar que Una".

Esto tiene algunas características interesantes: en primer lugar, se lleva a cabo la multiplicación de la naturaleza de la conectivo (la "y" en el medio) y la segunda es claro por qué Un⅋Un⊥ es cierto. Claro que si me dan una refutación de Un refutar A. no Hay nada que no sea constructivo al respecto. La tercera no requieren el uso de la ejecución en paralelo (aunque, por supuesto, eso puede ser una ventaja).

En mi interpretación tensor significa "puedo probar Una y puedo probar que B".

En el de arriba "demostrar" que significa "ganar como verificador" y si no hay un contexto que incluye el supuesto de que puedo usar el contexto linealmente. Por ejemplo, si hay Una a en el contexto de la voy a utilizar exactamente una vez.

No recuerdo que nadie haya explicando las conectivas de esa manera precisamente, pero puede ser equivalente a la de alguna otra formulación.

EDITAR Henning es correcto, creo que la mejor forma de decirlo es "un refutación de Una, puedo demostrar B o dado una refutación de B I puede demostrar que Una".

Par es una afirmación de que ambas opciones son posibles y no se compromete a cualquiera, pero el que rodea a prueba de contexto puede seleccionar uno o el otro.

Answer 4

Me permite contribuir otro intuitiva interpretación de recursos a lo largo de las líneas de eriksoe.

Todo fórmula en la lógica lineal, incluyendo la $\par$$\bot$, se puede pensar en una máquina que las solicitudes de entrada, a continuación, proporciona una salida, las solicitudes de entrada de nuevo, y así sucesivamente. Para la más fácil interpretación que he pensado hasta ahora es una "máquina expendedora de interpretación".

Deje $S$ denotar una máquina expendedora que se lleva a siclos y dispensa aperitivos, y $D$ denotar una máquina expendedora que toma dólares y dispensa bebidas. El tradicional recurso de interpretación de la lógica lineal funciona perfectamente bien aquí. La máquina expendedora $S \& D$ es "su elección entre el$S$$D$": puede convertirse en un $S$ o $D$, como ustedes quieran, pero no tanto. La máquina expendedora $S \oplus D$"$S$$D$, y no es hasta usted"; la máquina podría llegar a prescindir de sólo bocadillos, o se podría llegar a prescindir de sólo bebidas.

La máquina expendedora $S \otimes D$ "de las máquinas expendedoras $S$$D$". Es una máquina expendedora que tiene dos dinero ranuras y dos dispensadores; usted puede poner un siclo en el siclo de la ranura y obtener un bocadillo de la merienda dispensador, o usted puede poner un dólar a dólar ranura y obtener una bebida de la bebida dispensador, o usted puede hacer ambas cosas, o ninguna, cualquier número de veces, en cualquier orden.

Y, a continuación, la máquina expendedora $S \par D$ es un poco más complicado, pero no demasiado. Se trata de una máquina expendedora que tiene dos dinero ranuras y dos dispensadores, de tal manera que uno de los dinero slots ya ha sido usado, pero el correspondiente elemento de la comida no se ha dispensado todavía. Sólo puede utilizar esta máquina expendedora mediante la inserción de dinero en cualquier ranura no se ha utilizado todavía. La máquina expendedora entonces prescindir de un aperitivo o una bebida, como los deseos. Si se prescinde de un aperitivo, luego de la demanda de un siclo siguiente; si se prescinde de una bebida, entonces la demanda de un dólar siguiente.

Esto proporciona un poco de explicación de la $\par$ a la izquierda de la introducción de la regla, que, como eriksoe señala, puede ser leído en el sentido de que puede dividir los recursos restantes en dos y utilizar algunos de los recursos con cada lado de la $\par$. Supongamos que tiene una persona con mucho hambre y mucha sed persona. Usted puede dar a la persona que tiene hambre y un montón de siclos, y la sed persona montón de dólares, y directa a cada uno hacia el lado correspondiente de la máquina expendedora. Tanto la gente será feliz, porque desde su punto de vista, la máquina se comporta como se esperaba: en algunos moneda, y la máquina (eventualmente) suministra el alimento. Sin embargo, las dos personas no serán capaces de comercio con cada uno de los otros, porque uno de ellos será siempre demasiado ocupado, esperando la máquina expendedora para prestar atención a la otra persona.

La máquina expendedora de interpretación para $\bot$ es que es una máquina expendedora con un botón que puede pulsar (gratis) exactamente una vez, y luego es incapaz de prescindir de nada. La máquina expendedora $S \par \bot$ se comporta de manera efectiva de la misma manera como $S$, ya que sólo se podrá prescindir de aperitivos, y después de la merienda, se dispensa, siempre de la demanda de un siclo, en lugar de un pulsador. (Se puede exigir un botón de empuje, pero sólo una vez, en el comienzo mismo de su existencia.)