Pourquoi est-il important que les fonctions soient anonymes dans le calcul lambda?

19

Je regardais la conférence de Jim Weirich, intitulée « Aventures dans la programmation fonctionnelle ». Dans cette conférence, il présente le concept de combinateurs Y, qui trouve essentiellement le point fixe pour les fonctions d'ordre supérieur.

L'une des motivations, comme il le mentionne, est de pouvoir exprimer des fonctions récursives en utilisant le calcul lambda afin que la théorie de Church (tout ce qui est effectivement calculable puisse être calculé en utilisant le calcul lambda) reste.

Le problème est qu'une fonction ne peut pas s'appeler simplement ainsi, car le calcul lambda n'autorise pas les fonctions nommées, c'est-à-dire

n(x,y)=x+y

ne peut pas porter le nom « », il doit être défini de manière anonyme:n

(x,y)x+y

Pourquoi est-il important pour le calcul lambda d'avoir des fonctions qui ne sont pas nommées? Quel principe est violé s'il y a des fonctions nommées? Ou est-ce que j'ai juste mal compris la vidéo de Jim?

Rohan Prabhu
la source
4
Cela ne semble pas du tout important. Vous pouvez affecter à une variable , puis vous avez donné un nom à la fonction. n(x,t)x+yn
Yuval Filmus
@YuvalFilmus oui, vous pouvez lier un nom à une fonction. Je pense que la vraie question ici, la perplexité, est pourquoi (en lambda calcul) une fonction ne peut-elle pas s'appeler par un tel nom? Pourquoi avons-nous besoin d'une technique comme l'opérateur Y pour effectuer des fonctions récursives? J'espère que ma réponse ci-dessous vous aidera.
Jerry101
1
@ Jerry101 La raison historique de l'absence d'auto-application est que -calculus était destiné à être un fondement des mathématiques, et la capacité de s'auto-appliquer rend un tel fondement immédiatement incohérent. Cette incapacité apparente (dont nous savons maintenant qu'elle peut être contournée) est donc une caractéristique de conception de -calculus. λλλ
Martin Berger
@MartinBerger, veuillez en dire plus. Incohérent pour la raison de ma réponse? Ou pour une autre raison?
Jerry101
1
@ Jerry101 Incohérent dans le sens où vous pouvez prouver 0 = 1 dans une telle fondation de mathématiques. Après Kleene et Rosser a montré l'incohérence du pur, typées -calcul, le simplement typé -calcul a été développé comme une alternative qui ne nous permet pas de définir combintors point fixe tels queλ Y λλλY . Mais si vous ajoutez une récursivité au -calculus simplement tapé, cela devient à nouveau incohérent, car chaque type est habité par un programme non terminé. λ
Martin Berger

Réponses:

24

Le principal théorème concernant cette question est dû à un mathématicien britannique de la fin du XVIe siècle, appelé William Shakespeare . Son article le plus connu sur le sujet est intitulé " Roméo et Juliette " a été publié en 1597, bien que les travaux de recherche aient été menés quelques années plus tôt, inspirés mais des précurseurs tels qu'Arthur Brooke et William Painter.

Son principal résultat, énoncé dans l' acte II. La scène II , est le célèbre théorème :

Qu'est-ce qu'il y a dans un nom? ce que nous appelons une rose
Par tout autre nom aurait une odeur douce;

Ce théorème peut être intuitivement compris comme «les noms ne contribuent pas au sens».

La plus grande partie de l'article est consacrée à un exemple complétant le théorème et montrant que, même si les noms n'ont aucun sens, ils sont à l'origine de problèmes sans fin.

Comme l'a souligné Shakespeare, les noms peuvent être modifiés sans changer le sens, une opération qui a été appelée plus tard -conversion par Alonzo Church et ses disciples. Par conséquent, il n'est pas nécessairement simple de déterminer ce qui est désigné par un nom. Cela soulève une variété de problèmes tels que le développement d'un concept d'environnement où l'association nom-signification est spécifiée, et des règles pour savoir quel est l'environnement actuel lorsque vous essayez de déterminer la signification associée à un nom. Cela a dérouté les informaticiens pendant un certain temps, ce qui a donné lieu à des difficultés techniques comme le fameux problème de Funarg.α. Les environnements restent un problème dans certains langages de programmation populaires, mais il est généralement considéré comme physiquement dangereux d'être plus spécifique, presque aussi mortel que l'exemple élaboré par Shakespeare dans son article.

Cette question est également proche des problèmes soulevés par la théorie du langage formel , lorsque les alphabets et les systèmes formels doivent être définis jusqu'à un isomorphisme , afin de souligner que les symboles des alphabets sont des entités abstraites , indépendamment de la façon dont ils "se matérialisent" comme éléments d'un ensemble.

Ce résultat majeur de Shakespeare montre aussi que la science s'écartait alors de la magie et de la religion, où un être ou un sens peut avoir un vrai nom .

La conclusion de tout cela est que pour le travail théorique, il est souvent plus pratique de ne pas être encombré de noms, même si cela peut sembler plus simple pour le travail pratique et la vie quotidienne. Mais rappelez-vous que tout le monde qui s'appelle maman n'est pas votre mère.

Remarque :
La question a été abordée plus récemment par la logicienne américaine du 20e siècle Gertrude Stein . Cependant, ses collègues mathématiciens réfléchissent encore aux implications techniques précises de son principal théorème :

