Discussion:Logique linéaire

Cet article est mauvais

Cet article est mauvais: il manque un paragraphe qui permet de comprendre ce que ce charabia apporte, grossièrement ce que cela apporte à la logique, et des exemples d'applications etc ..; Wikipedia peut mieux faire que ces encyclopédies dont les définitions ne peuvent être comprises que par ceux qui les connaissent déjà ... Zorgi c++

Il faut être plus constructif dans les critiques pour que les rédacteurs puissent en tirer parti. Cet article suppose que le lecteur ait lu et compris auparavant les articles sur la théorie de la démonstration. Ceci dit, l'article dit La logique linéaire promeut une vision géométrique des syntaxes formelles, c'est donc bien ce que la logique linéaire apporte à la logique. Je prends acte qu'il manque d'applications. En effet, bien que située très en amont, la logique linéaire a néanmoins des applications en programmation fonctionnelle et en linguistique. Pierre de Lyon 23 mai 2007 à 14:48 (CEST)

Je suis d'accord avec Zorgi : cet article est sans doute très bien fait pour une personne ayant de bonnes connaissances en logique et voulant se remémorer ce qu'est la logique linéaire, mais son caractère essentiellement formel le rend beaucoup trop abscons pour qu'il puisse prétendre être un article encyclopédique. La logique peut être aussi expliquée avec des mots, ce qui n'empêche d'ailleurs pas de mettre les systèmes formels pour que tous les publics puissent y trouver leur compte.

Par ailleurs, il serait bon que ce genre d'article soit un minimum pédagogique, et celui-ci ne l'est absolument pas : c'est un docte exposé ex cathedra d'un professeur parlant à ses pairs sans se soucier d'être compris. — Le message qui précède, non signé, a été déposé par 82.235.39.225 (discuter), le 27 juillet 2007 à 15:20

Bonjour, je (AFRN) reprend cette critique en 2012. Naturellement la logique linéaire est importante par ses implications.... Mais, mais, ...

Je vais essayer de dire ce que je ressent à la lecture de cet article en prenant un exemple: l'hypothétique article "Tasse":

"La tasse étend à partir du XVIIeme siècle français le concept de coupe, lui même généralisateur de celui de hanap. Elle est peinte par de nombreux peintres en natures mortes mais se trouve rarement le sujet principal en raison de présupposés esthétiques rarement explicités. La tasse permet aussi de stocker temporairement des liquides en particulier dans les réfrigérateurs, du moins à partir du XXème siècle. Jacques Lepape utilise le concept de tasse inversé à partir de 1953 pour en faire une particularisation de la cloche à fromage."

Même si tout est vrai, on ne te dit rien de CE QU'EST UNE TASSE , et l'article, bon ou mauvais est simplement inutile. Il en est de même de l'article "logique linéaire". Il faut expliciter ce qu'est la logique (aristotélicienne), puis expliciter ce qui manque pour l'utiliser dans certaines conditions. Il faut ensuite expliciter ensuite ce qu'est la logique linéaire et dire alors ce qu'elle permet de faire et que ne permettait pas la logique classique.

J'avoue être incapable de mener ce travail à bien. Mais je ne dirais pas que l'article "logique linéaire" est mauvais, c'est bien pire: il est en l'état superfétatoire et inutile. J'espère malgré la force de ma critique avoir donné des indications positives et utiles 90.3.127.139 (d) 4 juin 2012 à 09:22 (CEST)

Je trouve vos critiques sévères et injustes. Les prérequis de cet article sont clairs et les hyper-liens renvoient vers ce qu'il faut lire avant d'aborder la logique linéaire, à savoir

+ l'article sur la théorie de démonstration,

+ l'article sur l'isomorphisme de Curry-Howard,

+ l'article sur le lambda-calcul.

Comme souvent, quand on aborde un article d'une encyclopédie qui se trouve sur le sommet d'une tour de connaissance, il faut avoir lu d'autres articles ou être informé de leurs contenus. C'est le cas de l'article logique linéaire. Contrairement au pseudo article sur la tasse, cet article contient une définition de son objet: « [la logique linéaire est] un système de typage des programmes d'ordre supérieur [...] permettant d'exprimer la manière dont ceux-ci gèrent leurs ressources ». Je suis d'accord que cette définition ne dit pas pourquoi ce formalisme a été appelé une « logique » et la partie de la définition que j'ai sautée dit mal pourquoi Girard lui a associé l'adjectif « linéaire ». Je vous invite donc à faire des propositions d'amélioration. --Pierre de Lyon (d) 27 juin 2012 à 18:30 (CEST)

