Discussion:Lambda-calcul

La réduction

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 $\lambda x.y$, $x$ est lié ce qui semble contradictoire et nécessite plus d'explications.
• $(\lambda x.xxx)(\lambda x.xxx)=(\lambda x.xxx)(\lambda x.xxx)(\lambda 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)

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)

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)

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

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)

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)

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)

Je pense que c'est néanmoins un bon outils pour comprendre la syntaxe grammaticale du langage. Peut-être serait-il intéressant de créer un wikiBook sur le thème du Lambda-calcul et laissé l'article encyclopédique plus concis? M'vy (d)

Je découvre cet article en cherchant à mieux comprendre la fonction lambda dont dispose Python. Les grammaires pour les expressions parenthésées ne me paraissent pas non plus en bijection avec les langages décrits. Si je me permettais, j'évoquerais le bug du copié-collé. La dernière alternative de la seconde forme ne serait-elle pas (Λ) Λ plutôt que Λ (Λ). Quoi qu'il en soit davantage d'explications me sembleraient utiles, en ce qui me concerne en tous cas.--90.49.174.63 (d) 9 janvier 2009 à 18:25 (CET)

Je ne tiens pas spécialement à ce que les grammaires soient gardées, cependant il semble que cela faisait 12 ans qu'elles ne correspondaient pas au texte qui précedait. J'ai donc paré au plus pressé en les corrigeant.GuiGeek (discuter) 4 mars 2020 à 14:09 (CET)

Merci. J'avais oublié ma proposition d'il y a onze ans ! Peut-être pourrait-on réévaluer le fait de garder ces grammaires ou non. --Pierre de Lyon (discuter) 5 mars 2020 à 08:55 (CET)

Je trouve que, pour qui s'intéresse au lambda, la notion de grammaire est capitale. Après il y a la question de quelle grammaire, et avec quelle syntaxe/formalisme. --Jean-Christophe BENOIST (discuter) 5 mars 2020 à 12:37 (CET)

un manque de parenthésage?

Bonjour, curieux de mathématiques j'essaye d'apprendre le lambda calcul sur internet, je me trompe peut être mais il me semble qu'il manque des parenthèse aux termes:

• fthenelse vrai x y = λbuv.(b u v) vrai x y

qu'il faudrait plutôt écrire :

• fthenelse vrai x y = (λbuv.(b u v)) (vrai) x y

Ce qui me parait logique car dans le premier cas, il n'y a pas de redex.

En effet sur le lambda calculateur trouvé à cette page: http://joerg.endrullis.de/lambdaCalculator/index.html, rien ne se passe si on met:Init = \b.\u.\v.(b u v) \a.\b.a x y; mais si on met:Init = (\b.\u.\v.(b u v)) (\a.\b.a )x y;ça marche

Merci pour ce que vous faites --Nicobzz (d) 23 octobre 2010 à 18:22 (CEST)

Autre remarque

Bonjour, j'ai peur de vous déranger mais peut-être la remarque que je porte permettra de clarifier le texte si je l'ai bien compris car il me semble qu'il y a des informations contradictoires:

il est écrit:

"Un lambda-terme t est dit en forme normale si aucune bêta-contraction ne peut lui être appliquée, c'est-à-dire si t ne contient aucun rédex. Ou encore, s'il n'existe aucun lambda-terme u tel que t → u. Exemple: λx.y(λz.z(yz)) ."

• ce que je comprend comme: la forme normale est le terme de la dernière réduction d'une suite de réduction.

d'autre part il est écrit:

"On dit qu'un lambda-terme t est normalisable s'il existe un terme u tel que t =β u. Un tel u est appelé la forme normale de t."

• ce que je comprend comme: la forme normale est un terme d'un réduction quelconque d'une suite de réduction.

il est aussi écrit:

"On dit qu'un lambda-terme t est fortement normalisable si toutes les réductions à partir de t sont finies."

