Лямбда-исчисление Чёрча Лямбда-исчисление в живых языках: от Lisp до современных стрелочных функций
0%

Лямбда-исчисление в живых языках: от Lisp до современных стрелочных функций

22 мин 4651 слов
#лямбда-исчисление#функциональное программирование#компиляторы#замыкания

Лямбда-исчисление в живых языках: от Lisp до современных стрелочных функций

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

Эта статья — про то, что они не на бумаге. Когда вы пишете

const inc = x => x + 1;

вы буквально пишете λx. x + 1. Не «похоже на», не «вдохновлено» — это оно и есть, с точностью до значка. Синтаксис => появился в JavaScript в 2015 году, но выбранная за ним семантика — из статьи Чёрча 1936 года, и она прошла в язык через Lisp (1958), ALGOL 60, ISWIM, Scheme, ML и Smalltalk-блоки.

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

Короткая история одной идеи

Лямбда-исчисление задумывалось как основание математики, а не как язык программирования. Чёрч предложил его в 1932–1936 годах, первая версия оказалась противоречивой, урезанная «чисто функциональная» часть — нет. Через двадцать с лишним лет Джон Маккарти делал язык для символьных вычислений, увидел у Чёрча удобную нотацию для безымянных функций и утащил её вместе с именем.

Важная деталь для интуиции: Lisp 1.0 взял у Чёрча синтаксис, но не семантику. Первые реализации использовали динамическую область видимости, и знаменитая проблема funarg (когда возвращённая функция видела чужие переменные) — это ровно то, что в нашем треке называется захватом имён. Правильное решение нашли в Scheme: лексическая область видимости плюс замыкания. То есть индустрия наступила на грабли из статьи про подстановку и потратила пятнадцать лет, чтобы прийти к альфа-конверсии.

Три конструкции — и всё ваше рабочее утро

Напомню весь язык: переменная, абстракция, аппликация. Теперь перевод на живые языки.

Переменная — обращение к имени. Ничего интереснее в ней нет.

Абстракция λx. M — создание функции:

x => M                  // JavaScript
function (x) { return M }   // он же, длинно

lambda x: M             # Python
def f(x): return M      # он же, с именем

Аппликация f a — вызов:

f(a)

f(a)

Разница только в скобках: в лямбда-исчислении аппликация обозначается пробелом и левоассоциативна, f a b = (f a) b. В JS/Python это f(a)(b). И то и другое — каррирование: функция одного аргумента, возвращающая функцию одного аргумента.

Возьмём терм из статьи про синтаксис и разложим:

λx. λy. x

const K = x => y => x;
K(1)(2);   // 1

K = lambda x: lambda y: x
K(1)(2)    # 1

Это TRUE из статьи про булевы значения и комбинатор K из комбинаторной логики одновременно. В стандартной библиотеке Haskell он называется const, в Ramda — always, в Python его пишут руками. Один и тот же терм, четыре имени.

Замыкание = код функции плюс окружение для свободных переменных

Вызов функции — это бета-редекс, буквально

Бета-редукция — правило (λx. M) N → M[x := N]. В коде редекс выглядит как немедленно вызванное функциональное выражение (IIFE):

(x => x + 1)(5)

Разберём по шагам, как разбирали бы на бумаге:

Шаг 0.  (λx. x + 1) 5
        редекс: слева абстракция, справа аргумент

Шаг 1.  подставляем 5 вместо x в теле  x + 1
        (x + 1)[x := 5]  =  5 + 1

Шаг 2.  5 + 1
        это дельта-редекс: встроенная арифметика, не часть чистого исчисления

Шаг 3.  6
        нормальная форма

Движок JavaScript делает ровно эти шаги, только вместо переписывания текста кладёт 5 в слот аргумента на стеке. Наблюдаемый результат тот же.

Теперь два аргумента, чтобы увидеть каррирование в действии:

Шаг 0.  (λx. λy. x + y) 3 4
Шаг 1.  аппликация левоассоциативна: ((λx. λy. x + y) 3) 4
Шаг 2.  внутренний редекс: (λy. 3 + y)
Шаг 3.  (λy. 3 + y) 4
Шаг 4.  3 + 4
Шаг 5.  7

