Lambda Calculus est-il purement syntaxique?

29

Je lis depuis quelques semaines sur le Lambda Calculus, mais je n'ai encore rien vu qui soit matériellement distinct des fonctions mathématiques existantes, et je veux savoir si c'est juste une question de notation, ou s'il y a de nouvelles propriétés ou règles créées par les axiomes de calcul lambda qui ne s'appliquent pas à toutes les fonctions mathématiques. Ainsi, par exemple, j'ai lu cela:

"Il peut y avoir des fonctions anonymes" : les fonctions Lambda ne sont pas anonymes, elles sont simplement appelées lambda. Il est permis en notation mathématique d'utiliser la même variable pour différentes fonctions si le nom n'est pas important. Par exemple, les deux fonctions d'une connexion Galois sont souvent appelées *.

"Les fonctions peuvent accepter des fonctions comme entrées" : Pas nouveau, vous pouvez le faire avec des fonctions ordinaires.

"Les fonctions sont des boîtes noires" : seules les entrées et les sorties sont également des descriptions valides des fonctions mathématiques ...

Cela peut sembler être une discussion ou une question d'opinion, mais je crois qu'il devrait y avoir une réponse «correcte» à cette question. Je veux savoir si le calcul lambda n'est qu'une convention de notation ou de syntaxe pour travailler avec des fonctions mathématiques, ou s'il existe des différences substantielles ou sémantiques entre les lambdas et les fonctions ordinaires.

Neil
la source
2
Je ne veux pas en faire une réponse complète, mais les fonctions ne peuvent pas accepter les fonctions comme entrées. Je peux écrire f (g (0)), mais je ne peux pas écrire f (g, 0). Ce dernier est appelé «fonctionnel» et appelle des règles différentes.
Cort Ammon - Rétablir Monica
Les fonctions @CortAmmon sont des fonctions. Une fonction est juste un ensemble de paires (bien que, à proprement parler, c'est un triple (D, R, G) où D est le domaine R est la plage et G est le graphique (ensemble de paires), un autre petit problème que j'ai avec la réponse acceptée, mais ce n'est ni ici ni là). Donc, si D est un ensemble de fonctions et que vous prenez des paires où le premier élément est une fonction dans D, alors vous avez une fonction. Consultez Wikipédia: "Une fonctionnelle est une cartographie [fonction] ..."
Neil
C'est-à-dire que toutes les fonctions sont des fonctions, toutes les fonctions ne sont pas des fonctions. Mais toutes les règles qui s'appliquent aux fonctions s'appliquent aux fonctionnelles
Neil

Réponses:

63

Ironiquement, le titre est sur le point mais pas de la façon dont vous semblez le dire, qui est "le lambda calcul n'est-il qu'une convention de notation" qui n'est pas exacte.

Les termes lambda ne sont pas des fonctions 1 . Ce sont des morceaux de syntaxe, c'est-à-dire des collections de symboles sur une page. Nous avons des règles pour manipuler ces collections de symboles, notamment la réduction bêta. Vous pouvez avoir plusieurs termes lambda distincts qui correspondent à la même fonction. 2

J'aborderai vos points directement.

Premièrement, lambda n'est pas un nom qui est réutilisé. Non seulement cela serait extrêmement déroutant, mais nous n'écrivons pas (ou ), ce que nous ferions si était le nom d'une fonction, tout comme nous écrivons . Dans nous pourrions remplacer (s'il était défini par un terme lambda) par le terme lambda produisant quelque chose comme signifiant est une expression qui peut représenter une fonction, non une déclaration déclarant une fonction (nomméeλ(x)(λ x)λf(x)f(x)f(λy.y)(X)(λy.y)λou autre chose). En tout cas, lorsque nous surchargeons la terminologie / notation, c'est (on l'espère) fait d'une manière où cela peut être désambiguïsé par le contexte, ce qui ne peut certainement pas être le cas pour les termes lambda.

Votre point suivant est bien, mais quelque peu hors de propos. Ce n'est pas une compétition où il y a des termes et des fonctions d'équipe Team Lambda, et un seul peut gagner. Une application majeure des termes lambda est l'étude et la compréhension de certains types de fonctions. Un polynôme n'est pas une fonction bien que nous les identifiions souvent de manière bâclée. L'étude des polynômes ne signifie pas que l'on pense que toutes les fonctions devraient être des polynômes, ni que les polynômes doivent "faire" quelque chose de "nouveau" pour être étudiés.

Les fonctions théoriques d'ensemble ne sont pas des boîtes noires, bien qu'elles soient entièrement définies par leur relation entrée-sortie. (Ils sont littéralement leur relation entrée-sortie.) Les termes lambda ne sont pas non plus des boîtes noires et ils ne sont pas définis par leur relation entrée-sortie. Comme je l'ai mentionné précédemment, vous pouvez avoir des termes lambda distincts qui produisent la même relation entrée-sortie. Cela souligne également le fait que les termes lambda ne peuvent pas être des fonctions, bien qu'ils puissent induire des fonctions. 2

En fait, l'analogie entre les polynômes et les termes lambda est très proche, et je soupçonne que vous n'apprécierez peut-être pas la distinction entre un polynôme et la fonction qu'il représente, alors je vais développer un peu. 3 Généralement, lorsque des polynômes sont introduits, généralement avec des coefficients réels, ils sont traités comme des fonctions réelles d'un type particulier. Considérons maintenant la théorie des registres à décalage à rétroaction linéaire (LFSR). C'est en grande partie la théorie des polynômes (univariés) sur F2 , mais si nous considérons cela comme une fonction F2F2 , alors il y a au plus 4 ces fonctions. Il existe cependant un nombre infini de polynômes sur F2 . 4Une façon de voir cela est que nous pouvons interpréter ces polynômes comme autre chose que des fonctionsF2F2 , en fait n'importe quellealgèbreF2 fera l'affaire. Pour les LFSR, nous interprétons couramment les polynômes comme des opérations sur les flux binaires, qui, si nous le voulions, pourraient être représentés comme des fonctions2N2N , bien que la grande majorité de ces fonctions ne soient pas à l'image de l'interprétation d'un LFSR.