Rose est une rose est une rose est une rose.

publié en 1913 dans une courte communication intitulée "Sacred Emily".

babou
la source
3
Note supplémentaire: Au cours des dernières décennies, "rose" a (en informatique) été principalement remplacé par "foobar" (et des parties de celui-ci) comme exemple canonique d'un nom aussi bon que n'importe quel autre. Cette préférence a apparemment été introduite par les ingénieurs ferroviaires américains.
FrankW
Cela dit, les noms canoniques des concepts souvent utilisés sont importants pour une communication efficace.
Raphael
1
@Raphael D'accord, mais je mettrais cela dans la catégorie de la vie quotidienne. Et comment connaissons-nous les limites de ce qui est vraiment canonique? Pourtant, je ressens souvent de l'inquiétude lorsque je vois des étudiants prendre toute la terminologie, la notation et les définitions (ou même la façon dont certains théorèmes sont énoncés) pour une vérité immuable donnée par Dieu. Même ici, sur SE, les élèves posent des questions, sans se rendre compte que nous ne connaissons peut-être pas leurs notations ou les définitions qu'ils utilisent en classe. La magie des vrais noms ne meurt pas facilement.
babou
10

λλπνx.Pπ

λλλ paradoxe de Kleene-Rosser ). Haskell Curry a analysé le paradoxe de Kleene-Rosser et s'est rendu compte que son essence est ce que nous connaissons maintenant sous le nom de Y-Combinator.

letf=MinN(λf.N)Mλ

Martin Berger
la source
1
Je pense que l'OP voulait pouvoir nommer des fonctions, pas interdire des fonctions anonymes. Cela dit, je pense que toute exigence de λ-calcul concernant la nécessité de fonctions anonymes se manifesterait également dans des langages comme Lisp / Scheme ou ML. Dans le cas de Lisp / Scheme, la méta-circularité des évaluateurs devrait permettre de créer de nouveaux noms selon les besoins, même si je ne suis pas sûr que je le souhaiterais de cette façon dans un système formel. L'utilisation d'un nombre illimité de fonctions n'est pas nécessairement un problème lorsque la récursivité permet la réutilisation locale des noms déjà utilisés.
babou
λλ
La dernière ligne doit-elle indiquer (lambda f. N) M?
Joe the Person
@JoethePerson Oui, bien repéré. Fixé. Merci.
Martin Berger
4

Je crois que l'idée est que les noms ne sont pas nécessaires. Tout ce qui semble nécessiter des noms peut être écrit comme des fonctions anonymes.

Vous pouvez penser au calcul lambda comme au langage d'assemblage. Quelqu'un dans une conférence sur l'assemblage pourrait dire "Il n'y a pas d'arborescence d'héritage orientée objet dans le langage d'assemblage." Vous pourriez alors imaginer une manière intelligente d'implémenter des arbres d'héritage, mais ce n'est pas la question. Le fait est que les arbres d'héritage ne sont pas requis au niveau le plus élémentaire de la programmation d'un ordinateur physique.

Dans le calcul lambda, le fait est que les noms ne sont pas nécessaires pour décrire un algorithme au niveau le plus élémentaire.

Real John Connor
la source
4

J'apprécie les 3 réponses ici jusqu'à présent - plus particulièrement l'analyse Shakespearen de @ babou - mais elles ne mettent pas en lumière ce que je pense être l'essence de la question.

Le λ-calcul lie les noms aux fonctions chaque fois que vous appliquez une fonction à une fonction. Le problème n'est pas le manque de noms.

"Le problème est qu'une fonction ne peut pas s'appeler simplement" en se référant à son nom.

(En pur Lisp, la liaison nom -> fonction n'est pas dans la portée du corps de la fonction. Pour qu'une fonction s'appelle par son nom, la fonction devrait se référer à un environnement qui fait référence à la fonction. Pure Lisp n'a pas structures de données cycliques. Impure Lisp le fait en mutant l'environnement auquel la fonction se réfère.)

Comme l'a souligné @MartinBerger, la raison historique pour laquelle le λ-calcul ne laisse pas une fonction s'appeler par son nom était une tentative d'exclure le paradoxe de Curry lorsqu'il essayait d'utiliser le λ-calcul comme fondement des mathématiques, y compris la logique déductive. Cela n'a pas fonctionné car des techniques comme le combinateur Y permettent la récursivité même sans auto-référence.

De Wikipédia:

Si nous pouvons définir la fonction r = (λ.x x x ⇒ y)alorsr r = (r r ⇒ y) .

Si r rc'est vrai, alors yc'est vrai. Si r rest faux, alors r r ⇒ yc'est vrai, ce qui est une contradiction. Il en yva de même et comme ypour toute déclaration, toute déclaration peut être vérifiée.

r rest un calcul sans terminaison. Considéré comme logique r rest l'expression d'une valeur qui n'existe pas.

Jerry101
la source
λ.x xxxxx
@RohanPrabhu se λ.x x xtraduit en Lisp as (lambda (x) (x x))et en JavaScript as function (x) {return x(x);}. x⇒ysignifie x implies y, à peu près la même chose que (NOT x) OR y. Voir en.wikipedia.org/wiki/Lambda_calculus
Jerry101
Merci d'avoir répondu à cette question embarrassante de recrue!
Rohan Prabhu