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.

[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.

[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 !