Pourquoi la stratégie d'évaluation par appel d'offres n'est-elle pas complète?

Question

Je suis en train de lire un article sur différents evaluation strategies (j'ai lié un article dans le wiki, mais je suis en train de lire un autre article en anglais). Et il dit que, contrairement aux stratégies call-by-name et call-by-need, stratégie call-by-value est pasTuring complete.

Quelqu'un peut-il expliquer, s'il vous plaît, pourquoi est-ce le cas? Si c'est possible, ajoutez un exemple de pls.

Answer 1

Je conteste la revendication dans l'article que vous êtes en train de lire. (Je ne suis pas payé pour cela, donc je vais fournir un argument suggestif, pas une preuve.)

Il est bien connu que, au moins sous la réduction d'ordre normal (alias appeler par son nom), le calcul lambda pur est Turing-complet. Mais si nous regardons l'article séminal de John Reynolds Definitional Interpreters for Higher-Order Programming Languages, nous pouvons voir que Reynolds discute longuement la différence entre appel par nom et appel par valeur. Une partie critique de l'argument est que, afin de faire une distinction appropriée, nous pouvons transformer un programme en continuation-passing style. La transformation CPS est différente pour l'appel par besoin et appel par valeur, mais les termes transformés résultants peuvent être évalués dans l'un ou l'autre style. Voici donc l'argument: écrire un programme lambda-calcul qui simule une machine de Turing, puis CPS le transforme en utilisant la transformée CBN, et vous pouvez évaluer le code résultant en utilisant une stratégie de réduction CBV. Coup! Turing-complet. En pratique, je parie que vous pouvez écrire un programme CBV pour émuler une machine de Turing; il suffit probablement de choisir un combinateur à virgule fixe approprié, par exemple Θ. (Plus célèbre Y Combinator ne fonctionne que lors d'un appel par nom stratégie de réduction, par exemple, la réduction d'ordre normal.)

Avertissement: Je n'ai pas étudié le calcul lambda dans les âges, et je suis sûr qu'il sont plusieurs détails erronés dans l'argument ci-dessus. Mais je suis confiant dans la substance. Ce ne serait pas la première fois que je repèrerais quelque chose de manifestement faux dans les ressources en ligne sur la théorie du langage de programmation.

Answer 2

Votre question n'a pas beaucoup de sens sans référence à un langage spécifique, mais je ferai de mon mieux pour répondre à la question concernant le calcul Lambda non typé. L'existence d'un combinateur point par point à valeur fixe (c'est-à-dire "combinateur Y") pour le calcul lambda non typé semble réfuter la revendication de base (voir: Fixed Point Combinator). L'existence d'un tel combinateur rompt une normalisation forte, ce qui suggère qu'il existe au moins un langage qui soit complet et qui utilise une stratégie d'évaluation appel par valeur.

L'existence (ou l'absence) d'un système de types est beaucoup plus susceptible d'affecter la complétude d'un langage. Par exemple, le lambda-calcul simplement typé ne peut pas coder un combinateur à point fixe et est fortement normalisant (c'est-à-dire que tous les termes bien typés se réduisent à une valeur), ceci indépendamment de la stratégie d'évaluation employée. Au contraire, c'est une conséquence du système de type.