Lambda Calculus est-il purement syntaxique?

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.

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 ¹ . 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. ²

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$\lambda(x)$$(\lambda\ x)$$\lambda$$f(x)$$f(x)$$f$$(\lambda y.y)(x)$$(\lambda y.y)$$\lambda$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. ²

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. ³ 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 $\mathbb F_2$ , mais si nous considérons cela comme une fonction $\mathbb F_2\to\mathbb F_2$ , alors il y a au plus $4$ ces fonctions. Il existe cependant un nombre infini de polynômes sur $\mathbb F_2$ . ⁴Une façon de voir cela est que nous pouvons interpréter ces polynômes comme autre chose que des fonctions$\mathbb F_2\to\mathbb F_2$ , en fait n'importe quellealgèbre$\mathbb F_2$ 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 fonctions$\mathbf{2}^{\mathbb N}\to\mathbf{2}^{\mathbb N}$ , 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 .

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

$D$$D$$D$$D^D\subseteq D$, 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.

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

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

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.