Discussion :

[am@123]

Bonjour à tous ,alors je crois que c'est le bon forum pour parler de lambda calcul,vu que ça fais parti des langages fonctionnels. j'ai lu un peut sur cette théorie , la question que j'ai pas trouvé, est ce qu'il existe des applications de cette theorie dans les autres domaines de l'informatique , bon c'est sur qu'il existe , mais les quels ???
si quelqu'un a une idée merci bien de la partager !

[gorgonite]

le lambda-calcul est la base de la théorie des langages informatiques... et le modèle fonctionnelle lui ressemble beaucoup

comme tout modèle mathématique, on peut le retrouver à plein d'endroits... mais bien caché

[InOCamlWeTrust]

Pour causer concret, les compilateurs Caml produisent littéralement du lambda calcul. Si l'on regarde bien la liste des options telle qui fournie par --help, il y a un certain nombre d'options non documentées : elles permettent, entre autres, de voir le lambda-code produit par la compilation... c'est assez marrant !

Donc, en tant que tel, le lambda-calcul ne sert à rien (peut-être comme décoration...), mais il est appliqué dans des domaines très concrets.

[am@123]

mais il est appliqué dans des domaines très concrets.

merci à vous , pour ce fil , justement c'est ce que je cherche , quels sont ses applications ??,et franchement je ne trouve pas la documentation, je dois donner des exemples concrets , et la sur google , il n'y a que le coté théorique , alors si quelqu'un peut m'aider , merci bien...

[millie]

Comme le lambda-calcul peut servir à formaliser la notion d'algorithme (tout comme d'autre équivalent, tel que les machines de turing). Tu peux démontrer formellement que des problèmes sont indécidables.

C'est en fait une application pratique, car ça te permet de démontrer que pour des problèmes particuliers, il n'y a pas de solution algorithmique.

Cela permet également de formaliser correctement la notion de Complexité. Et ainsi, tu peux montrer formellement que des problèmes sont par exemple NP-complet et donc que tu ne risques pas de pouvoir trouver des algorithmes résolvant le problème de manière efficace.

[Garulfo]

Comme le lambda-calcul peut servir à formaliser la notion d'algorithme (tout comme d'autre équivalent, tel que les machines de turing). Tu peux démontrer formellement que des problèmes sont indécidables.[...]

Ta phrase a un problème

Bon sinon le Lambda-calcul sert aussi dans la spécification de programme, la génération automatique de code, la preuve automatique, etc.
Souvent ce sont de bases des travaux de recherches qui sont difficiles à comprendre pour un étudiant de premier cycle universitaires. Mais il y a là de la matière.

Cherche des trucs comme

• automated programming lambda calculus
• automated proof lambda calculus
• specification lambda calculus
• automated reasonning lambda calculus
• vincent danos
• jean-louis krivine

et des combinaisons du genre.

Pour le côté complexité, on ne se sert peu ou pas du tout du lambda-calcul pour cette tâche. Les modèles plus « classique » sont plus développé et, donc a priori, plus approprié. Mais il y a peut-être des travaux que je ne connais pas.

Finalement à ma connaissance, le lambda-calcul a donné le pi-calcul qui sert dans la spécification de système de communication. On retrouve pas mal de travaux sur ça depuis une dizaine d'années. J'avais vu un chercheur du Microsoft Research Center, Andrew Gordon, faire une superbe présentation sur la sécurité. Cardelli se sert du pi-calcul pour la modélisation de système en bio.
Donc refait des recherches avec "pi-calculus"...

Sinon sache que le moteur de base de Google n'est pas le meilleur élément pour ce genre de recherche, mais par contre http://scholar.google.com/ est bien plus adapté.

Bon courage.

[millie]

Ta phrase a un problème

[gorgonite]

Bon sinon le Lambda-calcul sert aussi dans la spécification de programme, la génération automatique de code, la preuve automatique, etc.

les preuves automatiques utilisent le lambda-calcul ? comme tout en infos, il doit bien y avoir moyen de s'y reporter, mais des systèmes qui soient basés dessus

à ma connaissance, ils sont plutôt basés sur

