Tout d'abord, je n'ai jamais étudié ces choses ou quoi que ce soit d'autre, il se peut donc que je pose des questions très idiotes, ce dont je suis désolé, mais je vous en prie, soyez indulgents avec moi :)
Je suis en train de jouer avec l'implémentation du calcul lambda, avec une évaluation appel par appel. J'essaie de suivre ce document sur le sujet, où la partie pertinente semble être la sémantique naturelle décrite à la page 28.
Quoi qu'il en soit, ce que je ne comprends pas dans cette stratégie d'évaluation, c'est que, d'après ce que j'ai compris, la substitution réelle n'a lieu que lors de l'évaluation des variables. Les abstractions s'évaluent elles-mêmes, puisque ce sont les valeurs, et les applications ne font qu'ajouter de nouvelles entrées au cache.
Mais dans ces conditions, comment évaluer exactement un terme tel que
(λx.λy.x y) λa.a
Selon la sémantique naturelle, décrite dans l'article en lien, la première étape de l'évaluation consisterait à ajouter l'entrée x -> λa.a vers le cache, et évaluer le corps de l'abstraction sur la partie lhs de l'application, qui est λy.x y . Mais comme il s'agit d'une valeur, l'évaluation se termine. À ce stade, nous avons un terme qui n'est pas fermé et un tas non vide. Bien que nous sachions exactement que ce terme devrait s'évaluer à λy.(λa.a) y .
Qu'est-ce que je comprends mal ? Comment cela fonctionne-t-il dans les langues qui utilisent réellement cette stratégie d'évaluation ?
