Quelle est la différence entre les stratégies de réduction et les stratégies d'évaluation?

Extrait de l' article sur la stratégie d'évaluation sur Wikipédia:

La notion de stratégie de réduction dans le calcul lambda est similaire mais distincte.

Extrait de l' article sur la stratégie de réduction sur Wikipédia:

Elle est similaire mais subtilement différente de la notion de stratégie d'évaluation en informatique.

Quelle est la distinction subtile entre les stratégies d'évaluation et les stratégies de réduction à laquelle ces deux articles font allusion? S'agit-il seulement de deux concepts similaires de domaines différents?

Une stratégie de réduction est une fonction sur Lambda qui sélectionne un redex (expression réductible) parmi tous les redex possibles - selon ce que vous définissez comme un redex.

De manière informelle, une stratégie d'évaluation est l'ordre dans lequel une langue évalue ses arguments. Une stratégie de transfert de paramètres est ce que le langage remet à la fonction.

Pour comprendre le lien entre ceux-ci, étudiez l'article de Plotkin sur Appel par nom, appel par valeur et le calcul lambda. Il précise clairement que vous souhaitez choisir des AXIOMES distincts en fonction de l'ordre d'évaluation que vous souhaitez. Pour le nom Cb, vous voulez l'ancien axiome bêta et pour la valeur cb, vous voulez un axiome bêta. Si vous faites cela, tous les méta-théorèmes fonctionnent de la même manière pour les deux saveurs. J'ai montré plus tard (avec de nombreux collaborateurs) que cette idée se généralise à tout ce que le monde du PL a étudié.

Tout est technique, pas un poème qui puisse être interprété. Lisez-le.

- Matthias Felleisen

ps Je dirai que je pense que les gens auront plus de facilité à comprendre le papier de Plotkin de la partie I de notre livre Redex. Mais oui, c'est 3 fois plus long.

L'article wikipedia "Stratégie de réduction" est entièrement extrait d' une édition particulière effectuée par une adresse IP anonyme vers l'article "Stratégie d'évaluation".

L'opinion qu'elle représente n'est pas consensuelle, dans le sens où je soupçonne que relativement peu de personnes sur le terrain donneront spontanément cette réponse si vous leur demandez "distingueriez-vous les noms" stratégie de réduction "et" stratégie d'évaluation "?". Je ne l'ai entendu de Matthias Felleisen, qui est catégorique quant à l'importance de cette distinction - et je suppose que ce point de vue est partagé par d'autres qui ont eu la chance de prendre le temps de discuter de ces points en détail avec lui.

Ma compréhension actuelle de ce point (mais je n'ai pas encore étudié les détails techniques à leur juste mesure) concerne les points suivants: il s'agit de savoir si vous utilisez la sémantique "grand pas" par rapport à "petite étape" - cette distinction est standard et comprise par tout le monde sur le terrain. La sémantique des petits pas définit une étape atomique de réduction, et le résultat est en général encore réductible. La sémantique à grandes étapes définit une «grande» étape de réduction qui va du programme de démarrage à sa valeur (ou un type de «réponse» plus riche si votre langue a d'autres effets observables que le retour d'une valeur, par exemple, entrée / sortie ou état mutable).

Si vous définissez à la fois une relation à grand et à petit pas, vous pouvez vérifier que la sémantique à grand pas est incluse dans la fermeture transitive de la relation à petit pas, et que la relation à petit pas ne se réduit pas à d'autres termes bloqués que celles atteintes par la relation à grand pas, ou divergent si la réduction à grand pas est définie. Il s'agit de la relation de cohérence attendue entre les deux.

Je pense que le libellé de l'article peut être plus ou moins décrit, en termes modernes, comme «la stratégie d'évaluation est la relation à grand pas», «la stratégie de réduction est la relation à petit pas». Notez que la discussion faite dans l'article "Stratégie de réduction" concerne principalement des articles et des recherches (et, plus important encore, des points de vue éloquents formés au cours de leur lecture et de leur écriture) entre 1973 et 1991, à une époque où ces notions venaient de naître, et probablement pas aussi bien compris qu'aujourd'hui. (La sémantique des grands pas a été soulignée par Kahn en 1987, et l'un des travaux les plus importants sur la sémantique des petits pas est Wright et Felleisen, 1992)

Pour le côté le plus opiniâtre de la raison pour laquelle Felleisen insiste sur l'importance de cette différence (c'est-à-dire pourquoi il peut y avoir plus que juste "petit pas contre grand pas, meh"), ma compréhension actuelle est la suivante: le ce qui est fait est que la sémantique à petits pas doit être considérée comme un détail d'implémentation. lela sémantique, selon cet argument, est la fonction abstraite qui mappe chaque programme à sa valeur / réponse, et les autres sont des dispositifs d'implémentation conçus pour l'approcher (ou raisonner sur l'équivalence induite par cette sémantique). Quand nous disons grand pas aujourd'hui, nous pensons à un système de règles d'inférence de nature syntaxique, mais la "stratégie de réduction" qui est discutée ci-dessus est en fait son abstraction comme cartographie. (Je ne pense pas que cela donne plus d'expressivité ou de force à la notion dans la pratique, mais cela la rend plus abstraite.)

Je pense donc que ce que cette page de wikipedia et Matthias Felleisen disent est quelque chose comme: "Définissez votre évaluation comme bon vous semble, mais en fin de compte, ce qui compte, c'est la façon dont vos programmes sont mis en correspondance avec leurs valeurs / réponses / comportements, et c'est ce qui devrait être appelé "sémantique opérationnelle" et motivé. ".

Notez que cette position va quelque peu à l'encontre de la distinction actuelle (qui je pense est plutôt consensuelle, mais cela peut être un parti pris culturel de ma part) entre la "sémantique opérationnelle" et la "sémantique dénotationnelle", où la première est considérée comme de nature plus syntaxique. (définie comme une relation de réduction), et cette dernière est typiquement caractérisée par le fait que les programmes équivalents en termes de calcul ont exactement la même dénotation (de sorte que la dénotation est inconsciente du mécanisme de calcul réel). Selon ce dernier point de vue, ce qui est proposé comme une "stratégie d'évaluation" ou une "sémantique opérationnelle" dans les articles et mon explication ci-dessus seraient plutôt considérés comme une sémantique dénotationnelle - mais certes plus concrète que la plupart: valeurs / réponses / les comportements sont plus proches des objets syntaxiques que de nombreux domaines sémantiques.

Références: pour comprendre ce point de vue, il est probablement utile de revenir à sa source proclamée, qui est l'article de Gordon Plotkin en 1973. Vous pouvez également avoir de la chance en essayant l'un des derniers articles cités sur wikipedia; J'ai trouvé par exemple que "Parameter-Passing and the Lambda Calculus", par Crank et Felleisen, 1991, a donné un aperçu très clair de leur position sur la question dans les premières pages.