β-редукция и стратегии: поручение, которое не кончается

Костя · стажёр, Седьмой отдел

Смотри, что Тимофей Ильич принёс: (λx. x x) (λx. x x), и приписка «это поручение машина будет выполнять вечно». Может, Арбитр на таком и завис? Вельский подсунул ему вечное поручение, машина думает до сих пор, а мы ищем захваты.

Хорошая версия, и проверить её можно. В уроке 43 мы вычисляли термы на глаз: «впиши во все места». В уроке 44 узнали, как вписывать без захвата. Теперь соберём из этого настоящее правило вычисления и посмотрим, что бывает, когда в терме несколько мест, где можно вписывать. Выяснится, что от порядка зависит, кончится ли вычисление вообще.