comment contrôler l'ordre d'évaluation en appel par valeur?

Question

J'ai quelques questions sur l'appel par valeur lambda calcul.

1) λx. (Λy.y) x est un terme bloqué ou doit être évalué à λx.x?

2) λx. (Λy.y) (λz.z), qu'en est-il de celui-ci?

3) comment contrôler l'ordre d'évaluation en implémentation?

Je me sens très confus, pourrait-on expliquer cette valeur, terme bloqué, ordre d'évaluation, comment contrôler?

Merci d'avance!

Answer 1

1) λx. (Λy.y) x est un terme bloqué ou doit être évalué à λx.x?

Il peut être utile de penser en termes de termes et de sous-termes. Ici, nous avons:

• Une abstraction, & lambda; (& lambda; y.y) x, avec:
  • une application (& lambda; y.y) x, qui applique
    • & lambda; y.y (une abstraction, avec le simple terme y)
    • x.

Les applications peuvent être transformés, par conséquent, nous obtenons:

• Une abstraction, & lambda; x. x, puisque l'application réécrit à x. Ceci est également écrit comme le combinateur I.

& lambda; x (& lambda; y.y) x est pas un terme bloqué. Un terme est bloqué ssi il ne peut pas être transformé.

2) λx. (Λy.y) (λz.z), qu'en est-il de celui-ci?

Idéalement, vous essayez maintenant de le faire vous-même.

Nous avons:

• Une abstraction, & lambda; x. (& lambda; y.y) (& lambda; z.z), avec:
  • Une application, qui applique
    • L'abstraction & lambda; y.y à
    • L'abstraction & lambda; z.z.

Nous pouvons transformer l'application en utilisant y = (& lambda; zz) et obtenez: & lambda; x (& lambda; zz), qui peut être raccourci à & lambda; xz.z ou . K *.

3) comment contrôler l'ordre d'évaluation en implémentation?

Vous ne pouvez pas. Lambda calculus ne le définit pas. C'est un modèle de calcul, pas un langage de programmation. Puisque le lambda-calcul est confluent, toute évaluation d'un terme donnera la même forme normale si elle donne une forme normale. En d'autres termes, chaque terme a au plus une forme normale, mais des chemins d'évaluation infinis peuvent exister.

Le terme KI Ω, par exemple, a un chemin de réduction infinie car il réduit à lui-même (en réduisant Ω ≡ ω ω ≡ (& lambda; z.zz) (& lambda; z.zz) lui-même), alors qu'il peut également être réduit à I en appliquant K ≡ & lambda xy.x. Par conséquent, l'astuce dans un langage basé sur le lambda-calcul est de choisir une stratégie d'évaluation qui donnera une forme normale si elle existe. La stratégie la plus élémentaire est la stratégie "leftmost outermost", également appelée évaluation d'ordre normal, qui sélectionne toujours le plus à gauche & lambda; abstraction qui peut être appliquée. Il est inefficace, mais garantit une forme normale s'il en existe une.

Dans les langages de programmation, des astuces doivent être appliquées pour rendre l'évaluation plus efficace. Le plus souvent, cela comprend strictness analysis et graph rewriting.