Агата Сомова · старший инспектор
Видел табло? Дерево меняется по кусочку, и под каждой сменой машина печатает в журнал короткое слово:
E-If,E-IfTrue,E-PredSucc. Механик говорит, это номер статьи, по которой сделан шаг. Если так, каждый шаг можно проверить, как приговор. Научись читать эти статьи. Вельский спросит про каждый шаг: «по какому праву?»
Арбитр не выносит вердикт одним махом. Он переписывает дерево дела маленькими кусками, и каждая перезапись разрешена одним правилом. Список этих правил в TAPL занимает полстраницы: рис. 3-1 для «да/нет» и рис. 3-2 для чисел. Сегодня прочитаем их все вслух и напишем на Haskell функцию, которая делает ровно один такой шаг.
Это называется операционной семантикой: смысл программы задают тем, как машина её выполняет.
урок из курса
Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.
Оплата пока не подключена: премиум и курсы открываются промокодом.