Discuter:Lambda-calcul

Un article de Wikipédia, l'encyclopédie libre.

WikiProjet Informatique
 Lambda-calcul fait partie du projet Informatique, qui a pour but d'enrichir le contenu de Wikipédia sur les sujets liés à l'informatique. Si vous voulez participer, vous pouvez modifier cet article ou visiter la page du projet où vous pourrez vous joindre au projet et consulter la liste des tâches et des objectifs. Le portail informatique pourrait aussi vous intéresser.
Bon début Cet article a été classé comme d'Avancement BD selon le Tableau d'évaluation du projet. (Voir les statistiques)
Élevée Cet article a été classé comme d'Importance élevée selon le Tableau d'évaluation du projet. (Contester?)

La réduction est une seule étape de réduction. Une bêta-réduction est une suite de réduction et de contractions. Et merci de ne pas cacher une modif en résummant à "mise en page" --Tom 9 jul 2004 à 15:18 (CEST)

Désolé pour l'intitulé de la modif, j'avais oublié que j'avais aussi ajouté ça avant de jouer un peu avec le code. J'aurais par contre apprécié un commentaire un peu moins suspicieux a priori, mais ce n'est pas très grave.
Sur le fond, je maintiens qu'on utilise le terme bêta-réduction pour désigner une étape de réduction. Et ça vaut mieux, parce que des réductions, y'en a un paquet. Outre les trois (alpha, bêta et êta) mentionnées ici, on peut ajouter delta (si on veut pouvoir utiliser des primitives), voire iota et zeta si on aime faire des preuves en Coq (cf [1], en anglais). -- Virgile 9 jul 2004 à 22:04 (CEST)

Désolé pour le ton suspicieux :-) Sinon on dirait que cette notion est vague. Certains appellent la réduction en une étape la "bêta0-réduction" d'autres "réduction" d'autres "bêta-réduction". Il faudrait regarder dans le Barendregt pour avoir quelque chose d'officiel. Sinon ouais ce serait bien de rajouter les autres réductions. --Tom 10 jul 2004 à 15:31 (CEST)

Je n'ai jamais vu "bêta0". Pour réduction tout court, c'est vrai que c'est un peu la règle (en fait, on parle souvent de règle plus que de réduction) de base, ce qui pourrait expliquer l'omission d'une partie du nom "quand le contexte est clair" comme on dit les bouquins. Pour le reste, j'avais déjà introduit alpha (qui n'est pas vraiment une réduction, mais plutôt une conversion) et êta dans l'article. Les autres (j'en ai cité que deux, mais le bestiaire est très, très vaste) ne s'appliquent qu'à des extensions du lambda-calcul de base, pas toujours triviales à décrire (c'est un champ de recherches actives), donc ça ne peut pas s'introduire d'un coup de baguette magique. -- Virgile 10 jul 2004 à 21:59 (CEST)

C'est vrai qu'il y a plein d'extensions. Je pense que rester sur le lambda calcul de base et le lambda calcul typé du permier et second ordre est une bonne idée. C'est une encyclopédie, pas un cours :-) --Tom 11 jul 2004 à 11:02 (CEST)

Hep là j'ai appris quelque chose, que ces variables que j'utilisais il y a 15ans en S c'était un développement d'un langage mathématique... c'est complêtement fantastique, mais j'en attends plus encore.N'est-ce pas aux nouveaux utilisateurs de ce langage de le faire comprendre à tous. Différent d'un langage informatique, les mathématiques ouvrent des espaces conceptuels...même si c'est une encyclopédie, ajoutez des liens expliquant concrêtement ce langage usuel. Je suis impatient de voir comment cela va s'étoffer d'autres articles.

En fait cette "réduction" peut s'appeler la bêta-contraction. La fermeture réflexive transitive de la bê-contraction c'est la bêta-réduction et la fermeture transitive symétrique de la bêta réduction c'est la bêta conversion ou bêta-équivalence. Voilà comme ça je pense que c'est clair.

Tom 11 oct 2004 à 14:37 (CEST)

