Lambda-calcul : un jeu de mathématicien ?

Bonjour,
J'ai découvert le lambda-calcul il y a plus d'une quinzaine d'année lors de ma dernière année de D.E.A. C'était pas le dernier cours de ma scolarité mais presque ! Ca m'avait été présenté à l'époque uniquement sous son aspect mathématique. Le lien avec l'informatique était totalement absent... On avait bien eu des cours Lisp, mais là uniquement comme langage informatique. Le lien n'était pas fait. Faut croire qu'il manque de salle de café dans les salles de profs.
Comme je présume que parmi vous il doit y avoir de jeunes () étudiants, je serais curieux de savoir comment est abordé le lambda calcul aujourd'hui ?

Cependant, j'avais bien aimé la chose à l'époque. Mais, bon après, il a fallu manger, donc : au boulot ! Et là, toutes ces belles théories : aux oubliettes
Quelqu'un a-t-il déjà été amené à travailler avec ces concepts de lambda calcul dans le monde professionnel (s'entend hors contexte de recherche) ?

Je suppose que ça dépend pas mal d'où tu étudies : pour ma part à l'ENS Lyon j'ai bouffé du lambda-calcul à toutes les sauces (ça tient aussi au fait que ça fait partie des domaines qui m'intéresse).
La connaissance du lambda-calcul et problématiques afférentes est très intéressant dès lors que tu cherches à écrire un DSL et a fortiori un interpréteur/compilateur, tu peux t'en sortir sans mais tu perds pas mal de temps et le résultat est généralement moins intéressant. Bien sûr des tas d'informaticiens vivent leur vie entière sans écrire aucun méta-code mais développer un DSL adapté à l'application à développer est en fait une stratégie très efficace et souvent utilisée par les équipes de très bons programmeurs.

Le lambda-calcul en tant que base de tous les langages fonctionnels est également intéressant pour te donner une perspective de haut-niveau sur cette classe de langage, utile si tu essaies d'en utiliser un dans ton boulot...

--
Jedaï

Ce qu'il y a de remarquable avec le lambda-calcul c'est que :
*il est plus ancien que la machine de Turing
*alors que machine de Turing, qui est plus récente, n'a plus rien à apporter et est devenu un désert théorique, le lambda-calcul reste incroyablement fécond, il est le modèle sous-jacent incontournable pour développer et étudier les propriétés des nouvelles sémantiques ou des nouveaux systèmes de typage
*il reste le modèle behavioriste de référence pour l'implantation des langages fonctionnels (plus comme le dit Jedai une technique d'implantation naive pour rapidement prototyper un interpréteur)

(suite)(pas droit à plus de 1000 caractères ni à la balise list )

Par contre, à un niveau plus pragmatique :
* le monde étant ce qu'il est je pense que le secteur informatique continuera de rechercher une main-d'oeuvre abondante qui maîtrise les frameworks les plus répandus, plutôt qu'une main d'oeuvre rare qui maîtrise des sémantiques "ésotériques". dans ces conditions le paradigme fonctionnel peut échapper au monde universitaire, en particulier parce qu'il bénéficie d'un certain soutien de la part de Microsoft, mais on peut s'attendre à ce que cette démocratisation ne bouleverse pas la convergence du marché vers des technologies tout POO
* même à supposer que tu programme dans un langage fonctionnel tu n'as pas vraiment plus besoin de connaissances sur le lambda-calcul qu'un programmeur Java a besoin de connaissances sur la machine de Turing

(suite et fin)

* aucun compilateur moderne n'utilise le lambda-calcul en tant que technique d'implantation, au contraire une étape importante de la compilation consiste à éliminer les lambda-abstractions (étape dite de lambda-lifting) afin d'éviter trop de béta-réductions et trop de créations de fermetures.

@spiceguid, le lambda-calcul est plus ancien, mais il n'avait pas le même objectif à ses débuts. Il était là pour être un autre système de fondation des mathématiques comme la théorie des ensembles. Le fait qu'il ait échoué à cette tâche, avec le paradoxe de Kleene-Rosser, fait qu'on a tout d'un coup plus vue l'intérêt de modèle de calcul.

Sinon personnellement, j'ai vu du lambda-calcul dans mes études à partir du DEA (Logique à Paris VII). C'est donc une version plus mathématique qu'informatique que j'ai vu, même si on faisait des liens, notamment avec ocaml.

Pour 3Darchi, il me semble que tu n'auras pas beaucoup de réponse ici. Ne sommes-nous pas tous des vieux chevaliers à la bannière ornée de lambda ?

@Garulfo: Comme je le dis au début, j'ai comme toi abordé le lambda-calcul du point de vue math aussi à mon D.E.A. (en 95) (aussi autour des pbs de logiques...). Je pensais qu'aujourd'hui ça pouvait être plus enseigné en informatique. C'est entre autre pour ça que j'ai ouvert le sujet. Pour savoir, s'il y a des étudiants dans la salle, comment le lambda-calcul est aujourd'hui présenté.

Je vais avoir une U.E "Modèles de calcul" là, je te dirai si on va aborder le lambda-calcul, mais j'en doute fort.

En cours de Lisp, on avait un peu étudié la chose, mais je crois que je n'ai rien retenu du cours sur cette partie et je n'arrive même plus à retrouver mes supports de cours concernant ça.

Enfin, de manière générale, je ne retiens pas trop les cours que je suis

@3DArchi. Oui j'avais compris. Ce que je voulais dire, c'est que, pour ma part, je n'ai pas fait d'études en informatique. C'est donc différemment que j'ai perçu le lambda-calcul. On me le présentait avant tout dans l'optique d'une nouvelle fondation puis en lien avec la théorie de la démonstration et des prouveurs.

Et sinon, je peux te dire comment moi je l'enseigne en informatique: lorsque je donne le cours de programmation fonctionnel, je fais un léger lien avec le lambda calcul pour leur montrer qu'il existe un modèle simple à appliquer. Mais ça s'arrête là. Mon mentor lui faisait une semaine complète de lambda-calcul et un premier devoir tout de suite dessus. Les notes étaient catastrophiques ^_^