BONJOUR
(J'ai poster ce sujet dans la catégorie physique-chimie , mais on m'a dit qu'il était préférable de la poster ici.)
Donc voilà je voudrais savoir ce qu'est le lambda-calcul. Si quelqu'un pouvait me donner un réponse assez simple à comprendre ..
Merci d'avance.

Personnellement, je l'aurais plutôt posté dans "Autres langages, outils et approches" vu que c'est plutôt un outil (et une approche) informatique que mathématiques. Sinon n'ayant comme connaissance que ce que Wikipédia m'a appris, je ne pense pas pouvoir te répondre de manière satisfaisante.

Il te plaît pas l'article Wikipédia (et anglais affilié pour quelque chose de plus complet) ?

Non c'est juste qu'on m'a dit qu'il fallait mieux le poster ici donc c'est ce que j'ai fait.
Mais c'est pas que je n'aime pas l'article, je l'ai lu, c'est juste qu'il y a pas longtemps j'ai lu dans le magasine " Sciences et vie " qu'il y avait un théorie qui allait bouleversé notre vision du cerveau. En gros elle disait que toutes pensée étaient un calcul, et que dans le cerveau se superposent des couches de langage, dont le premier est le lambda-calcul.Ce que j'ai compris c'est qu'elle comparait le fonctionnement du cerveau a celui d'un ordinateur et que les deux utilisaient un langage , celui du lambda-calcul.L'ordinateur grâce au courant électrique , et le cerveau grâce à l'influx nerveux.
(c'est une théorie de jean-Louis Krivine et l'article date de 2002)
Je ne voulais pas qu'on me donne le lien d'un article, mais plutôt qu'on m'explique avec des mots plus simple parce que je ne comprends rien au langage mathématique qu'ils utilisent pour définir ce qu'est le lambda-calcul.Je pense que je n'ai pas les connaissances suffisantes pour comprendre. Mais merci quand même.

Un conseil : ne lit plus jamais science et vie sans prendre un regard critique sévèrement affuté.

Déjà, pas moyen de retrouver le moindre article faisant allusion à la théorie dont tu parles, même sur la page perso du chercheur : ça doit surement être faux ou quelque chose de vraiment trop interprété par les journalistes pour être exact.

La vulgarisation scientifique est une arête aiguë : d'un côté la lourdeur d'un formalisme inadapté au néophyte ou la complexité d'une abstraction impossible au débutant, de l'autre la science-fiction, le rêve, la surinterprétation, l'extrapolation.

Science et Vie a depuis un moment tendance à pencher du second côté.

Jean-Louis Krivine n'a jamais fait de neuroscience. Il y a fort à parier que l'article de Science et Vie soit le résultat de l'enthousiasme débordant d'un journaleux ne pipant que dalle au lambda-calcul et à la logique (thème de recherche de Krivine) en général.

Je ne suis pas un spécialiste du domaine, loin de là. Mais si tu veux savoir d'où vient le lambda-calcul, voici ce qu'on peut en dire.

Au début du siècle dernier, les mathématiciens ont voulu prendre un peu de recul sur les mathématiques en général. Des questions naturelles sont alors apparues : qu'est-ce qu'une preuve ? Qu'est-ce qu'une théorie mathématique ? Peut-on formaliser ces concepts abstraits en objets mathématiquement manipulable ? etc.

Ce sujet peut sembler un peu épistémologique et certains y verront surtout de l'enculage de mouche. Ceci dit, c'est un domaine qui a permis de penser les mathématiques différemment et d'avoir un regard nouveau sur certaines "certitudes" (voir par exemple le résultat le plus connu du domaine : le théorème d'incomplétude de Gödel).

Bref, c'est dans ce contexte scientifique que Church crée le lambda-calcul sur l'idée qu'en mathématiques, tout est fonction. Le lambda-calcul fournit une syntaxe (comment écrire les choses) et une sémantique (comment les comprendre) des fonctions.

Parallèlement au lambda-calcul, d'autres systèmes de formalisation prennent leur essor (tel la théorie de la démonstration). Ces domaines ont fourni quelques résultats et ont plus ou moins sombré pendant quelques temps. C'est dans les années 1960 qu'ils refleurissent grâce à la correspondance de Curry-Howard qui établit un lien entre système formel (objets mathématiquement manipulable) et système fonctionnel (moyen effectif de calcul). Cette correspondance lie notamment la théorie de la démonstration pour une certaine logique au lambda-calcul.

Le lambda-calcul a également joué un rôle non anodin dans le domaine de la calculabilité (savoir si quelque chose est réalisable par un ordinateur). Il est la base de la notion de fonctions récursives qui ne sont finalement qu'un autre formalisme des machines de Turing (plus ou moins la formalisation d'un ordinateur).

Enfin, tu peux aller regarder du côté du langage Haskell dont la syntaxe est inspiré du lambda-calcul.


J'espère que ceci t'aidera à comprendre d'où vient la notion. Si tu veux aller plus loin, il va falloir mettre les mains dans le cambouis, manipuler un peu de maths, et être près à tordre ses neurones dans tous les sens.

"Déjà, pas moyen de retrouver le moindre article faisant allusion à la théorie dont tu parles, même sur la page perso du chercheur : ça doit surement être faux ou quelque chose de vraiment trop interprété par les journalistes pour être exacte"
C'est le magasine n°1013 il date de février 2002 et le titre c'est "L'intelligence dévoile enfin sa vraie nature , toute pensée est un calcul !"

Citation

Enfin, tu peux aller regarder du côté du langage Haskell dont la syntaxe est inspiré du lambda-calcul.

Mais bien sûr ! La vulgarisation scientifique est une arête aiguë.

(Je n'ai pas vu ce topic intéressant parce qu'il a été posté n'importe où (il fallait poster dans Autres Langages comme dit plus haut), alors je suis aigri.)


Jean-Louis Krivine fait de la réalisabilité. Il espère révéler le contenu calculatoire des méthodes de preuves utilisées par les mathématiciens, en particulier l'axiome du choix. Il crée donc des liens fort entre le raisonnement et le calcul (au sens de la réduction des lambda-termes, ou encore de l'exécution d'un programme). C'est de là, je pense, que vient l'allusion au cerveau (qu'il a peut-être faite lui-même, il lui arrive je crois d'être un peu fantaisiste dans ses analogies).

Un autre sujet lié au lambda-calcul est l'école Montague en linguistique, qui cherche à expliquer le sens des phrases de façon compositionnelle en traduisant chaque mot en un lambda-terme associé. Les traductions sont plus ou moins compliquées selon la richesse des phénomènes linguistiques dont on veut rendre compte, mais ont des liens forts avec des outils utilisés pour l'étude des langages de programmation; par exemple, la dépendance du sens d'un mot à son contexte peut être représenté par un passage de continuations.