• des systèmes de types (Coq par exemple)
• du model-checking
• de l'interprétation abstraite

sinon y a des systèmes comme tptp, que je connais assez mal

Finalement à ma connaissance, le lambda-calcul a donné le pi-calcul qui sert dans la spécification de système de communication. On retrouve pas mal de travaux sur ça depuis une dizaine d'années. J'avais vu un chercheur du Microsoft Research Center, Andrew Gordon, faire une superbe présentation sur la sécurité. Cardelli se sert du pi-calcul pour la modélisation de système en bio.
Donc refait des recherches avec "pi-calculus"...

MRC ne signifierait pas plutôt Microsoft Research Cambridge http://research.microsoft.com/~adg/


dans le genre petites subtilités supplémentaires, on peut citer le lambda-pi-calcul

[Garulfo]

les preuves automatiques utilisent le lambda-calcul ? comme tout en infos, il doit bien y avoir moyen de s'y reporter, mais des systèmes qui soient basés dessus

à ma connaissance, ils sont plutôt basés sur

• des systèmes de types (Coq par exemple)
• du model-checking
• de l'interprétation abstraite

Il y a beaucoup de système de preuve automatique: FDR2, HOL, ISABELLE, COQ etc. Certains sont obscurs et ne sont utilisés que là où ils ont été fait.
Beaucoup utilise ML en langage et, implicitement, les optimisations du lambda-calcul. J'avais suivi preuve automatique et aussi théorie de la démonstration quand j'étais à Paris VII en DEA de logique.

MRC ne signifierait pas plutôt Microsoft Research Cambridge http://research.microsoft.com/~adg/

Tu remarqueras que je n'ai pas utilisé d'acronyme.
Gordon et Cardelli travaille avec Cambridge, mais il y a d'autres Microsoft Research Center, dont un à Redmond et au moins un en Chine.

[gorgonite]

Beaucoup utilise ML en langage et, implicitement, les optimisations du lambda-calcul. J'avais suivi preuve automatique et aussi théorie de la démonstration quand j'étais à Paris VII en DEA de logique.

DEA de logique pure ou celui de sémantique & logique ?


effectivement, implitement si on considère que tout ce qui est fait de manière fonctionnelle découle du lambda-calcul...

Tu remarqueras que je n'ai pas utilisé d'acronyme.
Gordon et Cardelli travaille avec Cambridge, mais il y a d'autres Microsoft Research Center, dont un à Redmond et au moins un en Chine.

je croyais que vous traduisiez le sigle... désolé

[Garulfo]

DEA de logique pure ou celui de sémantique & logique ?

Logique pure.
Si je citais Danos et Krivine c'est qu'ils ont été mes professeurs;
Manoury et Chailloux aussi.

je croyais que vous traduisiez le sigle... désolé

C'est pas un drame Pis tu vas pas me vouvoyer quand même.

[gorgonite]

Logique pure
....

C'est pas un drame Pis tu vas pas me vouvoyer quand même.

je suis dans celui qui était autrement sémantique & logique, avec des profs comme Patrick Couseau, Xavier Leroy, etc

[InOCamlWeTrust]

merci à vous , pour ce fil , justement c'est ce que je cherche , quels sont ses applications ??,et franchement je ne trouve pas la documentation, je dois donner des exemples concrets , et la sur google , il n'y a que le coté théorique , alors si quelqu'un peut m'aider , merci bien...

Tu peux déjà commencer par compiler un petit bout de code en OCaml et utiliser l'une des options dont je parle dans le post un peu plus au-dessus : c'est un exemple concret de ce à quoi sert le lambda-calcul... de plus, OCaml est utilisé pour implanter le compilateur Lustre qui est lui-même utilisé pour faire les programmes volant sur les Airbus, ou encore faisant fonctionner des centrales nucléaires... plus concret que ça, tu meurs !

[Garulfo]

Relis la bien.. la première phrase n'a pas de proposition principale:
« Comme le lambda-calcul peut servir à formaliser la notion d'algorithme (tout comme d'autre équivalent, tel que les machines de turing). »
Tu vois, il manque un morceau.
Je suppose que la deuxième phrase est en faite la proposition principale de la première:
« Tu peux démontrer formellement que des problèmes sont indécidables. »
Ceci amène que tu as un point et une majuscule qui ne devrait pas être là.

