J'essaie de comprendre la logique linéaire pour mieux comprendre les systèmes de type linéaire. Cependant, quand je lis les règles, je ne parviens pas à avoir une intuition comme je l'ai fait dans la logique modale - signifie A est requis comme dans les cadres Kripke A est requis pour chaque monde accessible [ ◊ A est A est mutatis possible mutandis]. Mais je ne trouve aucune explication intuitive de la dualité et laquelle des paires conjonction / disjonction (le cas échéant) correspond à ∧ et ∨ .
lo.logic
type-theory
linear-logic
Maciej Piechotka
la source
la source
Réponses:
Je ne suis pas sûr que cette question soit idéale pour CSTheory, mais étant donné qu'elle recueille déjà des votes positifs, voici une réponse que quelqu'un aurait pu donner si la question avait été publiée sur cs.stackexchange .
Dans cette lecture est le processus qui communique avec .A⊥⅋B⊥ A⊗B
L'équivalent de disjonction de la logique linéaire peut recevoir une lecture similaire de la théorie des processus. La formule
devrait également être considéré comme deux processus et en parallèle, mais plutôt que d'envoyer activement des messages, ils attendent que l'environnement décide lequel exécuter. Donc est assis là, attendant sur son canal pour un bit d'information qui décide si devrait fonctionner comme ou . Il s'agit d'une version «parallèle» de dans les langages de programmation séquentiels. Le dual de estA B A&B A&B A B if/then/else (A&B)⊥ A&B
peut être vu comme un processus envoyant 1 bit d'information à , à savoir: "continuer comme " ou "continuer comme ". Ceci est similaire à dans évaluant à tandis que évaluant à , sauf que le choix entre et est maintenant fait par l'environnement.A&B A B if true then P else Q P if false then P else Q Q A B
L'opérateur! A également une interprétation théorique du processus: si est lu comme un processus, alors peut être lu comme exécutant une infinité de processus en parallèle.Dans cette lecture , les axiomes la logique linéaire deviennent des « fils » de simples messages avant de processus aux processus . Cette interprétation des axiomes est déjà dans les réseaux de preuve de Girard (3).A⊢A A⊥ A
Cette interprétation théorique du processus a été influente et a donné lieu à de nombreux travaux de suivi comme par exemple (2) pour les types de session. Néanmoins, il y a quelques cas de bord qui le rendent un peu gênant, et à ma connaissance, il n'a pas été conçu pour fonctionner parfaitement pour une logique linéaire complète , même en 2017.
1. S. Abramsky, Interprétations computationnelles de la logique linéaire .
2. P. Wadler, Propositions as sessions .
3. Wikipédia, filet de preuve .
la source