<foo> simply produces <foo>in the text).
<URL: http://somewhere.tld/ >,
and it will be automatically made into a link.
(Do not try any other way or it might count as an attempt to spam.)mailto: URI,
e.g. mailto:my.email@somewhere.tld,
if you do not have a genuine Web site).
Tito (2022-11-03T17:19:00Z)
Pour répondre à « J'avoue ne guère avoir d'idée de ce qu'il [Girard] voulait faire avec [la logique linéaire] » : en fait, dans les années 1980, Girard a inventé une sémantique du λ-calcul simplement typé (i.e. de la logique intuitionniste propositionnelle) dans les « espaces cohérents », et en analysant l'interprétation des connecteurs là-dedans il s'est rendu compte qu'il y avait des décompositions A ∨ B = !A ⊕ !B et A ⇒ B = !A ⊸ B. Donc il a d'abord découvert les opérations !,⊕,⊸ dans une sémantique, puis ensuite il les a réifié dans une syntaxe pour pouvoir décomposer son interprétation du λ-calcul en traduction intuitionniste→linéaire + sémantique de la LL dans les espaces cohérents. Tout cela est raconté dans la section V du papier Linear Logic de 1987, qui est tout à fait lisible (à l'époque il parlait beaucoup moins de brocolis…).
Pour cette raison je trouve d'ailleurs assez injuste le jugement émis sur les catégories *-autonomes dans un commentaire précédent. Déjà, elles ont été définies par des catégoriciens avant l'apparition de la logique linéaire. Mais en plus, elles ont une tendance à surgir naturellement en sémantique des langages de programmation, c'est ça qui a mené à la naissance de la LL et le phénomène s'est reproduit pas mal de fois après. Cela dit, c'est vrai que ces sémantiques ne sont en général pas « fully complete » pour la LL, il y a toujours des choses en plus.
Au passage, la méthodologie « examiner la structure présente dans des sémantiques pour en faire une syntaxe » est assez fructueuse, elle a aussi produit le λ-calcul différentiel et la théorie homotopique des types.
(Précision : les espaces cohérents font partie de la théorie des domaines à la française (Berry, Curien, Ehrhard, …) où les morphismes entre domaines sont stables en plus d'être Scott-continus, même si Girard ignorait à l'origine les domaines stables de Berry et s'inspirait de ses propres travaux précédents sur les ordinaux — ceux pour lesquels il a eu la médaille d'argent du CNRS. D'ailleurs Girard crache souvent sur les domaines de Scott parce que ce serait de la « fausse topologie ».)
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 ?