Pierre, je retiens votre phrase : "Je suis d'accord que cette définition ne dit pas pourquoi ce formalisme a été appelé une « logique » et la partie de la définition que j'ai sautée dit mal pourquoi Girard lui a associé l'adjectif « linéaire »." Je crois qu'il faut se résoudre à admettre que la définition proposée en préambule de l'article n'est pas satisfaisante. En fait, elle réduit la logique linéaire à certains de ses aspects mathématiques les plus abstraits. Mais on peut aussi voir la logique linéaire de façon beaucoup plus simple comme une logique de la consommation/production et même tenter d'étudier ses notions primitives, sans être un as en théorie de la démonstration. Cf. la thèse que j'ai rédigée il y a une quinzaine d'année http://www.youscribe.com/catalogue/rapports-et-theses/savoirs/techniques/formalisation-en-logique-lineaire-du-fonctionnement-des-reseaux-de-1544323. Bien cordialement, François.

La réponse de Pierre est une réponse de mauvaise foi, même si je ne remets en cause en aucun cas la bonne foi de Pierre lui-même.

1. Je lis une encyclopédie pour m'informer sur un sujet. En conséquence le chapeau de l'article est tout a fait indispensable se doit être clair et accessible a tout le monde. Cela n'est absolument pas le cas ici. POINT
2. La notion de prérequis est sans doute en vogue dans certaines régions du Mérieuxland. Elle n'a PAS sa place dans une encyclopédie. (re) lisez les merveilleux ouvrages de Flammarion ou de Quillet si vous désirez savoir ce QU'EST une encyclopédie.
3. Si on mettait des hyperliens pour coupe, hanap, etc.. L'article "tasse" resterait mauvais
4. Demander a quelqu'un qui ne connait rien d'un sujet de rédiger sur ce sujet, alors même qu'il affirme ne pas avoir pu prendre connaissance de ce sujet en raison d'une rédaction MAUVAISE, c'est simplement de la mauvaise foI

Ibn Harwa (d) 13 octobre 2012 à 11:30 (CEST)

La discussion met en lumière trois problèmes:

1. Il n'y a pas de bon livre didactique sur la logique linéaire, livre sur lequel les rédacteurs de l'article de Wikipédia pourraient s'appuyer.
2. Il n'y a pas assez de bonnes volontés pour participer à la rédaction de cet article.
3. Le fait de ne pas bien comprendre le pourquoi et le quoi de la logique linéaire est frustrant.

J'ajoute qu'il est vrai qu'un article en devenir n'a sa pas place dans une encyclopédie commerciale, d'où les grandes carences de la plupart d'entre elles. En revanche il a sa place dans l'encyclopédie très originale qu'est Wikipédia.

Qu'est-ce que le Merieuxland? Je n'ai pas trouvé d'article sur Wikipédia sur ce sujet, ni même sur le web.

--Pierre de Lyon (d) 16 octobre 2012 à 18:41 (CEST)

J'ai tenté d'améliorer l'introduction en ajoutant un paragraphe moins formel. Dites-moi ce que vous en pensez et aidez-moi à l'améliorer. --Pierre de Lyon (d) 4 novembre 2012 à 12:39 (CET)

Bonjour Pierre, Je reprends la souris après un arrêt forcé. Merci beaucoup de la modification du chapeau. Le premier paragraphe est désormais parfait (pour moi (sourire) ). Je pense pouvoir arranger un (petit) peu les deux autres paragraphes qui restent encore un peu durs. Pour ceux qui ne le savent pas, le Mérieuxland est un désert scientifique dont l'épicentre est à l'ex iufm de Lyon. Ibn Harwa (discuter) 2 octobre 2013 à 08:23 (CEST)

