Quel est l'intérêt d'appeler -calculus une algèbre?

Quelle est la différence d'appeler -calculus une algèbre au lieu d'un calcul? Je pose cette question parce que j'ai lu quelque part la ligne « -calculus n'est pas un calcul mais une algèbre» (iirc, attribué à Dana Scott). Dans quel but? Merci.$\lambda$$\lambda$

Un calcul est un système de calcul basé sur la manipulation d'expressions symboliques. Une algèbre est un système d'expressions symboliques et de relations entre elles [*]. Autrement dit, un calcul est un système pour trouver des réponses, et une algèbre est un moyen d'exprimer les relations entre les termes.

Le -calcul est soit un calcul, soit une algèbre, selon que vous voulez considérer les règles β et η comme des règles de réduction orientées ou des équations non orientées. Si vous pensez que les règles sont orientées, vous avez fixé un ordre d'évaluation et les règles vous indiquent comment prendre un terme et produire une forme normale. Si vous pensez que les règles ne sont pas orientées, elles vous donnent la relation d'égalité sur les termes λ .$\lambda$$\beta$$\eta$$\lambda$

[*] Il existe également une définition catégorique de l'algèbre, qui est une définition formelle quelque peu plus restrictive que l'idée informelle. En gros, la différence est que la définition formelle de l'algèbre englobe uniquement les systèmes sans liaison variable. Les combinateurs SKI forment donc une algèbre, mais pas le -calculus.$\lambda$

Traditionnellement, une algèbre est un ensemble de porteuses dont les opérations satisfont certaines équations (pensez «groupe»). Il existe de nombreuses façons de généraliser la notion:

• les algèbres multi-triées ont plusieurs ensembles de supports. Un exemple serait un module sur un anneau R , où nous voulons considérer le tout comme une seule algèbre. Un autre exemple, assez stupide, est un graphe orienté, qui a deux ensembles de porteurs, E des arêtes et V des sommets, et deux opérations, source s : E → V et cible E → V , ne satisfaisant à aucune équation.$M$$R$$E$$V$$s : E \to V$$E \to V$

• des axiomes plus généraux qui ne sont pas de simples équations peuvent être autorisés. Par exemple, les axiomes d'un champ sont toutes des équations à l'exception de . Un autre exemple est quelque chose comme un domaine intégral.$x \neq 0 \implies x \cdot x^{-1} = 1$

• des opérations plus générales peuvent être autorisées, en particulier celles d'arité infinie, ou des opérations d'ordre supérieur qui prennent des fonctions comme arguments. Un exemple d'une opération infinitaire est le dans les algèbres médianes de Martin Escardo et Alex Simpson. Si vous allez loin dans cette direction, vous arrivez à des monades.$M$

En ce sens, le -calculus non typé est une algèbre car il est spécifié en termes d'un ensemble de porteuses avec certaines opérations (d'ordre supérieur) satisfaisant certaines équations ( β et η ).$\lambda$$\beta$$\eta$

Il existe une définition assez précise de ce qu'est une algèbre dans la théorie des catégories: voir cet article par exemple. Il a fallu quelques années pour comprendre comment une structure avec des variables liées pouvait être comprise dans le même contexte que le terme structure d'algèbre couramment utilisé en mathématiques et en informatique, et il s'avère que le concept catégorique d'algèbres F est capable d'unifier deux. Je ne suis pas sûr des aspects historiques de la solution, mais une approche possible est que les algèbres pré-en-cas introduites par Fiore, Plotkin et Turi (disponibles ici ) ont réglé la question et encouragé des approches différentes mais similaires, voir par exemple Hirshowitz et al. et son doctorante Julianna Zsido .

Il reste à faire des recherches sur la façon d'utiliser les concepts catégoriels pour refactoriser et approfondir notre compréhension des structures avec des variables liées, dans l'espoir d'éliminer la "cruft" syntaxique qui comprend généralement les chapitres les plus ennuyeux des thèses sur -calculi et connexes structures.$\lambda$

S'il est vrai que la notion de "calcul" est moins bien définie que la notion d '"algèbre", généralement le "calcul" implique généralement un processus de calcul, tandis que les algèbres ont des schémas de construction avec des théories équationnelles.
On pourrait dire qu'il y a plus un sentiment que les algèbres "existent déjà" en tant que structures et que nous découvrons simplement des vérités à leur sujet, plutôt que d'utiliser une méthode pour produire de nouvelles réponses qui n'existaient pas auparavant.

Si vous pensez à ce que Scott essayait d'accomplir avec les domaines Scott, sa déclaration est logique: il essayait de trouver des structures mathématiques et algébriques prédéfinies qui serviraient de sémantique fixe pour LC. Il voulait supprimer le sentiment que le sens d'un terme était tout ce qui arrivait d'un processus particulier.

Vous pourriez être intéressé par une réponse précédente à une question connexe: Qu'est - ce qui constitue la sémantique dénotationnelle?

$\beta$$\eta$$M$$N$

Si Scott avait jamais appelé le calcul lambda une "algèbre" (ce dont je doute plutôt), alors il aurait fait un point assez subtil, à savoir que vous pouvez penser au calcul lambda comme ayant une signification a priori .

Pourtant, il aurait du mal à convaincre les algébriques de sa prétention, car il n'a pas d'équations dans le calcul lambda, il a des équivalences (c'est-à-dire au niveau méta). "L'algèbre combinatoire", en revanche, est parfaitement normale.

Le calcul n'existe pas, mais il existe un objet mathématique bien défini appelé algèbre , bien que le mot ait de nombreuses utilisations . Cependant, je suppose que le nom a été donné dans le sens de

(...) l'étude abstraite des systèmes de numérotation et des opérations en leur sein.

$\lambda$