const add = x => y => x + y;
add(3)(4);        // 7
const add3 = add(3);   // это результат шага 2 — «частично применённая» функция
add3(4);          // 7

add = lambda x: lambda y: x + y
add(3)(4)         # 7
add3 = add(3)     # результат шага 2
add3(4)           # 7

Промежуточный шаг 2 в реальном языке — не абстракция ума, а объект в куче: замыкание, внутри которого лежит x = 3. Об этом ниже.

let, где, аргументы по умолчанию: сахар над аппликацией

Питер Ландин в 1966 году показал: let не нужен как отдельная конструкция языка, это сокращённая запись аппликации.

let x = N in M     ≡     (λx. M) N

Проверим на примере, полностью раскрутив:

Шаг 0.  let x = 5 in x * x
Шаг 1.  переписываем как аппликацию:  (λx. x * x) 5
Шаг 2.  бета:  (x * x)[x := 5]  =  5 * 5
Шаг 3.  25

В JavaScript это видно невооружённым глазом — до появления модулей так делали пространства имён:

// let x = 5 in x * x
(x => x * x)(5);      // 25

// вложенные let — вложенные лямбды
// let a = 2 in let b = 3 in a + b
(a => (b => a + b)(3))(2);   // 5

# в Python то же самое, только выражений-let нет вовсе
(lambda x: x * x)(5)                  # 25
(lambda a: (lambda b: a + b)(3))(2)   # 5

Тот же трюк объясняет несколько «странностей» реальных языков:

  • Аргумент по умолчанию — это лямбда с уже подставленным значением: def f(x, n=10) эквивалентно наличию терма, где свободная n заранее связана.
  • Мутабельный дефолт в Python (def f(xs=[])) кусается ровно потому, что подстановка происходит один раз при создании функции, а не при каждом вызове. В терминах трека: значение подставлено в терм, а не пересчитывается.
  • with в Python или using в C# — не лямбда-сахар, а обёртка над протоколом; не путайте.
  • Блочные выражения в Kotlin/Rust (let x = { ... };) — снова связывание, синтаксически другое, семантически то же.

Замыкания: то, чего в исчислении нет — и почему это одно и то же

В чистом исчислении бета-редукция физически переписывает тело: (λn. λy. n + y) 10 превращается в λy. 10 + y. Тело изменилось.

Настоящий компилятор так не делает — переписывать машинный код на лету дорого. Вместо этого он оставляет тело как есть и создаёт замыкание: пару «указатель на код + окружение с захваченными свободными переменными».

function makeAdder(n) {
  return y => n + y;    // n здесь свободна внутри стрелочной функции
}
const add10 = makeAdder(10);
add10(5);    // 15

Что здесь происходит на языке трека:

Шаг 0.  makeAdder 10   ≡   (λn. λy. n + y) 10
Шаг 1.  бета:  (λy. n + y)[n := 10]
Шаг 2.  λy. 10 + y
Шаг 3.  (λy. 10 + y) 5
Шаг 4.  10 + 5
Шаг 5.  15

Что происходит в движке:

Шаг 1'. создаётся замыкание { code: "λy. n + y", env: { n: 10 } }
Шаг 3'. вызов: заводим кадр { y: 5 }, родитель — env замыкания
Шаг 4'. ищем n: нет в кадре → есть в родителе → 10
Шаг 5'. 15

Результаты совпадают всегда — при условии, что область видимости лексическая. Замыкание — это ленивая подстановка, отложенная до момента, когда значение реально понадобится. Именно поэтому динамическая область видимости (искать n в кадре вызывающего, а не в месте определения) даёт другие ответы: это ровно захват имён, от которого нас спасает альфа-конверсия.

Проверка на понимание — код, который ломается при динамической области видимости и работает при лексической:

n = "глобальная"

def make():
    n = "локальная"
    return lambda: n      # свободная n связана лексически

def call(f):
    n = "чужая"
    return f()            # при динамике вернулось бы "чужая"

print(call(make()))       # "локальная"

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

Альфа-конверсия в проде: минификаторы, гигиена макросов, де Брёйн

Альфа-конверсия — «имя связанной переменной не имеет значения». В индустрии это не философия, а рабочий инструмент.