Cela s'applique également aux termes lambda, nous pouvons les interpréter comme des choses autres que des fonctions. Ils sont également à la fois des objets beaucoup plus maniables que les ensembles de fonctions infiniment typiques. Ils sont tous deux beaucoup plus calculatoires que des fonctions arbitraires. Je peux écrire un programme pour manipuler des polynômes (avec des coefficients qui sont au moins représentables par calcul) et des termes lambda. En effet, les termes lambda non typés sont l'un des modèles originaux de fonctions calculables. Cette perspective plus symbolique / syntaxique, calculatrice / computationnelle est généralement plus soulignée, en particulier pour le calcul lambda non typé, que les interprétations plus sémantiques du calcul lambda. TapéLes termes lambda sont des choses beaucoup plus faciles à gérer et peuvent généralement (mais pas toujours) être facilement interprétés comme des fonctions théoriques définies, mais peuvent également généralement être interprétés dans une classe de choses encore plus large en plus des fonctions que le calcul lambda non typé. Ils ont également une riche théorie syntaxique qui leur est propre et un lien très profond avec la logique .

1 Il est possible que le problème aille dans l'autre sens. Vous avez peut-être une mauvaise compréhension de ce qu'est une fonction.

, et pour la catégorie des ensembles, il n'y a pas d'objets réflexifs non triviaux. L'histoire est assez différente pour les termes lambda typés , mais peut toujours être non triviale.

3 Si vous êtes clair sur cette distinction, alors l'analogie devrait être assez informative.

4 Ce problème ne se produit pas avec les champs de caractéristique 0, comme les nombres complexes, les réels, les rationnels ou les entiers, de sorte que la distinction n'est pas aussi nette, bien qu'elle existe toujours.

Derek Elkins
la source
8
C'est une réponse incroyable que je dois juste dire. Élimine vraiment de longs malentendus pour moi. Merci!
the0ther
4
J'aimerais pouvoir y répondre en détail! Beaucoup de choses que j'aimerais suivre. Dans l'ensemble, cela m'a été très utile, et apparemment aussi à quelques autres personnes, alors merci pour la réponse approfondie et réfléchie.
Neil
1
Il y a juste un point que je conteste ici, c'est votre affirmation selon laquelle les polynômes n'ont pas à "faire" quelque chose de "nouveau" pour être étudiés. Bien sûr qu'ils le font! Bien sûr, selon votre domaine, "nouveau" peut avoir différentes significations (par exemple, un mathématicien pur ne fera pas de distinction entre les vecteurs de colonne et les vecteurs de ligne car ils sont isomorphes, mais un statisticien peut considérer la distinction comme utile à des fins de calcul). Tout nouveau formalisme doit se justifier.
Neil
2
@Neil: La note de bas de page n ° 2 en particulier offre des preuves très claires que le calcul lambda "fait quelque chose de nouveau" que les fonctions "régulières" "ne peuvent pas faire". Pour un exemple plus concret d'une expression lambda non fondée, voir Combinateurs à virgule fixe . Les chiffres de l'Église rendent également la lecture fascinante, en particulier la fonction précédente.
Kevin
1
J'ajouterais que les lambdas en tant que fonctions ne font rien d'utile. La seule chose que vous pouvez faire avec un lambda est de lui passer un lambda et il retourne un lambda. Vous n'avez aucun moyen de tester ce que fait le lambda résultant. Vous pouvez seulement lui passer un autre lambda pour obtenir un autre lambda en retour. En tant que fonctions, l'ensemble des "fonctions lambda" se comporte exactement comme un ensemble singleton contenant uniquement la fonction d'identité. Ce n'est qu'en considérant l'entrée et la sortie d'un lambda comme des expressions que vous pouvez différencier les lambdas.
Florian F
0

Pensez au concept de variables. Dans les anciennes langues comme basic, vous n'aviez pas d'allocation dynamique et vous aviez besoin d'un nom pour chaque variable. (Ce n'est pas parfaitement exact car vous aviez des tableaux, mais l'idée est que ...) dans de nombreux problèmes, vous devez être en mesure d'allouer autant de variables que vous le souhaitez, sans être limité par le nombre de noms définis par votre programme.

Les fonctions lambda vous permettent de vous débarrasser de la même limitation concernant les noms de fonctions, permettant à votre programme de définir autant de fonctions qu'il en a besoin et de les "stocker" dans les mêmes structures de données complexes que les autres variables. Ce n'est pas quelque chose que vous pourriez faire avec des fonctions nommées conventionnelles.

Camion
la source
Pourquoi ne puis-je pas faire cela avec des fonctions nommées conventionnelles? Si j'écris f(x)=let g(y)=x+y in g, chaque mathématicien saura instantanément ce que l'on veut dire et conviendra qu'il s'agit d'un objet mathématique raisonnable (peut-être jusqu'à quelques chicanes sur la clarté du domaine de f). Ils seront également parfaitement heureux si j'écris ensuite l'ensemble {f(n) | n ∈ ℕ}, qui contient une infinité de fonctions et, en particulier, n'est pas limité par un nombre limité de noms à utiliser.
Daniel Wagner
La question concerne le calcul lambda. Bien que liés, ce n'est pas la même chose que les fonctions lambda dans les langages de programmation.
Andy Dent