Si tu veux. L'important là dedans c'est le bêta. Après, entre réduction et contraction, j'aurais tendance à penser que c'est une question de style. En tous cas la formulation actuelle me va parfaitement. Bon pour faire bonne mesure, j'ai introduit la delta-réduction, et un petit complément sur les types simples. Peut-être un jour le second ordre voire le cube de Barendregt si je trouve du temps... Virgile 14 oct 2004 à 23:22 (CEST)
Tiens ça faisait longtemps :-) Bravo pour la delta-réduction et les types simples, c'est joli. Pour le second ordre voire la publi dont j'ai rajouté le lien. Ca explique bien en peu de pages. Et c'est facile à trouver : c'est dans le JACM. A+ pour de nouvelles mises à jour :-)
Certains exemples sont déroutants, et nécessitent une approche plus progressive pour un lecteur non averti, je cite
  • f(x)=\int_a^b x+y ~dy, x est libre, hors dans un exemple suivant λx.y, x est lié ce qui semble contradictoire et nécessite plus d'explications.
  • (λx.xxx)(λx.xxx) = (λx.xxx)(λx.xxx)(λx.xxx) est un premier exemple déroutant, il fait le contraire de ce que le lecteur attend (une réduction de l'arbre) et surtout il arrive sans explications. il est mieux à sa place dans l'exemple expliqué plus bas au paragraphe normalisation

--Pilule (d) 30 avril 2008 à 00:44 (CEST)


Sommaire

[modifier] Retiré de l'article

je trouve que l'idée d'autoriser des corrections en direct est trés novateur et je décide de jouer le jeu en apportant mes connaissances dans le domaine mathématico-informatique afin de retrouver le plaisir de la recherche sauvage. KP

Salut, c'est bien d'avoir un nouveau contributeur sur cette page. Evite juste les abbréviations :-) même si je pense que tu n'as juste pas fait attention quand tu as mis le càd :-) Tom 30 oct 2004 à 11:48 (CEST)

Je donnerais bien un lien sur la version en ligne et gratuite de _Proofs and Types_, mais rien ne garantit que cette publication en ligne ne viole pas les droits d'auteur (cependant, je pense qu'elle est autorisée, car elle est stockée sur le site d'un chercheur, sur le serveur d'une université britannique).

je pense qu'il n'y a pas de problèmes vu que le livre n'est plus édité et qu'il est dispo sur le site de l'un des traducteurs. Tom 4 fev 2005 à 18:19 (CET)

"Même si en restreignant les termes valides par les types on garde généralement les plus intéressants."

A reformuler. Apokrif 4 fev 2005 à 19:31 (CET)

[modifier] Demande de revert

A cause d'un probleme de configuration, mon edition a fait sauter des caracteres speciaux. Je crains que si je fais un revert, les caracteres de l ancienne version disparaissent aussi,quelqu'un peut le faire a ma place ? Apokrif 4 fev 2005 à 19:42 (CET)

[modifier] Modestes remarques d'un modeste lecteur

Je viens de voir que cet article se trouve en première page de Google quand on tape la requête "lambda-calcul": Bravo !

Mais quelle déception quand on clique sur l'article: je n'y comprends rien !

On pourrait penser que c'est dûe à la complexité du sujet. Pourtant quand je lis l'article Lambda Calculus sur Wikipedia, je comprends tout ou presque. La difficulté ne vient pas de la matière, car en fait le Lambda-Calcul est une opération logique extrêment simple, la plus simple de toutes.

La stratégie adopté par les rédacteurs de la version anglaise me semble meilleur, car ils expliquent le fonctionnement du Lambda calcul par quelques exemples. Les définitions viennent ensuite, et vous remarquerez qu'il n'y a jamais de formalisme excessif. On voit par la suite clairement qu'il existe tous les éléments permettant la description du fonctionnement d'un langage de programmation: expression des entiers naturels et des opérations arithmétiques, opérateurs logiques, et puis surtout l'opérateur Y qui permet de faire fonctionner ce langage comme une véritable machine. On y voit également clairement l'influence du Lambda-calcul sur la science informatique.

Il me semble que vous oubliez vos lecteurs, et qu'il est dommage qu'une personne d'un niveau correcte en mathématique ne soit pas en mesure de comprendre une idée belle, élégante, et extrêmement puissante. --Geremy78 6 août 2005 à 18:28 (CEST)

je regarderai quand j'aurai un peu de temps. Et pour informations, ce n'est pas vraiment les mathématiciens qui étudient le lambda-calcul généralement mais les informaticiens. Donc il ne faut pas avoir un niveau correct en mathématiques (quoique) mais surtout un niveau correct en informatique. Naturellement en français il y a une ambigüité sur le mot "informatique". Il se traduit par deux mots en anglais : "computer science" et "information technology". Ici c'est des connaissances en "computer science" qu'il faut avoir :-) Mais promis j'essayerai de mettre une intro sympa ;-) Enfin si d'autres s'y dévouent ça ne me dérange pas non plus :-D Tom 7 août 2005 à 02:17 (CEST)
Bon j'ai rajouté deux trois petits trucs. C'est pas encore la panacée mais ça vient tout doucement.
Je me disais justement que ca manquait un peu d'exemple. Je vais en choisir quelques-uns parmis ceux que j'ai fais. Je les rajouterai le plus tot possible. M'vy 8 dec 2005

Je ne comprend rien car des termes sont utilisés sans être définis.

"L'outil le plus important pour le calcul est la substitution. Cette opération permet de remplacer une variable par un terme." Donc une variable peux s'identifier a un terme ? Quel est l'interet de remplacer une variable par un terme ? réponse:

"Grâce à ce mécanisme, les réductions vont pouvoir « calculer » le terme."

C'est quoi une réduction ? Donc un terme ca se calcule ? Quels sont les propriétés d'un terme ? J'ai vu qu'une application pouvait être un lambda terme, donc une application est calculable ??