(désolé de ce jolie HS sur l'analyse logique d'une phrase ^_^)

[InOCamlWeTrust]

Cela permet également de formaliser correctement la notion de Complexité. Et ainsi, tu peux montrer formellement que des problèmes sont par exemple NP-complet et donc que tu ne risques pas de pouvoir trouver des algorithmes résolvant le problème de manière efficace.

C'est marrant, car moi je suis intimement convaincu que : P = NP .

Enfin, bon, j'ai pas la démonstration, mais c'est juste un acte de foi très très fort.

[Jedai]

C'est marrant, car moi je suis intimement convaincu que : P = NP .

Enfin, bon, j'ai pas la démonstration, mais c'est juste un acte de foi très très fort.

C'est bien d'avoir la foi... Personnellement j'ai un gros doute, mais ça ne m'empêche pas de rêver de temps en temps (enfin ça signifierait aussi que la plupart des algorithmes actuels de cryptage deviendrait instantanément obsolète, mais bon...).

--
Jedaï

[millie]

C'est bien d'avoir la foi... Personnellement j'ai un gros doute, mais ça ne m'empêche pas de rêver de temps en temps (enfin ça signifierait aussi que la plupart des algorithmes actuels de cryptage deviendrait instantanément obsolète, mais bon...).

--
Jedaï

Oui et non. Si quelqu'un vient demain nous certifier que P=NP et que l'on ne dispose d'aucun moyen de trouver effectivement une formulation des algorithmes de cassage en complexité polynomial, ça ne nous servirait pas à grand chose. Juste à savoir, que le calcul de la bijection d'une fonction à sens unique à brèche secrète (par exemple) ne serait plus "difficile", mais bon, si on sait pas comment faire

[gorgonite]

je ne sais pas si vous suivez l'actualité (et si vous savez ce qu'il faut chercher), mais il y a eu récemment de grosses avancées sur le "crackage" de RSA... qui pourrait faire penser que P = NP

[Jedai]

Oui et non. Si quelqu'un vient demain nous certifier que P=NP et que l'on ne dispose d'aucun moyen de trouver effectivement une formulation des algorithmes de cassage en complexité polynomial, ça ne nous servirait pas à grand chose. Juste à savoir, que le calcul de la bijection d'une fonction à sens unique à brèche secrète (par exemple) ne serait plus "difficile", mais bon, si on sait pas comment faire

Oh que si ! Car tout problème NP peut-être rapporté à tout autre problème NP, c'est d'ailleurs comme cela que l'on prouve qu'ils sont dans la même classe (en démontrant que si l'on peut résoudre l'un on peut résoudre l'autre et vice-versa). Donc à partir du moment où tu as réussi à trouver un algorithme polynomial pour résoudre l'un des problèmes de NP, tu peux en déduire un algorithme polynomial pour n'importe quel autre problème NP, en fait il y a sans doute un chemin entier de "déduction" déjà dans les papiers de recherche, il ne reste plus qu'à le trouver et l'appliquer à ton algo polynomial.

je ne sais pas si vous suivez l'actualité (et si vous savez ce qu'il faut chercher), mais il y a eu récemment de grosses avancées sur le "crackage" de RSA... qui pourrait faire penser que P = NP

Vraiment ? C'est intéressant, tu as une URL ?
--
Jedaï

[millie]

Oui, justement, je ne parlais que du théorème : P=NP, sans preuve derrière.
En gros, je disais juste que si on savait seulement que P=NP, ça ne nous avancerait à rien.

Mais si on savait ce que tu as dit : "Donc à partir du moment où tu as réussi à trouver un algorithme polynomial pour résoudre l'un des problèmes de NP", c'est sûr ça serait beaucoup mieux.

D'ailleurs, il y a une fausse note dans la phrase, comme P est dans NP, il existe des problèmes dont il existe des solutions en temps polynomial dans P, donc dans NP.