Простое типизированное λ-исчисление: ярлык для поручения

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

С числами и «да/нет» понятно: у улики ярлык, и Допуск сверяет ярлыки. Но на этой странице поручения: $\lambda x:\text{Bool}.\dots$, $\lambda f:\text{Bool}\to \text{Bool}.\dots$. Поручение само ничего не хранит, оно что-то делает с уликой, которую ему дадут. Какой ярлык у того, что делает? И как проверить x, если неизвестно, что в него положат?

В блоке H ты расшифровал вторую половину блокнотов: поручения машине записаны λ-термами, и машина выполняет их подстановкой. Тогда у поручений не было ярлыков, и любой терм шёл в работу. Именно так поддельная доверенность и дошла до вычислителя.

На этой странице Арбенина добавляет ярлыки к поручениям. Получается язык, который TAPL называет простым типизированным λ-исчислением, и именно его правила набраны на первой странице Кодекса. После этого урока ты прочтёшь там почти каждую строку.