Минификаторы. Terser, esbuild, Closure Compiler переименовывают локальные переменные в a, b, c. Это буквально альфа-конверсия, и она корректна ровно потому, что связанные имена не наблюдаемы. Свободные (глобальные, импортированные) переименовывать нельзя — и минификаторы их не трогают. Различие «свободная/связанная» из второй статьи — это то, по чему минификатор принимает решение.

Гигиенические макросы. Макрос, разворачивающийся в код с временной переменной tmp, сломает пользовательский tmp — это захват имён в чистом виде. Scheme (syntax-rules), Rust (macro_rules!) решают проблему автоматическим переименованием при раскрытии. Классический источник — работа Кольбекера и др. о гигиеничном раскрытии макросов; текущее описание есть в документации Rust по макросам. В C макросы негигиеничны, поэтому там пишут __tmp_line_42 руками.

Индексы де Брёйна. Радикальное решение: не давать связанным переменным имён вообще, а ссылаться на «сколько лямбд наружу». Терм λx. λy. x записывается как λ λ 2. Альфа-эквивалентные термы становятся посимвольно равными, сравнение термов — тривиальным. Так устроены внутренние представления Coq, Agda, многих движков вывода типов.

λx. λy. x        →   λ λ 2
λa. λb. a        →   λ λ 2      те же самые, сравнение стало равенством строк
λx. λy. y x      →   λ λ 1 2

Эта-редукция: код-ревью на автомате

λx. f x → f, если x не свободна в f. На ревью это звучит так: «зачем оборачивать, передай функцию напрямую».

// эта-расширенная форма
users.map(u => formatUser(u));
// эта-редуцированная
users.map(formatUser);

list(map(lambda u: format_user(u), users))
list(map(format_user, users))

В Haskell это называют point-free стилем, hlint предлагает такие правки автоматически. Но у эта-редукции в реальных языках есть ловушки, которых нет в исчислении:

["1", "2", "3"].map(n => parseInt(n));   // [1, 2, 3]
["1", "2", "3"].map(parseInt);           // [1, NaN, NaN]

Почему: map передаёт колбэку три аргумента (элемент, индекс, массив), а parseInt принимает второй аргументом систему счисления. parseInt("2", 1) — недопустимое основание. То есть JS-функции не являются каррированными функциями одного аргумента, и потому эта-эквивалентность здесь неверна.

Второй случай — строгие языки с побочными эффектами: λx. f x откладывает вычисление f, а f вычисляет его сразу. Если f — дорогое выражение с эффектом, эта-редукция меняет момент срабатывания. В чистом ленивом Haskell разницы нет, в JS/Python — есть.

Мораль: эта-правило верно для чистых каррированных функций. Проверяйте оба условия, прежде чем «упрощать».

Стратегии вычисления: почему && не может быть обычной функцией

В статье о стратегиях мы разбирали нормальный и аппликативный порядок. Практическое следствие живёт в каждом языке.

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

const and = (a, b) => a ? b : false;
and(false, expensive());   // expensive() всё равно вызовется
false && expensive();      // не вызовется — && встроен в язык как особая форма

Лямбда-исчисление даёт готовое лекарство — обернуть аргумент в абстракцию (thunk), потому что абстракция вычисляется не раньше, чем к ней применят аргумент:

const andLazy = (a, thunk) => a ? thunk() : false;
andLazy(false, () => expensive());   // expensive не вызовется

Разберём по шагам, что делает обёртка:

Шаг 0.  and FALSE expensive          аргумент — терм, который надо вычислить сразу
Шаг 1.  аппликативный порядок требует нормализовать expensive → большая работа

Шаг 0'. andLazy FALSE (λ_. expensive)
Шаг 1'. (λ_. expensive) — уже нормальная форма, абстракция, вычислять нечего
Шаг 2'. в теле выбирается ветка FALSE, thunk просто выбрасывается
Шаг 3'. expensive не вычислен ни разу

