Кодировки Чёрча: числа и «да/нет» из одних функций

Тимофей Ильич · архивариус

Вот, сто тридцатая страница. Подпись внизу: «итого ключей», а рядом λs. λz. s (s z). Ниже «подтверждено» и λt. λf. t. Ни одной цифры, ни одного «да». Она что, считала одними бланками?

Считала. В уроке 43 мы заметили, что в λ-исчислении нет ни чисел, ни «да/нет», ни if. Есть только бланки и вписывание. Алонзо Чёрч в 1930-х показал, что этого хватает: число, «да», «нет», пару можно записать бланком так, что вычисление по правилам урока 45 будет работать как арифметика и логика. Такие записи называют кодировками Чёрча, и это и есть шифр Арбениной.

Главная мысль урока: значение в λ-исчислении определяется не тем, как оно выглядит, а тем, что оно делает, когда его применяют.