Comments on Et maintenant, un peu de logique linéaire

wpom (2019-01-26T02:04:09Z)

Je me demandais si on ne pouvait pas faire ça de la manière suivante:
https://pastebin.com/Fty6KwtW

Gaston Rachlou (2019-01-18T16:13:40Z)

A propos des brocolis, on peut conjecturer que Girard a été un grand lecteur des bandes dessinées de Marcel Gotlib, où ce légume (plutôt rare dans les années 60 et 70, les grandes années de Gotlib) joue un rôle secondaire, mais récurrent.

Ruxor (2019-01-15T21:33:15Z)

@jonas: Concerning your first question, I would say that the "resource" interpretation of linear logic is only vaguely define, and any attempt at making it formal will likely evolve into the game semantics; this is more or less what <URL: http://www.math.lsa.umich.edu/~ablass/llgames.pdf > (≡<URL: http://arxiv.org/abs/math/9310211 >) argues (or at least, what I make of it). Concerning your second question: when degenerated to classical logic, the game semantics of linear logic become a classical game of prover-refuter, in which the game A∧B means the refuter chooses either A or B as a challenge to the prover (and the game continues in this component) whereas the game A∨B means the prover chooses either A or B (and the game continues in this component), ⊤ means the prover wins immediately, ⊥ means the refuter wins immediately, and so on. (This is also related to the so-called "Dialectica interpretation" of logic, although I must admit the subtle differences between a number of superficially similar looking but confusingly different games or logical interpretations tend to escape me.)

ooten (2019-01-15T20:13:58Z)

Je vous conseille aussi d'aller sur la Page Oueb de Jean-Yves Girard <URL: http://girard.perso.math.cnrs.fr/Accueil.html >. Ca a l'air passionnant, j'ai l'impression qu'il essaye de rendre sa discipline accessible autant que possible (en agitant les mains) en ayant une vue globale de sa discipline. Sinon ton post est très réussi, Ruxor, il est synthétique et c'est une très bonne entrée pour essayer de comprendre de quoi il s'agit. :-)

jonas (2019-01-15T18:29:04Z)

I have a question about the partial interpretations of linear logic that you mention here. Is the interpretation as two-player combinatorial games essentially just a special case of the interpretation as producing and consuming resources? Is the restriction to classical (zeroth order) logic essentially a special case of the interpretation as two-player games?

Ruxor (2019-01-15T13:05:34Z)

@Dam's: Un peu, mais c'est plutôt décevant.

Pour la négation/dualité, le concept pertinent est celui de catégorie *-autonome, <URL: http://en.wikipedia.org/wiki/*-autonomous_category >, mais il est bigrement pénible d'en trouver[#], il n'y a pas l'air d'y en avoir de très naturelle (parce que les bidualités en mathématiques n'ont pas trop tendance à être l'identité), et j'ai l'impression qu'au final on ne fait que réécrire les règles de la logique linéaire en disant « oui, on pourrait regarder une catégorie qui vérifie ça », ce qui n'est pas franchement passionnant.

Pour ce qui est d'un analogue des topoi pour la logique linéaire, il me semble qu'il y a plein de problèmes à avoir un classificateur de sous-objet. Mon intuition est que la logique linéaire est globalement assez hostile à la notion même de valeur de vérité (qui est quand même ce qui sous-tend le classificateur de sous-objet d'un topos). En fait, je ne suis même pas persuadé qu'on sache faire une logique du second ordre satisfaisante sur la logique linéaire : un problème notamment est que si tu veux voir ∀ comme une conjonction paramétrique interne, ce sera un &, et si tu veux faire un ⊗ paramétrique interne tu ouvres les portes de toutes les souffrances du monde. Je serais ravi to be proved wrong.

[#] J'ai gribouillé quelque part l'exemple qui suit : soit k un anneau commutatif, D un k-module, et Chu(k-Mod,D) la catégorie dont les objets sont les triplets (V₁,V₂,v) où v:V₁×V₂→D est bilinéaire et dont les morphismes de (V₁,V₂,v) vers (W₁,W₂,w) sont les données de f:V₁→W₁ et g:W₂→V₂ tels que v(x,g(y))=w(f(x),y) pour tous x et y ; le dual de (V₁,V₂,v) est évidemment (V₂,V₁,v′) où v′(x,y)=v(y,x) ; la seule subtilité est de définir (V₁,V₂,v)⊗(W₁,W₂,w) (tout le reste est facile) : c'est (U₁,U₂,u) où U₁ est le produit tensoriel de V₁ et W₁ sur k, tandis que U₂ est la rétrotirette de Hom(V₁,W₂) et Hom(W₁,V₂) au-dessus de Hom(U₁,D), c'est-à-dire le module des couples (a,b) avec a:V₁→W₂ et b:W₁→V₂ (deux applications k-linéaires) telles que v(x,b(y))=w(a(x),y), et u:U₁×U₂→D est évidemment défini par u(x⊗y,(a,b)) = cette valeur. (On peut améliorer cet exemple en considérant les objets « séparés », qui sont ceux (V₁,V₂,v) pour lesquels le noyau gauche et le noyau droite de v sont triviaux. Mais il y a alors des hypothèses à mettre sur le schmilblick, et je ne sais pas les détails.)

Dam's (2019-01-15T12:12:55Z)

Moi ce qui m'intéresserait ça serait de mieux comprendre le lien entre la logique linéaire et son interprétation comme "la logique interne aux catégories monoidales symmétriques". De ce que je vois sur google, on a une interprétation de la logique linéaire intuitioniste dans des catégories monoidales symmétriques closes munies d'une comonade monoidale symmétrique, cf par exemple
https://hal.archives-ouvertes.fr/hal-00154229/document

Est-ce que tu as regardé ce genre de choses? Et comment interprèter la négation? Est-ce qu'on a une notion de "topos linéaire", qui serait l'équivalent pour la logique linéaire de ce qu'un topos est pour la logique intuitioniste?

Ruxor (2019-01-13T21:37:43Z)

@Typhon: Il y a peut-être plus intelligent à dire, mais on doit pouvoir formaliser ça en introduisant des termes V(x) (« je dispose de la valeur x »), des axiomes !((V(x)⊗V(y))⊸V(x+y)), !((V(x)⊗V(y))⊸V(x−y)), !((V(x)⊗V(y))⊸V(x×y)) et pareil pour toutes les autres opérations qu'on a le droit d'effectuer, et on cherche à démontrer quelque chose comme (V(x_1)⊗…⊗V(x_n))⊸V(z) où x_1,…,x_n sont les valeurs dont on dispose et z celle qu'on cherche à atteindre.

Typhon (2019-01-13T20:48:55Z)

En lisant le début de cette entrée je me suis rendu compte qu'il y avait une analogie frappante entre la logique linéaire où on utilise une et une seule fois les hypothèses et le jeu "Le Compte est bon" (= la partie "chiffres" de l'émission télévisée "des chiffres et des lettres") où on ne peut faire apparaître qu'une fois les nombres indiqués sur les plaques dans les calculs.

Peut-on décrire ce jeu en utilisant la logique linéaire ?

Bertrand Renard et Laurent Romejko encourent-ils un procès de la part de J-Y Girard ?

France Télévision a-t-elle tenté de préparer les français à l'avènement de la logique linéaire depuis toutes ces années ?


You can post a comment using the following fields:
Name or nick (mandatory):
Web site URL (optional):
Email address (optional, will not appear):
Identifier phrase (optional, see below):
Attempt to remember the values above?
The comment itself (mandatory):

Optional message for moderator (hidden to others):

Spam protection: please enter below the following signs in reverse order: ef6210


Recent comments