Это тот же приём, которым в статье про булевы значения чинили IF при аппликативном порядке. На практике он же — под капотом:

  • Supplier<T> и Optional.orElseGet в Java (в отличие от orElse, который вычисляет всегда);
  • lazy в Kotlin и Swift, Lazy<T> в C#;
  • ленивые сигналы и мемоизация в React/Vue/Solid;
  • генераторы Python: yield превращает тело в цепочку отложенных шагов.

Полный разбор ленивости — в статье про ленивые вычисления и потоки.

Y-комбинатор в языке, где есть имена

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

Классический Y = λf. (λx. f (x x)) (λx. f (x x)) в строгом языке зациклится: x x вычислится до передачи в f. Лекарство — эта-расширение, дающее Z-комбинатор (он же аппликативный Y):

Y = λf. (λx. f (x x)) (λx. f (x x))
Z = λf. (λx. f (λv. x x v)) (λx. f (λv. x x v))
       ^^^^^^^^^^^^^^^^ обёртка λv. ... откладывает самоприменение

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

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

Z = lambda f: (lambda x: f(lambda v: x(x)(v)))(lambda x: f(lambda v: x(x)(v)))

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

Раскрутим первый вызов по шагам, чтобы было видно, откуда берётся рекурсия:

Шаг 0.  Z factStep 3
Шаг 1.  (λx. factStep (λv. x x v)) (λx. factStep (λv. x x v))  применённое к 3
        обозначим X = λx. factStep (λv. x x v)
Шаг 2.  X X 3
Шаг 3.  бета по x := X:  factStep (λv. X X v)  3
Шаг 4.  factStep получает self = (λv. X X v) и возвращает
        λn. if n <= 1 then 1 else n * (λv. X X v) (n - 1)
Шаг 5.  применяем к 3:  3 * (λv. X X v) 2
Шаг 6.  (λv. X X v) 2  →  X X 2   — и мы снова в шаге 2, но с n = 2
Шаг 7.  3 * (2 * (X X 1))
Шаг 8.  X X 1  →  ... → 1
Шаг 9.  3 * 2 * 1 = 6

Обратите внимание на шаг 6: обёртка λv. ... v — это и есть эта-расширение, единственное отличие Z от Y. Оно превращает бесконечно раскручивающийся терм в абстракцию, которая ждёт аргумента. В строгом языке это разница между работающим кодом и переполнением стека.

Где Y-подобные вещи всплывают на практике: определение рекурсивных типов через Fix, fix в Haskell (fix f = let x = f x in x), рекурсивные схемы (catamorphism/anamorphism), а также обход letrec при компиляции языков, где рекурсивных связываний нет в ядре.

Как компилятор видит вашу программу

Самое неожиданное для многих: промышленные компиляторы функциональных языков буквально переводят исходник в лямбда-исчисление и работают уже с ним.

Что тут важно понять:

  • Ядро языка крошечное. У Haskell в исходнике десятки конструкций, в GHC Core — около десяти форм, и почти все они узнаваемы из нашего трека: переменная, абстракция, аппликация, let, case, литералы, приведения типов. Всё остальное — сахар. Официальное описание есть в GHC Commentary про Core.
  • Оптимизации — это редукции. Инлайн функции = бета-редукция, выполненная компилятором заранее. Устранение лишней обёртки = эта-редукция. Разбор «почему GHC не заинлайнил» на практике сводится к рассуждениям о размере терма и о том, сколько раз он используется.
  • Closure conversion — это перевод из мира «свободные переменные» в мир «явные поля». После него в программе нет свободных переменных вообще: каждая функция получает окружение аргументом. Смотри рисунок с замыканием выше.
  • CPS (continuation-passing style) — преобразование, где каждая функция получает дополнительный аргумент «что делать дальше». Оно тоже чисто лямбда-исчислительное и лежит в основе многих оптимизирующих компиляторов, а также async/await: компилятор превращает линейный код с await в цепочку колбэков, то есть в CPS.

Эндрю Аппель показал («SSA is Functional Programming», 1998), что SSA-форма в императивных компиляторах (LLVM, JVM JIT) изоморфна функциональному представлению: phi-узлы соответствуют параметрам функций-блоков. То есть даже компилятор C внутри рассуждает термами, просто называет их иначе.

Где ещё сидит лямбда в обычном дне разработчика

Пара примеров, где связь прямее, чем кажется.

