Calcul lambda en dehors de la programmation fonctionnelle?

21

Je suis un étudiant universitaire et nous étudions actuellement le lambda calcul. Cependant, j'ai encore du mal à comprendre exactement pourquoi cela est utile pour moi. Je me rends compte que si vous faites beaucoup de programmation fonctionnelle, cela pourrait être utile, mais je pense que ce n'est pas vraiment nécessaire pour apprendre la programmation fonctionnelle, qu'en pensez-vous?

Deuxièmement, le calcul lambda peut-il être utilisé dans le domaine de l'informatique mais en dehors des langages de programmation fonctionnels?

Jacob
la source

Réponses:

15

Le lambda calcul est fondamental en logique, théorie des catégories, théorie des types, vérification formelle, ... Fondamentalement, tout ce qui a à voir avec la sémantique du langage de programmation et la logique formelle. C'est un formalisme tellement fondamental que les personnes qui travaillent dans ces domaines n'en remettent même pas en question l'intérêt.

Je pense qu'il est extrêmement utile pour comprendre la programmation fonctionnelle car il vous donne l'essence de la programmation fonctionnelle. Fonctions, application, substitution. Sur cette base, vous pouvez développer vos compétences dans le raisonnement sur les programmes fonctionnels et leurs transformations. Les fonctions d'ordre supérieur sont un jeu d'enfant.

Bien sûr, vous pourriez apprendre la programmation fonctionnelle sans le calcul lambda, mais vous ne comprendriez jamais vraiment la programmation fonctionnelle sans lui.

Dave Clarke
la source
Merci beaucoup pour votre réponse Dave. Je pense que la vérification formelle est encore la meilleure raison pour expliquer pourquoi le calcul lambda est utile pour moi d'apprendre, et assez drôle, je ferai un cours sur la vérification formelle au semestre prochain. Souhaitez-vous également utiliser le calcul lambda pour effectuer une vérification formelle d'un logiciel écrit dans n'importe quel langage, par exemple un impératif ou orienté objet?
Jacob
1
Vous ne pouvez pas utiliser le calcul lambda directement lors de la vérification formelle, mais il apparaîtra dans les fondements de la vérification formelle. L'écriture de spécifications implique souvent l'écriture dans un langage fonctionnel, même pour le code impératif / OO.
Dave Clarke
D'accord, c'est intéressant, merci beaucoup, maintenant j'ai une raison de plus pour étudier cela. Savez-vous si le calcul lambda est utilisé pour concevoir des langages non fonctionnels (à des niveaux inférieurs)?
Jacob
1
ALGOL. Scala. En fin de compte, il est difficile de répondre à votre question. Le lambda-calcul est devenu une partie de la connaissance commune pour (la plupart) des concepteurs de langage et il influence donc la conception du langage, même s'il n'est pas explicitement utilisé. Considérez les blocs dans Smalltalk ou Ruby, les classes anonymes en Java. Ce sont des fermetures, qui sont étroitement liées aux fonctions d'ordre supérieur dans le calcul lambda.
Dave Clarke
D'accord, merci beaucoup Dave, c'est très apprécié.
Jacob
17

Vous demandez une application en dehors de l'informatique et de la logique. C'est facile à trouver, par exemple en topologie algébrique, il est pratique d'avoir une catégorie fermée cartésienne d'espaces, voir la catégorie pratique des espaces topologiques sur nLab. Le langage formel correspondant aux catégories fermées cartésiennes est précisément le -calculus. Permettez-moi d'illustrer avec un exemple très simple comment cela est utile.λ

Tout d'abord, comme exercice d'échauffement, supposons que quelqu'un vous demande si la fonction définie par f ( x ) = x 2 e x + log ( 1 + x 2 ) est différentiable. Vous n'avez pas réellement à prouver que c'est le cas, vous constatez simplement qu'il s'agit d'une composition de fonctions différenciables, donc différenciables. En d'autres termes, vous avez tiré une conclusion facile basée sur la forme de la définition.f:RRf(x)=x2ex+log(1+x2)

f:RRλ max sin

f(x)=(λf:C(R).xxf(1+t2)dt)(λy:R.max(x,sin(y+3))
λmax , , , etc.sin

Diverses extensions du -calculus permettent de faire la même chose dans d'autres domaines. Par exemple, comme un topos lisse est une catégorie fermée cartésienne, toute carte définie à l'aide du -calculus, à partir des dérivés et de la structure en anneau des réels (et vous pouvez ajouter la fonction exponentielle si vous le souhaitez) est automatiquement lisse. (En fait, le principal objectif des topos lisses est l'existence d'infinitésimaux nilpotents qui vous permettent de dire de manière significative des choses comme "nous disséquons un disque en triangles isocèles infiniment fins".)λλλ

Andrej Bauer
la source
1
Merci pour votre réponse élaborée. En fait, j'essayais de trouver une utilisation pour le calcul lambda en informatique mais en dehors de la programmation fonctionnelle, excuses si ce n'était pas clair. J'ai changé la question pour le dire plus clairement.
Jacob
Ah, dommage, j'aurais écrit une réponse détaillée à ce sujet.
Andrej Bauer
Toutes mes excuses à ce sujet. N'hésitez pas à ajouter des commentaires si vous souhaitez ajouter des informations supplémentaires :)
Jacob
2
Je pense que la question de Dave est très bien, je n'ai rien à ajouter. Si vous voulez voir les choses passionnantes que vous pouvez faire avec le -calculus, vous pouvez peut-être jeter un œil aux fonctionnalités impossibles. Mais comme réponse générale, Dave est très bon. λ
Andrej Bauer
7

Une façon de voir -calculus est un modèle simple et concis de programmes de paramétrage. Vous paramétrez le code dans presque tous les langages de programmation qui ont des fonctions, des procédures ou des méthodes, et dans n'importe quel langage qui a des modules ou qui vous permet de paramétrer des types. Le paramétrage est une forme de réutilisation. Parce que -calculus est si simple, les points communs entre de nombreux langages de programmation qui vous permettent de paramétrer du code, apparaissent clairement.λλλ

Il est certainement possible d'être un très bon programmeur sans connaître -calculus, mais vous manquez quelque chose de beau qui est également très utile.λ

Martin Berger
la source
5

λ

λ

λ

Peter Wone
la source