Семантика отношений сокращения вызова по необходимости и вызова по имени

Пытаясь обобщить свои знания о лямбда-исчислении, я понял, что хорошо знаком с вызовом по значению, но никогда не видел семантики сокращения вызова по необходимости. Я знаю определение, но было бы здорово увидеть точное значение.

Вот что у меня есть для call-by-need и call-by-value (не очень подробное описание):

Вызов по значению

Маленький шаг

• Ценности

  

• β-восстановление

  

• Контекст оценки

  

  

Большой шаг (с замыканиями и окружением)

• Закрытия

  

• Окружающая среда

  

• Снижение

  

  

  

Вызов по имени

Маленький шаг

• β-восстановление

  

• Контекст оценки

  

  

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

Так что я буду признателен, если кто-то может расширить мой список с вызовом по необходимости.