Лямбда-исчисление Чёрча Рекурсия без имён: комбинатор неподвижной точки Y
0%

Рекурсия без имён: комбинатор неподвижной точки Y

Рекурсия без имён: комбинатор неподвижной точки Y

Вот факториал. Все его писали:

const fact = n => n === 0 ? 1 : n * fact(n - 1);
def fact(n):
    return 1 if n == 0 else n * fact(n - 1)

Присмотритесь к правой части. Внутри тела стоит слово fact — то самое имя, которое мы прямо сейчас определяем. Это работает, потому что и JavaScript, и Python держат где-то таблицу имён, и к моменту первого вызова в ней уже лежит нужная функция.

А теперь вспомните, что такое чистое лямбда-исчисление: переменная, абстракция, аппликация. Всё. Никакой таблицы имён нет. Никакого const, def, let не существует. Единственный способ, которым переменная получает смысл, — она стоит под лямбдой, которая её связывает. Написать

FACT = λn. IF (ISZERO n) 1 (MULT n (FACT (PRED n)))

нельзя не потому, что это некрасиво, а потому, что здесь FACT справа — свободная переменная. Она ни к чему не привязана. Знак = в лямбда-исчислении — не оператор языка, а сокращение, которое мы, люди, пишем на бумаге; развернув его, мы получим выражение, которое ссылается само на себя, а термы так не строятся: терм — это конечное дерево.

Отсюда вопрос, который занимал Чёрча и Карри в тридцатых: можно ли получить рекурсию, вообще не имея имён? Если нельзя — лямбда-исчисление слабее машины Тьюринга и как модель вычислений никуда не годится. Ответ: можно, и трюк для этого нужен всего один.

Идея: пусть функция получит саму себя аргументом

Проблема в том, что тело функции не знает своего имени. Хорошо — давайте передадим ей то, что она должна вызвать, обычным параметром. Пусть первый аргумент называется self:

// Никакой рекурсии здесь нет: это обычная функция двух аргументов.
const factStep = self => n => n === 0 ? 1 : n * self(n - 1);
fact_step = lambda self: lambda n: 1 if n == 0 else n * self(n - 1)

Такую форму называют открытой рекурсией (open recursion): рекуррентный шаг записан, но «дырка» в месте рекурсивного вызова оставлена открытой и заполняется снаружи. factStep — совершенно обычная функция, ничего необычного в ней нет, её можно вызвать прямо сейчас:

factStep(x => 999)(0);   // 1   — база не трогает self
factStep(x => 999)(5);   // 4995 = 5 * 999 — self подставился как есть

Теперь заметьте: если бы мы могли передать в self сам факториал, всё бы заработало. То есть нам нужна такая функция FACT, что

FACT = factStep FACT

Функция, которая не меняется, если применить к ней factStep. В математике объект, который не меняется под действием функции, называется неподвижной точкой: x — неподвижная точка f, если f x = x. У функции f(x) = x² неподвижные точки 0 и 1. У f(x) = x + 1 их нет. А нам нужна неподвижная точка функции высшего порядка factStep, аргумент и результат которой — сами функции.

Значит, задача свелась к одной вещи: научиться находить неподвижную точку любого терма. Комбинатор, который это делает, называют комбинатором неподвижной точки, и обозначают Y.

Ручная версия: передаём себя руками

Прежде чем выводить Y, полезно один раз сделать это грубой силой. Идея: если функции нужна она сама — пусть она принимает себя и не забывает передавать себя дальше.

// f получает саму себя первым аргументом и обязана сама себя прокидывать
const factSelf = (me, n) => n === 0 ? 1 : n * me(me, n - 1);

factSelf(factSelf, 5);  // 120
fact_self = lambda me, n: 1 if n == 0 else n * me(me, n - 1)
fact_self(fact_self, 5)   # 120

Работает! И заметьте: имени factSelf внутри тела нет — там только параметр me. Мы уже победили, просто некрасиво: вызывающий обязан знать про фокус с me и писать me(me, ...) вручную.