Middleware — это композиция. Express, Koa, ASP.NET Core pipeline, Django middleware — всё это f ∘ g ∘ h, применённое к запросу. В терминах трека: λx. f (g (h x)).

const compose = (...fns) => x => fns.reduceRight((acc, f) => f(acc), x);
const pipeline = compose(auth, logging, rateLimit);
pipeline(request);

Promise — это не совсем монада, но then — это bind. Идея та же: связывание отложенного вычисления с продолжением. Разбор в статье про монады.

Дженерики — это System F. <T>(x: T) => T — это Λα. λx:α. x из статьи о типах. Java-стирание типов, C#-реификация, Rust-мономорфизация — это три разных инженерных ответа на вопрос «что делать с большой лямбдой во время исполнения».

AWS Lambda названа так не случайно: единица развёртывания — функция без состояния, которая получает вход и возвращает выход. Маркетинг, но честный.

Типичные ошибки и заблуждения

«Замыкания в цикле работают неправильно». Работают ровно правильно, вопрос в том, сколько связываний создаётся.

var создаёт одну связку на цикл, let — новую на каждую итерацию

const fs = [];
for (var i = 0; i < 3; i++) fs.push(() => i);
fs.map(f => f());     // [3, 3, 3]

const gs = [];
for (let i = 0; i < 3; i++) gs.push(() => i);
gs.map(g => g());     // [0, 1, 2]

var создаёт одну связку на всю функцию — все три терма ссылаются на одну свободную переменную, и после цикла её значение равно 3. let спецификация определяет так, что на каждую итерацию создаётся новая связка — три разных лямбды с разными окружениями. В Python классика та же:

fs = [lambda: i for i in range(3)]
[f() for f in fs]                  # [2, 2, 2]

gs = [lambda i=i: i for i in range(3)]   # значение по умолчанию = ранняя подстановка
[g() for g in gs]                  # [0, 1, 2]

«Лямбда — это анонимная функция». Не совсем: анонимность — свойство синтаксиса, а лямбда-абстракция — конструкция, создающая функцию. def f(x): return x — тоже лямбда-абстракция, просто с именем сверху.

«Функциональный код медленнее, потому что лямбды». Смешиваются два разных вопроса. Аллокация замыкания — реальная стоимость (объект в куче, давление на GC). Но JIT-компиляторы агрессивно инлайнят мономорфные колбэки, и в горячем цикле arr.map(f) часто компилируется в такой же машинный код, что и for. Мерить, а не гадать. При этом кодирования Чёрча из статьи про числа действительно катастрофически медленные — они учебные, не производственные.

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

Хвостовая рекурсия. В чистом исчислении рекурсия ничего не «кладёт на стек» — стека нет, есть переписывание терма. В реальных языках стек есть. Scheme и Elixir обязаны устранять хвостовые вызовы, JVM и CPython — нет, и в Python вы упрётесь в RecursionError на глубине около 1000. Поэтому академически элегантное решение через Y в Python — учебный пример, а не рабочий код.

Мини-лаборатория: интерпретатор за 45 строк

Лучшее упражнение — реализовать нормальный порядок редукции и посмотреть, как термы раскручиваются. Термы кодируем кортежами: ("var", "x"), ("lam", "x", body), ("app", f, a).

from itertools import count

_fresh = count()

def free_vars(t):
    """Свободные переменные терма."""
    kind = t[0]
    if kind == "var":
        return {t[1]}
    if kind == "lam":
        return free_vars(t[2]) - {t[1]}
    return free_vars(t[1]) | free_vars(t[2])

def subst(t, name, value):
    """t[name := value] с переименованием при угрозе захвата."""
    kind = t[0]
    if kind == "var":
        return value if t[1] == name else t
    if kind == "app":
        return ("app", subst(t[1], name, value), subst(t[2], name, value))
    # абстракция
    param, body = t[1], t[2]
    if param == name:
        return t                       # переменная перекрыта, подстановка не идёт внутрь
    if param in free_vars(value):      # захват — делаем альфа-конверсию
        fresh = f"{param}#{next(_fresh)}"
        body = subst(body, param, ("var", fresh))
        param = fresh
    return ("lam", param, subst(body, name, value))

