Значения и застрявшие термы: у зависания есть имя

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

Вот последняя запись на табло в ночь зависания: if iszero (pred (succ true)) then false else true. Это не «виновен» и не «невиновен». Механик клянётся, что ни одна статья к ней не подходит, поэтому машина и встала. Вельский говорит: раз шагать некуда, это и есть окончательный ответ, просто непривычный. Окончательный ответ это или нет?

Чтобы спорить с Вельским, нужны точные слова. «Машина остановилась» бывает двух видов, и снаружи они выглядят одинаково. Сегодня разделим их, дадим им имена из TAPL и докажем, что у Арбитра нет выбора, куда шагнуть. Тогда зависание дела склада перестанет быть загадкой и станет фактом, у которого есть название.