Ключевая техника здесь — самоприменение: выражение вида x x, где переменная применяется к самой себе. В типизированных языках так нельзя (об этом ниже), в чистом лямбда-исчислении — пожалуйста, синтаксис не запрещает. Именно самоприменение — источник всей рекурсии в этом исчислении.

Самый маленький пример самоприменения — знаменитый терм Ω (омега):

ω = λx. x x            -- «применить аргумент к самому себе»
Ω = ω ω = (λx. x x) (λx. x x)

Раскрутим его. Редекс один, подставляем x := (λx. x x):

(λx. x x) (λx. x x)
→β  x x  [x := (λx. x x)]
 =  (λx. x x) (λx. x x)

Получили ровно то, с чего начали. Ω редуцируется сам в себя вечно и не имеет нормальной формы — первый пример незавершающегося вычисления в лямбда-исчислении. Это не баг: чтобы язык был полным по Тьюрингу, в нём обязаны быть незавершающиеся программы (иначе решалась бы проблема остановки — подробнее в статье про вычислимость).

Самоприменение и петля редукции

Y — это Ω, у которого на каждом витке из петли что-то выпадает наружу.

Вывод Y

Нам нужен Y со свойством Y F = F (Y F). Пойдём от Ω и подкрутим его.

В Ω каждый виток даёт снова Ω. Вставим в тело обёртку f (...):

Y = λf. (λx. f (x x)) (λx. f (x x))

Это и есть комбинатор Y Карри. Он состоит из тех же деталей, что Ω: две копии одной абстракции, применённые друг к другу; разница только в том, что самоприменение x x завёрнуто в f.

Проверим свойство неподвижной точки — с полной раскруткой, шаг за шагом. Введём сокращение W = λx. F (x x), чтобы не переписывать длинные термы:

Шаг 0.   Y F
       = (λf. (λx. f (x x)) (λx. f (x x))) F

Шаг 1.   Бета-редукция внешнего редекса, подстановка f := F:
       → (λx. F (x x)) (λx. F (x x))
       = W W                                  -- по определению W

Шаг 2.   Теперь редекс — это W W. Раскрываем левое W:
         (λx. F (x x)) W
         подставляем x := W в тело F (x x):
       → F (W W)

Шаг 3.   Смотрим на результат: F (W W).
         Но W W — это ровно то, что получилось на шаге 1 из Y F.
         Значит:  Y F  →→  F (W W)   и   F (Y F)  →→  F (W W)

Оба терма сводятся к одному и тому же — F (W W). То есть Y F и F (Y F) бета-эквивалентны:

Y F  =β  F (Y F)

Это и есть определение неподвижной точки. Обратите внимание на аккуратность формулировки: не «Y F редуцируется в F (Y F)», а «они равны по бета-эквивалентности» — редукция идёт в общего потомка. Для комбинатора Тьюринга (см. ниже) выполняется более сильное свойство — настоящая редукция.

Что происходит дальше? На шаге 2 внутри результата снова сидит W W, а W W снова редуцируется в F (W W). Значит:

Y F →→ F (W W)
    →→ F (F (W W))
    →→ F (F (F (W W)))
    →→ ...

Бесконечная башня из F. И она безопасна ровно по одной причине: раскручивается лениво. Следующий слой появляется, только если вычисление до него добралось. Если F в какой-то момент перестанет трогать свой аргумент (а условие «если n = 0, вернуть 1» именно это и делает — отбрасывает ветку с рекурсивным вызовом), башня обрывается и всё сходится.

Разворачивание Y F в башню из F

Полная раскрутка: считаем факториал двойки

Соберём всё вместе. Чтобы трассировка читалась, разрешим себе писать числа, × и if как готовые примитивы — это стандартный приём «лямбда-исчисление с дельта-правилами». Всё то же самое собирается из чисел Чёрча и булевых значений, просто трасса стала бы вчетверо длиннее.

G = λself. λn. if (n = 0) then 1 else n × (self (n − 1))
FACT = Y G
W = λx. G (x x)

