Как я ошибаюсь в оценке по требованию?

Question

Прежде всего, я никогда не изучал эти вещи или что-то в этом роде, поэтому я могу задавать очень глупые вопросы, о которых я сожалею, но, пожалуйста, пройдите ко мне :)

Я играю с внедрением лямбда-исчисления , с оценкой по требованию. Я пытаюсь следовать this paper по этому вопросу, где соответствующий бит представляется естественной семантикой, описанной на странице 28.

В любом случае, что я не понимаю об этой стратегии оценки, так это, насколько я понимаю , фактическая подстановка происходит только при оценке переменных. Абстракции оценивают сами по себе, так как это значения, а приложения только добавляют новые записи в кэш.

Но если учесть, что, как именно можно идти о оценке термина как

(λx.λy.x y) λa.a

Согласно естественной семантике, описанной в связанном документе, первым шагом оценок можно был бы добавить запись x -> λa.a к кеш и оценить тело абстракции на приложениях, которое равно λy.x y. Но это значение, поэтому оценка заканчивается. В этот момент мы имеем не закрытый, а непустую кучу. Хотя мы точно знаем, что этот термин должен оцениваться до λy.(λa.a) y.

Что я не понимаю? Как это работает на языках, которые фактически используют эту стратегию оценки?

Answer 1

Ваше сокращение - это правильно. Дело в том, что стратегия вызова по необходимости, рассматриваемая в этой статье, является лишь слабой стратегией, в том смысле, что она никогда не будет уменьшаться при выражении лямбда. Это видно на рис.1, где выражение \ x.M является значением.

В конце редукции, если вы хотите явно получить лямбда-код, вам все равно необходимо развернуть кеш (часто называемый средой в литературе), что сводится к замене ассоциаций в кеше внутри вашего термина:

   λy.x y [x -> λa.a] = λy.(λa.a) y 

как ожидалось.