Как я неправильно понимаю оценку по требованию?

Question

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

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

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

Но, учитывая это, как именно можно оценить термин, как

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

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

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

Answer 1

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

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

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

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