Считаем FACT 2 в нормальном порядке (всегда редуцируем самый левый внешний редекс):

 1.  FACT 2
   = (Y G) 2

 2.  Раскрываем Y (подстановка f := G):
   → ((λx. G (x x)) (λx. G (x x))) 2
   = (W W) 2

 3.  Редуцируем W W → G (W W)   [x := W]:
   → (G (W W)) 2

 4.  Раскрываем G, подставляем self := (W W):
   → (λn. if (n = 0) then 1 else n × ((W W) (n − 1))) 2

 5.  Подставляем n := 2:
   → if (2 = 0) then 1 else 2 × ((W W) (2 − 1))

 6.  Условие ложно — берём else-ветку:
   → 2 × ((W W) 1)

 7.  Снова W W → G (W W):
   → 2 × ((G (W W)) 1)

 8.  Раскрываем G, self := (W W), затем n := 1:
   → 2 × (if (1 = 0) then 1 else 1 × ((W W) (1 − 1)))

 9.  Условие ложно:
   → 2 × (1 × ((W W) 0))

10.  Снова W W → G (W W), раскрываем G, n := 0:
   → 2 × (1 × (if (0 = 0) then 1 else 0 × ((W W) (0 − 1))))

11.  Условие ИСТИННО — берём then-ветку.
     Вся else-ветка вместе с (W W) просто ВЫБРАСЫВАЕТСЯ:
   → 2 × (1 × 1)

12.  → 2 × 1
   → 2

Вот весь фокус, шаг 11 — самый важный в статье. Башня из G никогда не строится целиком: if на каждом уровне отбрасывает одну из веток, и когда база рекурсии срабатывает, отбрасывается именно та ветка, в которой сидит W W. Больше разворачивать нечего — вычисление завершается.

Почему Y ломается в JavaScript и Python (и что с этим делать)

Переведём Y буквально:

const Y = f => (x => f(x(x)))(x => f(x(x)));
Y = lambda f: (lambda x: f(x(x)))(lambda x: f(x(x)))

И запустим:

Y(self => n => n === 0 ? 1 : n * self(n - 1));
// RangeError: Maximum call stack size exceeded

Причём падает не вызов факториала, а само построение Y(f) — до аргумента 5 дело не доходит. Разберёмся почему.

JavaScript и Python вычисляют аппликативным порядком (call-by-value): прежде чем применить функцию к аргументу, аргумент вычисляется до конца. В нашей трассировке шага 2 мы, наоборот, сначала подставляли, а вычисляли потом — это нормальный порядок. Разница фатальна:

Аппликативный порядок на W W = (λx. F (x x)) W:
  прежде чем подставлять, надо вычислить аргумент W... W — уже значение, ок.
  → F (W W)
  теперь прежде чем применить F, надо вычислить аргумент (W W)
  → F (F (W W))
  теперь надо вычислить аргумент (W W) внутри...
  → F (F (F (W W)))
  → ...

Здесь нет if, который что-то отбросит: аргумент вычисляется всегда, независимо от того, понадобится он или нет. Башня строится до упора, стек кончается.

Лечение — эта-расширение. В статье про редукции мы видели: M и λv. M v ведут себя одинаково при применении, но второй терм — это уже значение (абстракция), а не редекс. Значит, его вычисление откладывается до момента, когда его действительно вызовут. Обернём проблемное x x:

Z = λf. (λx. f (λv. x x v)) (λx. f (λv. x x v))

Это комбинатор Z, он же «call-by-value Y». Отличие от Y ровно одно: (x x) стало (λv. x x v). И теперь всё работает:

const Z = f => (x => f(v => x(x)(v)))(x => f(v => x(x)(v)));

const fact = Z(self => n => (n === 0 ? 1 : n * self(n - 1)));
fact(5);   // 120

const fib = Z(self => n => (n < 2 ? n : self(n - 1) + self(n - 2)));
[...Array(10).keys()].map(fib);   // [0,1,1,2,3,5,8,13,21,34]
Z = lambda f: (lambda x: f(lambda v: x(x)(v)))(lambda x: f(lambda v: x(x)(v)))

fact = Z(lambda self: lambda n: 1 if n == 0 else n * self(n - 1))
fact(5)          # 120