• ce que je comprend comme un lambda terme qui accepte une forme normale (dans le sens le terme de la dernière réduction d'une suite de réduction.) est fortement normalisable.

et enfin, et excusez moi d’écrire tant, il est écrit:

"(λx.y)(ΔΔ) est normalisable et sa forme normale est y, mais il n'est pas fortement normalisable."

• ce que je comprend comme un lambda terme qui admet une forme normale n'est pas forcément fortement normalisable, et de plus un terme qui admet une réduction ne contenant pas de redex n'est pas fortement normalisable.

Donc deux questions:

• La forme normale est elle la dernière réduction d'une suite de réduction?
• Pourquoi (λx.y)(ΔΔ) qui admet une dernière réduction sans rédex n'est pas fortement normalisable?

Merci vraiment à tous ceux qui ont rédiger cet article! --Nicobzz (d) 24 novembre 2010 à 23:21 (CET)

Je réponds à vos questions:

• La forme normale est elle la dernière réduction d'une suite de réduction?

Une forme normale est un terme tandis qu'une réduction est une relation, donc énoncée ainsi la proposition est bancale. En revanche, si l'on part d'un terme et qu'on le réduit jusqu'à ce qu'on ne puisse plus, le dernier terme que l'on obtient est une forme normale.

• Pourquoi (λx.y)(ΔΔ) qui admet une dernière réduction sans rédex n'est pas fortement normalisable?

Etant donné un terme, on peut réduire à différents endroits, on dit que la réduction est non déterministe. Ainsi dans (λx.y)(ΔΔ), on peut réduire λx.y.??, mais on peut aussi réduire ΔΔ, qui se réduit en ΔΔ, qui contient un redex, donc (λx.y)(ΔΔ) se réduit en (λx.y)(ΔΔ) et le processus ne s'arrête pas.

--Pierre de Lyon (d) 5 décembre 2010 à 19:33 (CET)

merci beaucoup...

• Je me suis permis de changer l'article en rajoutant un commentaire sur la réduction de (λx.y)(ΔΔ), mais surtout n'hésitez pas à l'annuler ou le changer si cela ne vous parait non rigoureux.
• Dans l'exemple (λx.y)(ΔΔ) considérez-vous que Δ ≡ λx.xx? dans ce que cas tout devient logique, cependant si c'est le cas il faudrait changer de position la phrase: " Posons Δ ≡ λx.xx" pour faire comprendre que celle ci s'applique à tout les exemples.
• Enfin: J'ai bien compris toutes les phrases que j'avais cité en comprenant où était mon erreur sauf celle-ci, peut être pourrez vous m'éclairer: je cite l'article: "On dit qu'un lambda-terme t est normalisable s'il existe un terme u tel que t =β u. Un tel u est appelé la forme normale de t.", dans cette phrase je comprend bien que t est normalisable s'il existe un terme u tel que t =β u, par contre je ne comprend pas pourquoi u serait la forme normale de t, car d'après ce que j'ai compris une forme normale n'a pas de redex , par exemple :λx.y(λz.z(yz)) donne comme terme après une réduction:λx.y(yz) qui contient un redex... A moins qu'on considère les termes français: "la forme normale du terme t" et "Un lambda-terme t est dit en forme normale" des significations différentes, ce qu'il faudrait préciser dans l'article pour le rendre plus clair.

--Nicobzz (d) 6 décembre 2010 à 23:07 (CET)

commentaire d'un inconnu:

En utilisant les outils dont on vient de se doter, on obtient, par applications et abstractions, des fonctions assez compliquées que l'on peut vouloir simplifier ou évaluer. Simplifier une application de la forme $(\lambda x.E)P$ revient à la transformer en une variante de l'expression $E$ dans laquelle toute occurrence libre de $x$ est remplacée par $P$. (c'est sans doute faux: c'est la formule P dans laquelle on remplace tous les x par de E non?)Cette forme de simplification s'appelle une contraction. il a en particulier écrit : "(c'est sans doute faux: c'est la formule P dans laquelle on remplace tous les x par de E non?)"

je ne suis pas un pro du lambda calcul et je l'ai appris sur wikipedia et sur internet, mais non cela est bien comme c'est écrit dans wikipedia : $(\lambda x.E)P$ revient à la transformer en une variante de l'expression $E$ dans laquelle toute occurrence libre de $x$ est remplacée par $P$.--Nicobzz (d) 10 avril 2012 à 23:05 (CEST)

Je confirme que c'est bien cela, c'est même la bêta-contraction que l'on peut même considérer comme la principale voire la seule règle de calcul du lambda-calcul. --Epsilon0 ε₀ 13 avril 2012 à 18:40 (CEST)

Je pense que le lecteur « inconnu » qui pose la question a confondu la construction $(\lambda x.E)P$ avec la conctruction let x = E in P qui existe dans des extensions du lambda-calcul (par exemple en OCaml) et qui fait bien ce qu'il dit : à savoir remplacer x par E dans P. --Pierre de Lyon (discuter) 30 mars 2017 à 08:51 (CEST)

Suppression de l'article Forme normale (lambda-calcul)

Il me semble que l'article indigent Forme normale (lambda-calcul) devrait être supprimé et remplacé par un simple renvoi vers le paragraphe La normalisation : notion de calcul de cet article. Qu'en pensez-vous? --Pierre de Lyon (discuter) 20 mars 2017 à 10:27 (CET)

Je suis d'accord et pense même que l'article devrait être supprimé car je vois mal qui chercherait un tel article, mais je ne sais. Son historique montre qu'il est dans cet état depuis 2005 et ce 12 minutes après sa création suite à un déplacement du contenu dans un autre article par son créateur  Laubrau :. --Epsilon0 (discuter) 12 juillet 2017 à 23:14 (CEST)

P.S :@Pierre merci d'avoir retiré mon explication fausse que je venais d'ajouter, ça m'a sauté au yeux quand j'ai vu ton commentaire. De plus l'explication correcte est dans le paragraphe juste au dessus --Epsilon0 (discuter) 12 juillet 2017 à 23:14 (CEST)

Les indices de de Bruijn

Un lambda-terme avec des liens

En regardant l'article Machine de Krivine, je m'aperçois qu'il n'y a pas assez d'explications sur les indices de de Bruijn sur lesquelles m'appuyer. Ma question est : doit-on étendre le paragraphe de l'article lambda-calcul (celui-ci) ou créer un article spécifique ? --Pierre de Lyon (discuter) 10 octobre 2017 à 19:38 (CEST)

 Epsilon0 : Ta modification qui consiste à faire démarrer les indices de de Bruijn à 1 est historique, puisque c'est celle de de Bruijn en 1972, mais il me semble que l'idée de commencer à 0 correspond à la norme dans les langages de programmation et les ouvrages didactiques du XXI^e siècle, comme par exemple dans le livre de Benjamin Pierce, Types and Programming Language, The MIT Press, 2002 (ISBN 0-262-16209-1, lire en ligne). --Pierre de Lyon (discuter) 10 juin 2018 à 23:06 (CEST)

 PIerre.Lescanne : Je ne suis pas sûr de bien comprendre ce que dit la page du livre que tu cites et via la convention adoptée, je remarque néanmoins qu'il est dit :

We know what to do with x, but we cannot see the binder for y, so it is not clear how “far away” it might be and we do not know what number to assign to it. The solution is to choose, once and for all, an assignment (called a naming context) of de Bruijn indices to free variables, and use this assignment consistently when we need to choose numbers for free variables

bref (même si n'ayant pas tous le contexte, je ne comprend pas bien) que c'est pas si clair et que comme je le pensais (voir mon commentaire de diff) la question de la représentation des variables libres est en jeu.

Un terme avec des liens (version 2 sans @)

Sinon, mon but initial était de réutiliser l'image qui m'a semblée claire de l'article anglais, mais je ne pouvais le faire sans modifier le codage au rique d'une contradiction.

Bref je te laisse faire si tu penses avoir de bonnes idées pour améliorer cette section que tu as très pertinemment initiée. --Epsilon0 ε₀ 11 juin 2018 à 19:55 (CEST)

Tu as raison : une image vaut mieux que milles explications. Que penses-tu de cette image ? --Pierre de Lyon (discuter) 11 juin 2018 à 21:37 (CEST)

Pour l'image dont je vois que tu es le créateur, l'aspect arbre me semble la représentation la plus claire de manière générale pour représenter la formation d'un terme (ou d'une du calcul des prédicats ; connaissance qui semble manquer à un récent intervenant du ensemble vide )donc tb. Sinon là tu gardes des variables liées avec valeur "0" : ok mais alors il faut harmoniser la section, cette fois avec i --> i-1. Aussi un détail concernant l'image : pourquoi cet espèce d'arobase (de @) dans les noeuds/sommet ? : on pourrait croire qu'un opérateur formel est à l’œuvre lors que ce n'est que le sommet d'un graphe qui n'a pas besoin d'être tagué. --Epsilon0 ε₀ 11 juin 2018 à 23:08 (CEST)

L'@ est la représentation de l'application en lambda-calcul. --Pierre de Lyon (discuter) 12 juin 2018 à 07:47 (CEST)

 Epsilon0 : Préfères-tu la seconde image ? --Pierre de Lyon (discuter) 12 juin 2018 à 09:45 (CEST)

Oui elle me semble plus lisible --Epsilon0 ε₀ 12 juin 2018 à 11:48 (CEST)

Je ne connais rien au lambda-calcul, et j'aime bien les deux images. Si l'arobase est standard et expliqué, ça me va (désolé, pas plus de temps pour me concentrer plus). Bonne journée et merci à vous ! --Fschwarzentruber (discuter) 12 juin 2018 à 12:17 (CEST)

L'article Forme normale (lambda-calcul) est proposé à la suppression

Bonjour, L’article « Forme normale (lambda-calcul) (page supprimée) » est proposé à la suppression (cf. Wikipédia:Pages à supprimer). Après avoir pris connaissance des critères généraux d’admissibilité des articles et des critères spécifiques, vous pourrez donner votre avis sur la page de discussion Discussion:Forme normale (lambda-calcul)/Suppression. Le meilleur moyen d’obtenir un consensus pour la conservation de l’article est de fournir des sources secondaires fiables et indépendantes. Si vous ne pouvez trouver de telles sources, c’est que l’article n’est probablement pas admissible. N’oubliez pas que les principes fondateurs de Wikipédia ne garantissent aucun droit à avoir un article sur Wikipédia. Pierre de Lyon (discuter) 10 octobre 2017 à 19:54 (CEST)

Fonction successeur

Je me suis permis d'annuler la modification de Polpalto du 12 février, puisque l'article dit explicitement que l'on est en train de construire un entier de Church. La phrase suivante expliquant que la fonction s'obtient en ajoutant une lambda-abstraction sur l'entier `n`. Si Polpalto souhaitait modifier plus profondément ce paragraphe, je n'y vois pas d'inconvénient et il ne faut pas voir dans cette annulation un attachement particulier à ce paragraphe. Cependant, même transitoirement, mieux vaut éviter les états incohérents de l'article. GuiGeek (discuter) 23 février 2022 à 17:15 (CET)