Функции и выражения также называются термами. Термы состоят из объявлений λ-функций (абстракций), применений λ-функций (аппликаций), а также переменных.
Если переменная относится к аргументу какой-то λ-функции внутри терма, то такая переменная называется связанной. Иначе, если она не привязана к какой-либо λ-функции в рассматриваемом терме, она называется свободной переменной.
Особый интерес в λ-исчислении представляют замкнутые термы (или комбинаторы). Комбинатор — терм, у которого нет свободных переменных, который не ссылается ни на что извне. Например, \f. f x — не комбинатор, а \x. \f. f x — комбинатор.
Есть еще один важный вопрос, который мы не обсудили: в каком порядке применять β-редукции. Очевидно (и доказывается), что если к какому-либо выражению попробовать в разном порядке применить β-редукции для сведения его к β-нормальной форме, то получится одно и то же (с точностью до названия переменных). Единственный вопрос — не уйдем ли мы в какой-то момент бесконечный цикл, и зависит ли это от порядка вычислений.
Порядок вычислений проще всего представить себе так. Представьте, что вы пишете программу на каком-то классическом языке программирования, вроде C++ или Python, и у вас там написано f(g()). Тогда сначала вычислится значение g(), а затем результат подставится в качестве аргумента для f.
А можно считать не так, а представить, что вы пытаетесь оптимизировать математическое выражение. Пусть, например, написано:
x = 183972 * 32432 x - (x + 100) = ?
Вряд ли вы будете вычислять сначала внутренние части: x и x + 100. Скорее всего, вы сначала раскроете все скобки и получите сразу -100.
Порядок вычисления изнутри наружу, как в C++ и Python, называется аппликативным порядком. Он может быть эффективнее в том смысле, что все выражения сводятся к самой короткой форме, и для вычислений не нужно много памяти. Порядок вычисления снаружи внутрь, как в математическом примере, называется нормальным порядком. Он требует больше памяти, но у него есть и плюс.
Попробуйте-ка вычислить такое выражение:
(\x. \y. y) ((\x. x x) (\x. x x)) 1
Нормальный порядок спокойно решает эту задачу такими β-редукциями:
(\x. \y. y) ((\x. x x) (\x. x x)) 1 -> (\y. y) 1 -> 1
А аппликативный порядок? Раскрываем (\x. x x) (\x. x x) — это самое внутреннее нераскрытое выражение. Для наглядности переименую переменные: (\x. x x) (\y. y y). Теперь подставим аргумент в качестве x слева: (\y. y y) (\y. y y). Получилось то же самое — ой, бесконечный цикл.
Вообще говоря, нормальный порядок потому и называется нормальным, что если это теоретически возможно, β-нормальную форму он выдаст обязательно.
Хотелось бы формально обсудить, как сравнивать выражения. Ну, то что 1 + 2 = 3 — мы знаем, а правда ли и что вообще означает запись \x. sin (1 + 2) = \y. (\x. sin x) 3?
Чтобы раз и навсегда решить это вопрос, давайте различать следующие обозначения:
a = b будет обозначать чисто математическое равенство.
a -> b, уже встречавшееся ранее, означает, что выражение a можно преобразовать в выражение b, последовательно применяя любые из трех уже знакомых нам операций: α-эквивалентность, β-редукция, η-преобразование. И пусть знак β вас не путает — совместимость, что с ней поделать. Стрелка означает однонаправленность отношения. Например:
(\x. sin x) (3) -> sin 3
Но не:
sin 3 -> (\x. sin x) (3)
a ->> b означает то же самое, что a -> b, но еще требуется, чтобы b было β-нормальной формой. Проще говоря, a ->> ... показывает, какой конечный результат будет при "выполнении" a. Если вам так проще — это рефлексивное транзитивное замыкание по трем основным преобразованиям. Например:
(\f. \x. \y. f x y) ->> (\f. f)
Но не:
(\f. \x. \y. f x y) ->> (\f. \x. f x)
a =b b означает, что выражение a можно преобразовать в выражение b, последовательно применяя любые из трех операций выше или обратные к ним. То есть, например:
(\x. sin x) =b sin
И наоборот:
sin =b (\x. sin x)
После всего этого появляется интересный вопрос. Вот, например, выражение succ 3 невычислимо в том смысле, что в результате применения β-редукций получается терм-функция \f. \x. f(f(f(f x))). Хотите получить самую-самую β-нормальную форму и применить еще одну β-редукцию? Удачи вычислить f x с применением переменной f.
И как вообще определить, правда ли succ 3 — это то же самое, что 4? В теории можно использовать β-эквивалентность, уже известную нам как отношение =b. Но хотелось бы научиться как-то конструктивно определять это.
Делается это так: вычисляем оба сравниваемые выражения, проводя все возможные β-редукции, которые можно, по нормальному порядку вычислений, даже если β-редуцированные термы находятся внутри определений функций. После этого достаточно просто сравнить выражения на посимвольное равенство. Пример для понимания: \a. \b. b ((\x. x x) a) = \a. \b. b (a a). Далее, термы \x. \y. x y и \y. \x. y x эквивалентны, хотя и не равны посимвольно — про α-эквивалентность забывать нельзя. Ну и как же не упомянуть замыкающее троицу η-преобразование: \f. \x. f x и \f. f также должны быть эквивалентны.
Однако в более сложных ситуациях при попытке применить этот метод всплывает некоторая проблема. Дело в том, что далеко не все термы имеют β-нормальную форму. Например, (\x. x x) (\x. x x) — типичный пример "бесконечного цикла" в λ-исчислении. В таком более общем случае задача конструктивной проверки β-эквивалентности неразрешима, но об этом мы подробнее поговорим чуть позже.