fib = Z(lambda self: lambda n: n if n < 2 else self(n - 1) + self(n - 2))
[fib(i) for i in range(10)]   # [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

Сложность у Z-версии ровно та же, что у обычной рекурсии: fact — O(n) по времени и O(n) по глубине стека, наивный fib — O(φⁿ) по времени и O(n) по стеку. Комбинатор не добавляет асимптотики, только константу на лишний вызов-обёртку λv. ... v на каждом шаге.

Важный практический вывод: Z — не экзотика. Ровно тем же приёмом (обернуть в функцию, чтобы отложить вычисление) вы пользуетесь, когда пишете () => expensive() вместо expensive(). Подробнее про отложенные вычисления — в статье про ленивость и потоки, а про сами стратегии — в следующей статье трека.

Комбинатор Тьюринга Θ

Y не единственный. Тьюринг в 1937 году предложил другой:

A = λx. λy. y (x x y)
Θ = A A

Раскрутим Θ F полностью:

1.  Θ F = (A A) F

2.  Редуцируем A A = (λx. λy. y (x x y)) A, подставляя x := A:
  → (λy. y (A A y)) F

3.  Подставляем y := F:
  → F (A A F)
  = F (Θ F)                       -- по определению Θ = A A

Три шага, и мы получили настоящую редукцию Θ F →→ F (Θ F), а не только бета-эквивалентность, как у Y. Это делает Θ удобнее в доказательствах.

Комбинаторов неподвижной точки бесконечно много. Есть даже красивое семейство Клопа, где комбинатор составлен из копий одной буквы (Yk = LLLLLLLLLLLLLLLLLLLLLLLLLL для подходящего L). Практический смысл один: свойство «быть комбинатором неподвижной точки» — это свойство поведения, а не конкретной формулы.

Что бывает, если применить Y к чему попало

Полезное упражнение на интуицию: Y не «делает функцию рекурсивной», он находит неподвижную точку. Что это значит для простых аргументов?

Y I, где I = λx. x (тождественная функция). Ищем X такой, что I X = X. Но I X = X для любого X — неподвижная точка у I любая. Что вернёт Y?

Y I →→ I (Y I) → Y I →→ I (Y I) → ...

Бесконечный цикл без нормальной формы. Логично: конкретного ответа не существует, Y возвращает «расходимость».

Y K, где K = λx. λy. x (константная функция, она же TRUE из кодирования Чёрча).

1.  Y K →→ K (Y K)
2.  K (Y K) = (λx. λy. x) (Y K)
  → λy. (Y K)                      -- подставили x := Y K

Получили функцию, которая игнорирует свой аргумент и возвращает Y K — то есть снова себя. Это «бесконечный пожиратель аргументов»: Y K a b c d ... можно кормить сколько угодно, ответ никогда не превратится в что-то простое. Нормальной формы нет, но, в отличие от Y I, каждый отдельный шаг что-то возвращает.

Мораль: Y осмысленно применять к термам вида «функция от self, которая где-то обрывает рекурсию». Ко всему остальному он тоже применяется — просто результат будет расходящимся.

Взаимная рекурсия

Классический вопрос: как быть, если функции вызывают друг друга?

// то, что мы хотим, но с именами
const isEven = n => n === 0 ? true  : isOdd(n - 1);
const isOdd  = n => n === 0 ? false : isEven(n - 1);

Приём стандартный: свернуть несколько функций в одну структуру и брать нужную по индексу. Структурой может быть пара, а «индексом» — булев селектор. В чистом виде:

STEP = λself. λtag.
         tag
           (λn. IF (ISZERO n) TRUE  (self FALSE (PRED n)))    -- ветка isEven
           (λn. IF (ISZERO n) FALSE (self TRUE  (PRED n)))    -- ветка isOdd

EVEN_ODD = Y STEP
ISEVEN = EVEN_ODD TRUE
ISODD  = EVEN_ODD FALSE

Здесь tag — булево значение Чёрча, то есть селектор из двух аргументов: TRUE a b → a, FALSE a b → b. Он сам выбирает нужную ветку, никакого if не требуется.

