Подстановка без захвата: поддельная доверенность

Агата Сомова · старший инспектор

Рудаков подписал строку ЗАВЕРИТЬ y, где y это он сам, подписант. В приложении конторы Вельского: ЗАВЕРИТЬ = λx. λy. x. А на ленте, которую подали в машину, стоит λy. y. Писарь клянётся, что просто раскрыл сокращение. Раскрой сам и скажи, та ли это бумага.

Доверенность нужна, чтобы кто-то заполнил поле дела от имени подписанта. В деле склада это поле «сколько ящиков недостаёт», и в боссе G ты видел, что в нём оказалось «да/нет». Как именно заполнять, сказано в строке, которую подписал Рудаков. Контора Вельского переписала эту строку на перфоленту, «раскрыв сокращения», и подала ленту в Арбитр. Допуск, который не пустил бы в машину дело с «да/нет» в числовом поле, шесть лет как отключён.

В уроке 12 Костя разбирал протокол «он сказал, что он был на складе» и мы встретили захват: подставленное имя попало под чужой квантор и поменяло смысл формулы. В λ-исчислении вычисление целиком состоит из подстановок, поэтому захват здесь опаснее. Сегодня определяем подстановку для λ-термов так, чтобы захват был невозможен, и проверяем, что сделал писарь.