J'ai une peu amendé mon travail de novembre 2012, en créant un paragraphe pour ce qui dans l'introduction me paraissait un peu indigeste. J'ai aussi retiré le bandeau à recycler. --Pierre de Lyon (discuter) 14 août 2014 à 13:10 (CEST)

Remarques en passant

• « La logique linéaire diffère toutefois de la logique intuitionniste sur un point essentiel : elle dispose d'une négation qui satisfait toutes les symétries que l'on trouve en logique classique sous le nom de lois de De Morgan : la négation est involutive, la négation d'une conjonction est la disjonction des négations, etc.  » non! cette même négation peut-être surajoutée à la logique intuitionniste (c'est l'équivalent du signe moins en arithmétique). En fait, la "logique de la formule" est bancales et c'est pourquoi cette négation supplémentaire! est nécessaire. La "logiques des séquents bilatères" (où l'on prouve des séquents plutôt que de simples formules) est plus belle. Cette négation ne sert alors plus qu'à changer les termes de cotés (c'est à dire, à créer des redondances d'écritures).   <STyx @ (en long break) 4 octobre 2013 à 23:40 (CEST)
• et justement, il y aurait beaucoup à dire sur ces redondances d'écriture qui foisonnent.   <STyx @ (en long break) 4 octobre 2013 à 23:40 (CEST)
• choisir une formulation monolatère à droite n'est pas très heureux, car elle déroutante pour le néophyte. Il en existe d'autres : Lafont, Wadler, ... sans cet (affreux) $\,^{\bot }$.   <STyx @ (en long break) 4 octobre 2013 à 23:40 (CEST)
• « Sa structure peut être décomposée en des systèmes formels plus élémentaires qui décrivent des étapes plus fines de la déduction. » : je n'aime pas du tout cette phrase ... par ailleurs obscures. A mon sens, ces nouvelle logiques sont plus précises/précieuses : la logique classique (rustre) dit "vrai" là où la logique int. (précieuse) dit selon le cas "constructivement vrai" ou (indirectement) "non-constructivement vrai". La LL est plus précieuse encore. En conséquence, le système de déduction est plus précis (non pas « plus élémentaires » :( ), donc bridé, donc moins puissant. En revanche, grâce à certaines propriétés de ces logiques, on obtient des formulations et des évaluations de plus en fines des propositions. Inversement, du point de vue des nouvelles logiques, la logique classique est plus grossière, elle fait des amalgames sémantiques.   <STyx @ (en long break) 5 octobre 2013 à 00:22 (CEST)
• « Cette suppression conduit au dédoublement des connecteurs de conjonction et de disjonction. » NON! mais c'est la conséquence d'une formulation unilatère des séquents (ou sinon, la volonté de conserver les lois de De Morgan).   <STyx @ (en long break) 5 octobre 2013 à 00:46 (CEST)
• L'explication la plus simple (amha) est (en bref ;) : si « $C\vdash M$ » signifie « il faut du chocolat pour faire de la mousse (au chocolat) » alors cela signifie en LL, « il faut un (disons "e plaque de") chocolotat pour faire une mousse ». Bref on passe du qualitatif au quantitatif ! ... ou de l'indéfini (du) au défini (un) ... ou encore (mais, c'est plus contestable et ambigu) de l'immatériel (non dénombrable/librement duplicable ou supprimable) au matériel (dénombrable/non duplicable, non supprimable). On peut définir la LL avec le symbole  ! (« $!M$ » signifie « de la mousse » en LL ; c'est la « dématérialisation » ou « l'indéfinition » de $M$). Il serait plus pédagogique de partir de la logique classique correctement reformulée et bridée, et d'introduire la fonction inverse de « linéarisation » (Wadler emploie « $\langle M\rangle$ ») qui transforme $M$ : de la mousse, en $\langle M\rangle$ : une mousse. Ah lala ! je crois que je vais m'y mettre .   <STyx @ (en long break) 5 octobre 2013 à 01:23 (CEST)

Merci Beaucoup pour ces "remarques en passant" ; particulièrement pour l'utilisation de la "mousse au chocolat" pour rendre la LL plus "savoureuse", je veux dire par là "mangeable", "digeste", enfin vous m'avez compris ... ;) Khwartz (discuter) 7 septembre 2015 à 14:40 (CEST)