def step(t):
    """Один шаг нормального порядка: самый левый внешний редекс. None — нормальная форма."""
    if t[0] == "app":
        f, a = t[1], t[2]
        if f[0] == "lam":                              # это редекс
            return subst(f[2], f[1], a)
        nf = step(f)
        if nf is not None:
            return ("app", nf, a)
        na = step(a)
        if na is not None:
            return ("app", f, na)
        return None
    if t[0] == "lam":
        nb = step(t[2])
        return None if nb is None else ("lam", t[1], nb)
    return None

def show(t):
    kind = t[0]
    if kind == "var":
        return t[1]
    if kind == "lam":
        return f"(\\{t[1]}. {show(t[2])})"
    return f"({show(t[1])} {show(t[2])})"

def normalize(t, limit=100, trace=True):
    for i in range(limit):
        if trace:
            print(f"{i}: {show(t)}")
        nxt = step(t)
        if nxt is None:
            return t
        t = nxt
    raise RuntimeError("предел шагов исчерпан — возможно, терм расходится")

Проверка на числах Чёрча: 2 применённая к succ и 0.

V = lambda n: ("var", n)
L = lambda p, b: ("lam", p, b)
A = lambda f, a: ("app", f, a)

two  = L("f", L("x", A(V("f"), A(V("f"), V("x")))))
succ = L("n", L("f", L("x", A(V("f"), A(A(V("n"), V("f")), V("x"))))))
zero = L("f", L("x", V("x")))

normalize(A(A(two, succ), zero))
# 0: (((\f. (\x. (f (f x)))) (\n. ...)) (\f. (\x. x)))
# ... и через несколько шагов — терм, альфа-эквивалентный числу 2

Сложность: каждый шаг — обход терма, то есть O(размер терма) по времени; число шагов в худшем случае неограниченно (нетипизированное исчисление полно по Тьюрингу, так что проблема остановки применима — см. вычислимость). Память — O(глубина рекурсии + размер текущего терма).

Аналог на JavaScript пишется один в один; если хотите, добавьте счётчик редексов и сравните нормальный порядок с аппликативным (меняется только то, редуцируем ли a до проверки f) — увидите разницу из восьмой статьи на живых числах.

Упражнения

Сведите к нормальной форме, выписывая каждый шаг. Ответы ниже.

1. (λx. λy. x y) (λz. z) w

2. (λf. λx. f (f x)) (λn. n + 3) 4 (арифметику считайте встроенной)

3. (λx. λy. x y) y — осторожно с именами.

4. (λx. λy. x) a ((λz. z z) (λz. z z)) в нормальном порядке. Что будет в аппликативном?

5. Что напечатает код и почему:

const fs = [];
for (var i = 0; i < 2; i++) fs.push(() => i);
console.log(fs[0](), fs[1]());

6. Верна ли эта-редукция здесь: ["10","10","10"].map(x => Number(x)) → ["10","10","10"].map(Number)? А для parseInt?

Ответ 1.

Шаг 0.  (λx. λy. x y) (λz. z) w
Шаг 1.  аппликация левоассоциативна: ((λx. λy. x y) (λz. z)) w
Шаг 2.  внешний левый редекс — внутренняя аппликация; бета по x := (λz. z):
        (λy. (λz. z) y)
Шаг 3.  (λy. (λz. z) y) w
Шаг 4.  бета по y := w:  (λz. z) w
Шаг 5.  бета по z := w:  w
Нормальная форма: w

Между шагами 2 и 3 в теле сидит эта-редекс λy. (λz. z) y, который эта-редуцируется прямо в λz. z — короткий путь даёт тот же ответ, как и обещает теорема Чёрча–Россера.

Ответ 2.

Шаг 0.  (λf. λx. f (f x)) (λn. n + 3) 4
Шаг 1.  ((λf. λx. f (f x)) (λn. n + 3)) 4
Шаг 2.  бета по f := (λn. n + 3):
        (λx. (λn. n + 3) ((λn. n + 3) x))
Шаг 3.  применяем к 4:
        (λn. n + 3) ((λn. n + 3) 4)