На рабочих языках это выглядит так (тег для читаемости сделан строкой):

even_odd = Z(lambda self: lambda tag:
    (lambda n: True  if n == 0 else self("odd")(n - 1)) if tag == "even" else
    (lambda n: False if n == 0 else self("even")(n - 1)))

is_even = even_odd("even")
is_odd  = even_odd("odd")
is_even(10), is_odd(10)     # (True, False)

Обобщение этого приёма — то, как компиляторы функциональных языков реализуют letrec (взаимно-рекурсивный блок определений): группа определений сворачивается в кортеж, к нему применяется комбинатор неподвижной точки, из результата достаются компоненты. Подробный разбор — у Саймона Пейтона Джонса в The Implementation of Functional Programming Languages, глава про трансляцию в супер-комбинаторы.

Зачем это в реальном коде

Соблазн сказать «красивая теория, но в проде я напишу def fact». Справедливо — но открытая рекурсия и явная неподвижная точка решают несколько задач, которые именованной рекурсией не решаются.

1. Мемоизация без изменения функции. Если рекурсивный вызов идёт через параметр self, вы можете подставить туда что угодно — например, кэширующую обёртку. С именованной рекурсией это невозможно: имя внутри тела жёстко указывает на исходную функцию, и никакой декоратор снаружи не перехватит внутренние вызовы (это классическая ловушка, когда @lru_cache навешивают на функцию, которая внутри зовёт себя по старому имени в замыкании).

def memo_fix(step):
    cache = {}
    def rec(n):
        if n not in cache:
            cache[n] = step(rec)(n)     # в self уходит кэширующая rec
        return cache[n]
    return rec

fib = memo_fix(lambda self: lambda n: n if n < 2 else self(n - 1) + self(n - 2))
fib(60)      # 1548008755920, мгновенно: O(n) вместо O(φⁿ)

Тело step не изменилось ни на символ — изменился только «узел», которым мы завязали рекурсию.

2. Трассировка и профилирование. Тот же приём: оборачиваем не результат, а шаг.

let calls = 0;
const traced = step => self => n => { calls++; return step(self)(n); };

const fib = Z(traced(self => n => (n < 2 ? n : self(n - 1) + self(n - 2))));
fib(15);      // 610
calls;        // 1973 — видно все внутренние вызовы, а не только внешний

3. fix как штатная библиотечная функция. В Haskell комбинатор неподвижной точки лежит в стандартной библиотеке — Data.Function.fix, причём определён самым наглым способом:

fix :: (a -> a) -> a
fix f = let x = f x in x        -- узел завязан прямо в let, спасибо лени

factorial = fix (\self n -> if n == 0 then 1 else n * self (n - 1))
ones      = fix (1 :)           -- бесконечный список из единиц
fibs      = fix (\xs -> 0 : 1 : zipWith (+) xs (tail xs))

Последние две строки — не курьёз, а рабочий идиом: в ленивом языке неподвижная точка порождает бесконечные структуры данных, и fix — их естественная запись.

4. Понимание того, что делает ваш компилятор. Именованная рекурсия в языке с лексической областью видимости — это сахар. Внутри компилятор либо строит циклическую ссылку в окружении, либо (в некоторых бэкендах и во всех формализациях семантики) применяет ровно комбинатор неподвижной точки. Когда вы читаете спецификацию языка или статью по теории типов и видите fix, это оно.

5. Открытая рекурсия как основа наследования. Строгий факт: метод в ООП — это функция с открытой рекурсией, где self/this подставляется системой при создании объекта, а переопределение метода в наследнике меняет то, куда указывает self в родительском коде. Наследование в теории объектов моделируется буквально как неподвижная точка «генератора класса» — см. классическую работу Уильяма Кука A Denotational Semantics of Inheritance. Отсюда же растёт вечная путаница с вызовом переопределённого метода из конструктора: узел неподвижной точки ещё не завязан.

Типы: почему Y не влезает в простые типы