"La substitution dans un lambda terme t d'une variable x par un terme u est notée t[x := u]."

Ok, donc si on avais deux fonctions f et g, on pourrais remplacer f(x) par f(g). Sauf que pour moi f(g) est un non sens si x n'est pas dans le meme ensemble que g ...

Enfin bon tous ca pour dire que je ne comprend rien.

Les articles sur le lambda-calcul sont toujours très légers et ne font que survoler le sujet. Disons qu'il y a deux approches:

  • l'approche ensembliste à la Jean-Louis Krivine où l'on s'intéresse au langage
  • l'approche implémentation à la Simon-Peyton-Jones où l'on s'intéresse à la machine d'éxécution

Cet article fait la part belle au langage. Soit. Mais même en admettant cette restriction, il est difficile d'être convaincu. Par exemple le combinateur Y ne permet que la récursion simple, pour un langage réaliste on a besoin de la récursion mutuelle. Il est difficile aussi d'imaginer que l'on va implémenter tous les TADs à l'aide de couples. Donc on veut des extensions, au minimum les TADs et les macros, voire une extension OOP.

Il faut aussi faire la distinction entre langage strict et langage paresseux -- Damien Guichard

[modifier] Plus d'exemples

Cet article est plutôt bon.
Cependant il donne souvent les définitions mathématiques sans tenter d'en indiquer le sens (Théorème de Church-Rosser : que signifie-t-il? De même l'exemple du lambda-terme non calculable n'est pas clair du tout pour un lecteur non averti.
Les constructions des booléens et des entiers demanderaient également quelques commentaires : c'est tout bonnement incompréhensible
L'auteur pourrait-il retravailler systématiquement chacun des passages les plus obscurs pour les rendre accessibles. Donner chaque fois un exemple serait une bonne chose.
Merci tout de même pour le travail effectué --Colonna 19 février 2006 à 17:31 (CET)

J'ai fait quelques modification notament sur le point de la normalisation, reduction et parenthésage.
Je passerai un peu de temps sur les applications ensuite. Booléens, entier de Church, les motivations et la construction des structures.
M'vy 21 février 2006 à 23:04 (CET)


[modifier] Lambda calcul et vulgarisation

Il y a quelques années (2002 ?) Science et Vie avait fait un dossier sur la question. De mémoire, il était très bon. Si je le retrouve, je l'ajouterais aux références. Seymour 15 octobre 2006 à 21:30 (CEST) Fait, mais il manque le titre exact du dossier, le numéro de page, et surtout un point de vue de spécialiste sur sa pertinence. Seymour 15 octobre 2006 à 21:51 (CEST)

Ayant un exemplaire de ce numéro de Science & Vie, voici les quelques infos le concernant :
L'article s'appelle "La vraie nature de l'intelligence", par Hervé Poirier (pages 38 à 57).
Cet article se décompose en 3 parties :
- "Toute pensée est un calcul" (pages 40 à 49) : Présente succintement le Lambda-Calcul, et la théorie de Jean-Louis Krivine selon laquelle Langage Informatique et Pensée Humaine auraient en commun une "couche" représentable en Lambda-Calcul (couche entre courant électrique et routines de base pour le Langage Informatique, langage logique entre influx nerveux et inconscient pour la Pensée Humaine).
- "Au-delà des mathématiques" (pages 50 à 53) : Présente le mathématicien Jean-Louis Krivine, et la démarche l'ayant amené à sa théorie.
- "L'informatique sauvée des bugs" (pages 54 à 57) : Présente quelques notions de démonstration de programmes (qui aurait pu éviter par exemple le crash d'Ariane 5 en 1996), et l'intérêt du logiciel Coq.
Je n'ai cependant pas d'avis de spécialiste sur la pertinence de cet article, si ce n'est que celui-ci semble avoir créé une vive réaction de la communauté scientifique travaillant sur le sujet et le Lambda-Calcul. De mon propre avis (qui n'a aucune valeur puisque je ne suis qu'étudiant), cet article a le mérite de présenter au grand public un modèle de calcul, mais avec les inconvénients que cela apporte (trop grande vulgarisation, sensation de révolution pour quelque chose qui n'est pourtant pas nouveau,...). Sib - 10 novembre 2006 à 01:23 (CET)
On m'a souvent parlé du livre de Raymond Smullyan en:To Mock a Mockingbird, qui est anglais et qui introduit plutôt la théorie sœur de la logique combinatoire, mais qui semble être très didactique. Pierre de Lyon (d) 11 mars 2008 à 10:07 (CET)


[modifier] Faut-il garder les grammaires ?

L'article propose deux grammaires pour les expressions parenthésées. Outre qu'elles ne me paraissent pas en bijection avec les langages décrits, elles n'apportent rien à clarté du texte. Dans une encyclopédie, il ne faut pas être trop pédant. Sans réaction des contributeurs, je me propose de les enlever. Pierre de Lyon (d) 11 mars 2008 à 10:07 (CET)