Шаг 4.  нормальный порядок — редуцируем внешний редекс, по n := ((λn. n + 3) 4):
        ((λn. n + 3) 4) + 3
Шаг 5.  внутренний редекс:  (4 + 3) + 3
Шаг 6.  7 + 3
Шаг 7.  10

Это TWO succ 4 — двукратное применение, ровно как в числах Чёрча.

Ответ 3.

Шаг 0.  (λx. λy. x y) y
        внешняя y — свободная, внутри абстракции y — связанная. Разные переменные!
Шаг 1.  наивная подстановка дала бы λy. y y — свободная y попала под связку. Это захват.
Шаг 2.  альфа-конверсия связанной переменной: (λx. λv. x v) y
Шаг 3.  бета по x := y:  λv. y v
Нормальная форма: λv. y v   (и эта-редукцией она сводится к самой y)

Ответ 4.

Обозначим Ω = (λz. z z) (λz. z z) — терм, который редуцируется сам в себя вечно.

Нормальный порядок (самый левый внешний редекс):
Шаг 0.  ((λx. λy. x) a) Ω
Шаг 1.  бета по x := a:  (λy. a) Ω
Шаг 2.  бета по y := Ω — y не встречается в теле, аргумент выбрасывается: a
Ответ: a  за два шага.

Аппликативный порядок (сначала нормализуем аргумент):
Шаг 0.  (λy. a) Ω
Шаг 1.  нормализуем Ω:  (λz. z z) (λz. z z) → (λz. z z) (λz. z z) → ...
Ответ: не завершается.

Это стандартная демонстрация теоремы о нормализации: если нормальная форма существует, нормальный порядок её найдёт, аппликативный — не обязательно. Именно поэтому Haskell (ленивый) вернёт результат там, где Python зациклится.

Ответ 5. Напечатает 2 2. var i — одна связка на всю функцию; обе стрелочные функции ссылаются на одну и ту же свободную переменную, а после выхода из цикла её значение равно 2 (условие i < 2 нарушилось именно при i = 2). С let было бы 0 1.

Ответ 6. Для Number — верна: Number использует только первый аргумент, лишние индекс и массив игнорирует, результат совпадает. Для parseInt — неверна: он принимает второй аргумент radix, и map передаст туда индекс. ["10","10","10"].map(parseInt) даст [10, NaN, 2] (radix 0 → по умолчанию 10; radix 1 → недопустимо, NaN; radix 2 → “10” в двоичной = 2). Эта-редукция корректна только для функций, чья арность действительно равна одному.

Мини-итог трека

  • Стрелочная функция — это лямбда-абстракция, вызов — аппликация, а вычисление вызова — бета-редукция. Разница между учебником и вашим редактором чисто нотационная.
  • let, аргументы по умолчанию, IIFE, блочные выражения — сахар над аппликацией. Ландин показал это в 1966-м, с тех пор ничего не изменилось.
  • Замыкание — инженерная реализация подстановки: тело не переписывается, значения свободных переменных носятся рядом. Лексическая область видимости — это отказ от захвата имён.
  • Альфа-конверсия работает в минификаторах и гигиенических макросах; эта-редукция — в советах линтера; индексы де Брёйна — во внутренностях пруф-ассистентов.
  • Порядок вычисления — не абстракция: он определяет, зациклится программа или нет, и почему && нельзя написать функцией в строгом языке.
  • Компиляторы функциональных языков в буквальном смысле переводят программу в типизированное лямбда-исчисление и оптимизируют её редукциями.

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

Что дальше

Трек закончен — дальше расходятся три дороги.

Практика. Всё, что мы кодировали в лямбдах, в рабочем коде выглядит как функции высшего порядка, композиция и типы данных. Идите в трек функционального программирования: обзор, композиция и каррирование, ФП в мейнстрим-языках и архитектура на ФП.

Теория. Лямбда-исчисление — одна из трёх эквивалентных моделей вычислимости, а типы — это логика. Смотрите вычислимость, логику и доказательства, основы теории категорий и теорию категорий в программировании.

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

Не знаете, что брать следующим, — загляните в дорожную карту портала: там треки выстроены в порядке, в котором они друг друга поддерживают.

Источники

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

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

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

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