Попробуйте типизировать λx. f (x x). Раз x применяется к x, тип x должен быть одновременно и функцией A → B, и её аргументом A. То есть A = A → B — уравнение, у которого в системе простых типов решения нет: типы там конечные деревья.

Это не недоработка, а фундаментальное свойство: просто типизированное лямбда-исчисление сильно нормализуемо — любое вычисление в нём завершается. Значит, оно не полно по Тьюрингу, и Y в нём выразить нельзя ни в каком виде. Языки с типами, которые всё-таки хотят рекурсию, добавляют её отдельным примитивом (fix как константа с типом (a → a) → a) либо разрешают рекурсивные типы (μ-типы), в которых уравнение A = A → B решается легально. Отсюда же следует, что тотальные языки вроде Agda и Idris требуют доказательства завершаемости — там Y просто не построить. Всё это — тема статьи про типизированное лямбда-исчисление.

TypeScript, кстати, Z типизирует — но только потому, что позволяет объявить рекурсивный интерфейс:

interface Rec<A, B> { (x: Rec<A, B>): (a: A) => B }

const Z = <A, B>(f: (self: (a: A) => B) => (a: A) => B): ((a: A) => B) =>
  ((x: Rec<A, B>) => f((v: A) => x(x)(v)))
  ((x: Rec<A, B>) => f((v: A) => x(x)(v)));

const fact = Z<number, number>(self => n => (n === 0 ? 1 : n * self(n - 1)));

Строчка interface Rec — это ровно тот самый μ-тип, записанный средствами TypeScript.

Типичные ошибки

  • Ждать, что Y заработает в JS/Python как есть. Не заработает: аппликативный порядок. Нужен Z (эта-расширенная версия). Симптом — стек переполняется в момент построения Y(f), ещё до первого «полезного» вызова.
  • Забыть, что F принимает self первым аргументом. Z(n => n === 0 ? 1 : ...) — типичная ошибка: сюда должна идти функция двух уровней, self => n => ....
  • Думать, что Y где-то хранит функцию. Ничего не хранится. Терм каждый раз пересоздаёт свою копию через самоприменение; никакого состояния, никакой таблицы имён.
  • Путать Y F и F. Y F — это «F, у которого дырка self заполнена самим результатом». Применять Y к уже готовой рекурсивной функции бессмысленно.
  • Забывать про базу рекурсии. Без ветки, которая отбрасывает self, башня не обрывается — получите Ω с лишними шагами. В лямбда-исчислении это выглядит как «терм не имеет нормальной формы», в реальном языке — как RecursionError.
  • Считать эта-обёртку косметикой. λv. x x v и x x эквивалентны по поведению, но не по порядку вычисления. Разница между работающей программой и переполнением стека — ровно в ней.

Упражнения

Все — на «сведите к нормальной форме или объясните, почему её нет». Считайте в нормальном порядке (самый левый внешний редекс первым). Ответы под каждым.

1. Сведите (λx. x x) (λy. y).

Ответ.

(λx. x x) (λy. y)
→β  x x  [x := λy. y]
 =  (λy. y) (λy. y)
→β  y [y := λy. y]
 =  λy. y

Нормальная форма — λy. y, то есть I. Самоприменение не обязано зацикливаться: всё зависит от того, что применяется.

2. Сведите (λx. x x x) (λx. x x x).

Ответ. Обозначим M = λx. x x x.

M M
→β  x x x [x := M] = M M M
→β  (M M) M → (M M M) M = M M M M
→ ...

Нормальной формы нет, и терм не просто зацикливается, а растёт: на каждом шаге в нём становится на одну копию M больше. Полезный контрпример к интуиции «раз не завершается, значит крутится по кругу».

3. Покажите первые три шага раскрутки Y F для произвольного F, не сокращая W.

Ответ.

Y F = (λf. (λx. f (x x)) (λx. f (x x))) F
→β  (λx. F (x x)) (λx. F (x x))
→β  F ((λx. F (x x)) (λx. F (x x)))
→β  F (F ((λx. F (x x)) (λx. F (x x))))

Каждый шаг выносит наружу ровно один F, а внутри воспроизводится исходный терм.

4. Что такое Y (λx. λy. y)? Сведите к нормальной форме.

Ответ. Обозначим F = λx. λy. y (это KI, оно же FALSE, оно же «вернуть второй аргумент»).

Y F →→ F (Y F)
    = (λx. λy. y) (Y F)
→β  λy. y                     -- аргумент просто выброшен, x нигде не встречается

Нормальная форма — λy. y, то есть I. Здесь F игнорирует self, поэтому башня обрывается на первом же слое. Сравните с Y K из текста, где x как раз используется, — и результат расходится.

5. Напишите на JavaScript через Z функцию, суммирующую массив чисел, без единой именованной рекурсии.

Ответ.

const Z = f => (x => f(v => x(x)(v)))(x => f(v => x(x)(v)));
const sum = Z(self => xs => (xs.length === 0 ? 0 : xs[0] + self(xs.slice(1))));
sum([1, 2, 3, 4, 5]);   // 15

O(n) вызовов, но O(n²) по памяти из-за slice — на практике передавайте индекс: self => i => i >= xs.length ? 0 : xs[i] + self(i + 1).

6. Почему Θ (комбинатор Тьюринга) в JavaScript падает так же, как Y, и как его починить?

Ответ. По той же причине — аппликативный порядок: в y (x x y) аргумент (x x y) вычисляется до применения y, и это снова разворачивает A A. Лечится тем же эта-расширением:

const A = x => y => y(v => x(x)(y)(v));
const Theta = A(A);
Theta(self => n => (n === 0 ? 1 : n * self(n - 1)))(5);   // 120

7. Что вернёт Z(self => n => n)(7)? Проверьте рассуждением, потом кодом.

Ответ. 7. Шаг рекурсии не использует self, поэтому Z просто отдаёт n => n. Хорошая иллюстрация: Z не заставляет функцию быть рекурсивной, он только предоставляет ей доступ к самой себе.

Мини-итог

  • В лямбда-исчислении нет имён, поэтому «функция, вызывающая себя по имени», записать нельзя — терм ссылался бы на свободную переменную.
  • Решение в два хода: вынести рекурсивный вызов в параметр (открытая рекурсия), а затем найти неподвижную точку получившейся функции.
  • Y = λf. (λx. f (x x)) (λx. f (x x)) — это Ω, у которого каждый виток самоприменения обёрнут в f. Отсюда Y F =β F (Y F).
  • Башня F (F (F ...)) безопасна, потому что разворачивается лениво; база рекурсии выбрасывает ветку с невычисленным self, и всё сходится.
  • В языках с call-by-value (JS, Python) нужен Z — тот же Y с эта-обёрткой λv. x x v, откладывающей вычисление.
  • В простых типах Y невыразим — именно поэтому просто типизированное лямбда-исчисление всегда завершается.
  • Открытая рекурсия — не только теория: на ней держатся мемоизация без правки кода, трассировка, fix в Haskell и семантика наследования в ООП.

Что почитать дальше по теме: Benjamin Pierce, Types and Programming Languages (главы 5 и 12 — Y, Z и нормализация); Hendrik Barendregt, The Lambda Calculus: Its Syntax and Semantics (каноника по комбинаторам неподвижной точки); статья Ричарда Габриэля The Why of Y — тот самый вывод Y «с нуля», шаг за шагом.

Что дальше

Мы дважды упирались в один и тот же вопрос: какой редекс редуцировать первым. От ответа зависело, завершится ли Y F вообще. Пора разобрать это системно — какие бывают стратегии вычисления, почему нормальный порядок находит нормальную форму, если она существует, а аппликативный быстрее, но может зациклиться, и что такое ленивость в реальных языках.

Стратегии вычисления: нормальный порядок, аппликативный, ленивость

Нашли неточность? Выделите фрагмент текста — рядом появится жучок.

Нужен разбор именно вашей ситуации?

Статья описывает общий случай. Если у вас частный — можно разобрать его отдельно, платно. А если не хватает целого материала, предложите тему: её оплачивают вскладчину, и она выходит открытой для всех.

Доска запросов