Практика 2. Рекурсия в λ-исчислении

осень 2026

Андрей Стоян, Илья Колегов

осень 2026

Летучка 2

Летучка 2 · 7 минут · Ваше ФИ: ____________________

  1. Функция двух аргументов записана как функция одного аргумента, возвращающая функцию. Как называется этот приём? ________________

  2. Заполните пропуски в умножении из домашки: \mathbf{mult} := \lambda n\,m.\,\mathbf{natElim}\ n ____________ ____

  3. Сделайте один β-шаг: \ (\lambda x.\,\lambda y.\,x)\ y\ \rightsquigarrow ________________

  4. Python вычисляет аргументы до вызова функции. Как корректно реализовать собственную абстракцию над if? Реализуйте рекурсивный факториал.

    def myif(c, t, e): return ________________________
def fac(n): return myif(n <= 1, ________________, ________________)

Условное выражение как функция

Эквивалентен ли код?


if b:
    return f()
else:
    return g()
def myif(cond, t, e):
    if cond:
        return t
    else:
        return e
myif(b, f(), g())

Нет: Python вычисляет аргументы до вызова, поэтому fac через myif не завершается.

def fac(n): return myif(n <= 1, 1, n * fac(n - 1))
fac(3) -> myif(3 <= 1, 1, 3 * fac(2))
       -> myif(3 <= 1, 1, 3 * myif(2 <= 1, 1, 2 * fac(1)))
       -> myif(3 <= 1, 1, 3 * myif(2 <= 1, 1, 2 * myif(1 <= 1, 1, 1 * fac(0))))
       ...

Перейдём к ленивой семантике вручную — с помощью абстракций:

def fac(n):
    return myif(n <= 1,
        lambda: 1,
        lambda: n * fac(n - 1)
    )
def myif(cond, t, e):
    if cond:
        return t()
    else:
        return e()

Ещё метаинформация о курсе

Туториал по прохождению

  • Перед парой перечитайте лекцию — всего 15 минут, но очень поможет нам на практиках
  • Управляйте временем и ресурсами
  • Рефлексируйте над неудачами — спокойно, работая с причинами: не «я не могу», а «чего не хватило: времени, определения, примера»
  • Застряли на 20 минут — спрашивайте — преподавателей, одногруппников, в чате; молчаливое непонимание грустно, а вопрос одного экономит время десятерым
  • Спите и отдыхайте — на дистанции семестра это не роскошь, а производительность

Полезная памятка от кураторов Computer Science Center.

Цикл без рекурсии

Факториал без рекурсии

\mathbf{natElim}\ n\ s\ z повторяет шаг s над z ровно n раз: при известном числе итераций рекурсия не нужна.

def fac(n):
    i, acc = 1, 1
    for _ in range(n):
        i, acc = i + 1, i * acc
    return acc

Закодируйте \mathbf{fac} через \mathbf{natElim}. Цикл выше держит две переменные, а \mathbf{natElim} протаскивает через шаги один терм. Что это за терм и каким будет шаг?

Состояние — пара «номер шага, накопленное произведение»:

\begin{alignedat}{2} &\mathbf{start} &&\ := \mathbf{pair}\ \mathbf{1}\ \mathbf{1} \\ &\mathbf{step} &&\ := \lambda p.\,\mathbf{pair}\ \underbrace{(\mathbf{suc}\ (\mathbf{fst}\ p))}_{\text{номер шага}}\ \underbrace{(\mathbf{mult}\ (\mathbf{fst}\ p)\ (\mathbf{snd}\ p))}_{\text{произведение}} \\[1.2em] &\mathbf{fac} &&\ := \lambda n.\,\mathbf{snd}\ (\mathbf{natElim}\ n\ \mathbf{step}\ \mathbf{start}) \end{alignedat}

Выбираем правильный уровень абстракции для рассуждений

\begin{alignedat}{2} & &&\ \mathbf{fac}\ \mathbf{3} \\ &\twoheadrightarrow &&\ \mathbf{snd}\ ((\lambda s\,z.\,s\ (s\ (s\ z)))\ (\lambda p.\,\mathbf{pair}\ (\mathbf{suc}\ (\mathbf{fst}\ p))\ (\mathbf{mult}\ (\mathbf{fst}\ p)\ (\mathbf{snd}\ p)))\ (\mathbf{pair}\ \mathbf{1}\ \mathbf{1})) \\ &\twoheadrightarrow &&\ (\lambda q.\,q\ \mathbf{K}_*)\ ((\lambda p.\,\mathbf{pair}\ (\mathbf{suc}\ (\mathbf{fst}\ p))\ \ldots)\ ((\lambda p.\,\ldots)\ ((\lambda p.\,\ldots)\ ((\lambda x\,y\,f.\,f\ x\ y)\ \mathbf{1}\ \mathbf{1})))) \\ &\twoheadrightarrow &&\ \ldots \text{ и ещё десяток строк, каждая длиннее предыдущей. Да ну серьёзно??} \end{alignedat}

Раскрывать до \lambda незачем: законы \mathbf{natElim} и пар уже доказаны, это «большие шаги»:

\begin{alignedat}{2} & &&\ \mathbf{fac}\ \mathbf{3} \\ &\rightsquigarrow_{\mathbf{fac}} &&\ \mathbf{snd}\ (\mathbf{natElim}\ \mathbf{3}\ \mathbf{step}\ \mathbf{start}) \\ &\twoheadrightarrow &&\ \mathbf{snd}\ (\mathbf{step}\ (\mathbf{step}\ (\mathbf{step}\ \mathbf{start}))) \qquad \text{законы } \mathbf{natElim} \\ &\twoheadrightarrow &&\ \mathbf{snd}\ (\mathbf{step}\ (\mathbf{step}\ (\mathbf{pair}\ \mathbf{2}\ \mathbf{1}))) \qquad \text{законы пар, } \mathbf{mult}\ \mathbf{1}\ \mathbf{1} \twoheadrightarrow \mathbf{1} \\ &\twoheadrightarrow &&\ \mathbf{snd}\ (\mathbf{step}\ (\mathbf{pair}\ \mathbf{3}\ \mathbf{2})) \twoheadrightarrow \mathbf{snd}\ (\mathbf{pair}\ \mathbf{4}\ \mathbf{6}) \twoheadrightarrow \mathbf{6} \end{alignedat}

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

Рекурсия

  • Одного цикла с фиксированным числом итераций недостаточно, чтобы уметь всё
  • Чтобы добиться вычислительной полноты, нужна полноценная рекурсия
  • В прикладные языки рекурсия встроена — достаточно в теле именованной функции вызвать её саму
  • Но у нас в языке нет именованных функций, же?!

С лекции: рекурсия как неподвижная точка

  1. Хотим терм \mathbf{fac}, удовлетворяющий рекурсивному уравнению: \mathbf{fac}\ n =_\beta \mathbf{if}\ (\mathbf{isZero}\ n)\ \mathbf{1}\ (\mathbf{mult}\ n\ (\boxed{\mathbf{fac}}\ (\mathbf{pred}\ n)))
  1. Абстрагируем правую часть по имени и по аргументу: \mathbf{fac}\ n =_\beta \underbrace{(\lambda \boxed{r}\,\boxed{n}.\,\mathbf{if}\ (\mathbf{isZero}\ \boxed{n})\ \mathbf{1}\ (\mathbf{mult}\ \boxed{n}\ (\boxed{r}\ (\mathbf{pred}\ \boxed{n}))))}_{\mathbf{fac'}}\ \mathbf{fac}\ n
  1. Правые аргументы совпадают, остаётся \mathbf{fac} =_\beta \mathbf{fac'}\ \mathbf{fac}: искомое — неподвижная точка \mathbf{fac'}, а её даёт комбинатор, так как \underbrace{\mathbf{Y}\ F}_{X} =_\beta F\ (\underbrace{\mathbf{Y}\ F}_{X}): \mathbf{fac} := \mathbf{Y}\ \mathbf{fac'} \equiv \mathbf{Y}\ (\lambda r\,n.\,\mathbf{if}\ (\mathbf{isZero}\ n)\ \mathbf{1}\ (\mathbf{mult}\ n\ (r\ (\mathbf{pred}\ n))))
  • Δ Свойство комбинатора неподвижной точки \mathbf{Y}\ F =_\beta F\ (\mathbf{Y}\ F) — единственное, что нужно знать про \mathbf{Y}, чтобы им пользоваться

Как работает Y: fac 3

Раскрыли имя \mathbf{fac}. Дальше единственный инструмент — свойство \mathbf{Y}\ F =_\beta F\ (\mathbf{Y}\ F).

Y fac′ 3

цепочка

\mathbf{fac}\ \mathbf{3} \rightsquigarrow_{\mathbf{fac}} \mathbf{Y}\ \mathbf{fac'}\ \mathbf{3}

Как работает Y: fac 3

Свойство \mathbf{Y}: наружу вышла копия \mathbf{fac'}, а внутри остался ещё один \mathbf{Y}\ \mathbf{fac'} — запас на следующую итерацию.

fac′ (Y fac′) 3

цепочка

\mathbf{fac}\ \mathbf{3} \rightsquigarrow_{\mathbf{fac}} \mathbf{Y}\ \mathbf{fac'}\ \mathbf{3}

=_\beta\ \mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{3} — свойство \mathbf{Y}

Как работает Y: fac 3

Два β-шага: r стало копией \mathbf{Y}\ \mathbf{fac'}, n стало \mathbf{3}. Перед нами тело \mathbf{fac'}, в нём никакой рекурсии.

if (isZero 3) 1 (mult 3 (Y fac′ (pred 3)))

цепочка

\mathbf{fac}\ \mathbf{3} \rightsquigarrow_{\mathbf{fac}} \mathbf{Y}\ \mathbf{fac'}\ \mathbf{3}

=_\beta\ \mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{3} — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{if}\ (\mathbf{isZero}\ \mathbf{3})\ \mathbf{1}

\qquad (\mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ (\mathbf{pred}\ \mathbf{3}))) — два β-шага

Как работает Y: fac 3

\mathbf{isZero}\ \mathbf{3} ложно, \mathbf{if} выбрал ветку else, \mathbf{pred}\ \mathbf{3} \twoheadrightarrow \mathbf{2}. Снаружи остался \mathbf{mult}\ \mathbf{3}, внутри — тот же кадр, что в начале.

mult 3 (Y fac′ 2)

цепочка

\mathbf{fac}\ \mathbf{3} \rightsquigarrow_{\mathbf{fac}} \mathbf{Y}\ \mathbf{fac'}\ \mathbf{3}

=_\beta\ \mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{3} — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{if}\ (\mathbf{isZero}\ \mathbf{3})\ \mathbf{1}

\qquad (\mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ (\mathbf{pred}\ \mathbf{3}))) — два β-шага

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{2}) — законы \mathbf{isZero}, \mathbf{if}, \mathbf{pred}

Как работает Y: fac 3

Вторая итерация: снова свойство \mathbf{Y}, снова копия \mathbf{fac'} наружу.

mult 3 (fac′ (Y fac′) 2)

цепочка

\mathbf{fac}\ \mathbf{3} \rightsquigarrow_{\mathbf{fac}} \mathbf{Y}\ \mathbf{fac'}\ \mathbf{3}

=_\beta\ \mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{3} — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{if}\ (\mathbf{isZero}\ \mathbf{3})\ \mathbf{1}

\qquad (\mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ (\mathbf{pred}\ \mathbf{3}))) — два β-шага

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{2}) — законы \mathbf{isZero}, \mathbf{if}, \mathbf{pred}

=_\beta\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{2}) — свойство \mathbf{Y}

Как работает Y: fac 3

И снова β-шаги и условие. Каждая итерация оставляет снаружи один \mathbf{mult}.

mult 3 (mult 2 (Y fac′ 1))

цепочка

\mathbf{fac}\ \mathbf{3} \rightsquigarrow_{\mathbf{fac}} \mathbf{Y}\ \mathbf{fac'}\ \mathbf{3}

=_\beta\ \mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{3} — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{if}\ (\mathbf{isZero}\ \mathbf{3})\ \mathbf{1}

\qquad (\mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ (\mathbf{pred}\ \mathbf{3}))) — два β-шага

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{2}) — законы \mathbf{isZero}, \mathbf{if}, \mathbf{pred}

=_\beta\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{2}) — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{mult}\ \mathbf{2}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{1})) — как выше

Как работает Y: fac 3

Третья итерация проходит так же: копия, β-шаги, условие ложно, снаружи ещё один \mathbf{mult}.

mult 3 (mult 2 (mult 1 (Y fac′ 0)))

цепочка

\mathbf{fac}\ \mathbf{3} \rightsquigarrow_{\mathbf{fac}} \mathbf{Y}\ \mathbf{fac'}\ \mathbf{3}

=_\beta\ \mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{3} — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{if}\ (\mathbf{isZero}\ \mathbf{3})\ \mathbf{1}

\qquad (\mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ (\mathbf{pred}\ \mathbf{3}))) — два β-шага

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{2}) — законы \mathbf{isZero}, \mathbf{if}, \mathbf{pred}

=_\beta\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{2}) — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{mult}\ \mathbf{2}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{1})) — как выше

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{mult}\ \mathbf{2}\ (\mathbf{mult}\ \mathbf{1}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{0}))) — итерация 3

Как работает Y: fac 3

Четвёртая итерация: копия, β-шаги, и на этот раз \mathbf{isZero}\ \mathbf{0} истинно.

mult 3 (mult 2 (mult 1 (if (isZero 0) 1 (mult 0 (Y fac′ (pred 0))))))

цепочка

\mathbf{fac}\ \mathbf{3} \rightsquigarrow_{\mathbf{fac}} \mathbf{Y}\ \mathbf{fac'}\ \mathbf{3}

=_\beta\ \mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{3} — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{if}\ (\mathbf{isZero}\ \mathbf{3})\ \mathbf{1}

\qquad (\mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ (\mathbf{pred}\ \mathbf{3}))) — два β-шага

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{2}) — законы \mathbf{isZero}, \mathbf{if}, \mathbf{pred}

=_\beta\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{2}) — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{mult}\ \mathbf{2}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{1})) — как выше

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{mult}\ \mathbf{2}\ (\mathbf{mult}\ \mathbf{1}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{0}))) — итерация 3

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{mult}\ \mathbf{2}\ (\mathbf{mult}\ \mathbf{1}\ (\mathbf{if}\ (\mathbf{isZero}\ \mathbf{0})\ \mathbf{1}

\qquad (\mathbf{mult}\ \mathbf{0}\ (\mathbf{Y}\ \mathbf{fac'}\ (\mathbf{pred}\ \mathbf{0})))))) — итерация 4

Как работает Y: fac 3

\mathbf{if} вернул \mathbf{1}, а ветка с \mathbf{Y}\ \mathbf{fac'}\ (\mathbf{pred}\ \mathbf{0}) выброшена, так и не раскрывшись. \mathbf{Y} разворачивался ровно столько раз, сколько потребовало условие.

mult 3 (mult 2 (mult 1 1)) ↠ 6

цепочка

\mathbf{fac}\ \mathbf{3} \rightsquigarrow_{\mathbf{fac}} \mathbf{Y}\ \mathbf{fac'}\ \mathbf{3}

=_\beta\ \mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{3} — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{if}\ (\mathbf{isZero}\ \mathbf{3})\ \mathbf{1}

\qquad (\mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ (\mathbf{pred}\ \mathbf{3}))) — два β-шага

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{2}) — законы \mathbf{isZero}, \mathbf{if}, \mathbf{pred}

=_\beta\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{fac'}\ (\mathbf{Y}\ \mathbf{fac'})\ \mathbf{2}) — свойство \mathbf{Y}

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{mult}\ \mathbf{2}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{1})) — как выше

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{mult}\ \mathbf{2}\ (\mathbf{mult}\ \mathbf{1}\ (\mathbf{Y}\ \mathbf{fac'}\ \mathbf{0}))) — итерация 3

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{mult}\ \mathbf{2}\ (\mathbf{mult}\ \mathbf{1}\ (\mathbf{if}\ (\mathbf{isZero}\ \mathbf{0})\ \mathbf{1}

\qquad (\mathbf{mult}\ \mathbf{0}\ (\mathbf{Y}\ \mathbf{fac'}\ (\mathbf{pred}\ \mathbf{0})))))) — итерация 4

\twoheadrightarrow\ \mathbf{mult}\ \mathbf{3}\ (\mathbf{mult}\ \mathbf{2}\ (\mathbf{mult}\ \mathbf{1}\ \mathbf{1})) \twoheadrightarrow \mathbf{6} — закон \mathbf{if}

Рекурсивное уравнение: fib

Реализуйте \mathbf{fib}\ n — n-е число Фибоначчи: запишите рекурсивное уравнение и решите его через \mathbf{Y}. Считайте, что \mathbf{le}, \mathbf{plus} и \mathbf{minus} уже есть.

  1. Уравнение: \ \mathbf{fib}\ n =_\beta \mathbf{if}\ (\mathbf{le}\ n\ \mathbf{2})\ \mathbf{1}\ (\mathbf{plus}\ (\mathbf{fib}\ (\mathbf{minus}\ n\ \mathbf{1}))\ (\mathbf{fib}\ (\mathbf{minus}\ n\ \mathbf{2})))
  2. Абстрагируем правую часть по имени и аргументу: \ \mathbf{fib'} := \lambda r\,n.\,\mathbf{if}\ (\mathbf{le}\ n\ \mathbf{2})\ \mathbf{1}\ (\mathbf{plus}\ (r\ (\mathbf{minus}\ n\ \mathbf{1}))\ (r\ (\mathbf{minus}\ n\ \mathbf{2}))), и уравнение стало \mathbf{fib} =_\beta \mathbf{fib'}\ \mathbf{fib}
  3. Решение: \ \mathbf{fib} := \mathbf{Y}\ \mathbf{fib'}

Найдите F такой, что F =_\beta M\ F для произвольного M.

Уравнение уже имеет вид «F — неподвижная точка M», абстрагировать нечего: F := \mathbf{Y}\ M

Кодирование данных

Варианты

Значения-варианты

Одна сущность бывает нескольких видов, и обрабатывать их нужно разным кодом: пользователь авторизован или нет, вершина выражения — константа или сложение.

def eval(node):
    if is_const(node):
        return node.value  # у константы должно быть значение
    elif is_plus(node):
        return eval(node.left) + eval(node.right)  # у плюса — операнды

API вариантов

  • Два конструктора: «левый» \mathbf{inl} и «правый» \mathbf{inr}, каждый принимает одно значение
  • Элиминатор \mathbf{either} выполняет одну из двух переданных ему функций в зависимости от варианта

Законы вариантов

  1. \mathbf{either}\ F\ G\ (\mathbf{inl}\ N) =_\beta F\ N
  2. \mathbf{either}\ F\ G\ (\mathbf{inr}\ M) =_\beta G\ M

Закодируйте варианты

Законы вариантов \quad \mathbf{either}\ F\ G\ (\mathbf{inl}\ N) =_\beta F\ N, \qquad \mathbf{either}\ F\ G\ (\mathbf{inr}\ M) =_\beta G\ M

Закодируйте варианты: \mathbf{inl}, \mathbf{inr} и \mathbf{either}, удовлетворяющие законам. Способов не меньше двух.

Через пары с тегом: булев тег говорит, какой это вариант, а \mathbf{either} выбирает код по тегу

\mathbf{inl} := \lambda x.\,\mathbf{pair}\ \mathbf{true}\ x\quad \mathbf{inr} := \lambda y.\,\mathbf{pair}\ \mathbf{false}\ y

\mathbf{either} := \lambda f\,g\,v.\,\mathbf{if}\ (\mathbf{fst}\ v)\ (f\ (\mathbf{snd}\ v))\ (g\ (\mathbf{snd}\ v))

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

\mathbf{inl} := \lambda x.\,\lambda f\,g.\,f\ x, \quad \mathbf{inr} := \lambda y.\,\lambda f\,g.\,g\ y, \quad \mathbf{either} := \lambda f\,g\,v.\,v\ f\ g

Списки

Списки

Иногда требуется хранить много сущностей одновременно, и при этом:

  • Уметь добавить в коллекцию новую сущность
  • Найти сущность в коллекции по индексу
1
2
3
4

Моделируем список

API списков

  • \mathbf{nil} — пустой список
  • \mathbf{cons}\ x\ t — список из элемента x в голове и списка-хвоста t
  • e.g. [\mathbf{1}, \mathbf{2}, \mathbf{3}] \equiv \mathbf{cons}\ \mathbf{1}\ (\mathbf{cons}\ \mathbf{2}\ (\mathbf{cons}\ \mathbf{3}\ \mathbf{nil}))
  • Элиминатор, аккумулирующий элементы: \mathbf{fold}
  • e.g. \mathbf{fold}\ [\mathbf{1}, \mathbf{2}, \mathbf{3}]\ F\ Z =_\beta F\ \mathbf{1}\ (F\ \mathbf{2}\ (F\ \mathbf{3}\ Z))

Законы списков

  1. \mathbf{fold}\ \mathbf{nil}\ F\ Z =_\beta Z
  2. \mathbf{fold}\ (\mathbf{cons}\ N\ M)\ F\ Z =_\beta F\ N\ (\mathbf{fold}\ M\ F\ Z)

Закодируйте списки

Закодируйте списки: \mathbf{nil}, \mathbf{cons} и \mathbf{fold}, удовлетворяющие законам. Способов снова не меньше двух: через варианты и пары или по Чёрчу, по образцу чисел.

Через варианты: список либо пуст, либо пара «голова, хвост»; \mathbf{fold} рекурсивен, нужен \mathbf{Y}

\begin{alignedat}{2} &\mathbf{nil} &&\ := \mathbf{inl}\ \mathbf{0} \\ &\mathbf{cons} &&\ := \lambda x\,t.\,\mathbf{inr}\ (\mathbf{pair}\ x\ t) \\ &\mathbf{fold} &&\ := \mathbf{Y}\ (\lambda r\,xs\,f\,z.\,\mathbf{either}\ \underbrace{(\mathbf{K}\ z)}_{\text{для } \mathbf{inl}}\ \underbrace{(\lambda p.\,f\ (\mathbf{fst}\ p)\ (r\ (\mathbf{snd}\ p)\ f\ z))}_{\text{для } \mathbf{inr}\text{: голова и свёртка хвоста}}\ xs) \end{alignedat}

По Чёрчу: как число применяет шаг k раз, список применяет шаг к каждому элементу; \mathbf{fold} снова \mathbf{I}

\mathbf{nil} := \lambda s\,z.\,z, \qquad \mathbf{cons} := \lambda x\,t.\,\lambda s\,z.\,s\ x\ (t\ s\ z), \qquad \mathbf{fold} := \lambda xs\,f\,z.\,xs\ f\ z

Как работает fold на вариантах: [1, 2]

Список через варианты: [\mathbf{1}, \mathbf{2}] \equiv \mathbf{inr}\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}]), где [\mathbf{2}] \equiv \mathbf{inr}\ (\mathbf{pair}\ \mathbf{2}\ [\,]) и [\,] \equiv \mathbf{inl}\ \mathbf{0}. Считаем \mathbf{fold} законами \mathbf{either} и пар.

fold [1, 2] f z

цепочка

\mathbf{fold}\ [\mathbf{1}, \mathbf{2}]\ f\ z

Как работает fold на вариантах: [1, 2]

Раскрыли \mathbf{fold} по свойству \mathbf{Y} и сделали β-шаги: \mathbf{either} с двумя ветками смотрит на xs, а это \mathbf{inr}-вершина.

either (K z) (λp. …) (inr (pair 1 [2]))

цепочка

\mathbf{fold}\ [\mathbf{1}, \mathbf{2}]\ f\ z

\twoheadrightarrow\ \mathbf{either}\ (\mathbf{K}\ z)\ (\lambda p.\,\ldots)

\qquad (\mathbf{inr}\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}])) — раскрыли \mathbf{fold}

Как работает fold на вариантах: [1, 2]

Закон \mathbf{either} для \mathbf{inr} выбрал вторую ветку и отдал ей пару. Вот теперь её тело важно: голова и свёртка хвоста.

(λp. f (fst p) (fold (snd p) f z)) (pair 1 [2])

цепочка

\mathbf{fold}\ [\mathbf{1}, \mathbf{2}]\ f\ z

\twoheadrightarrow\ \mathbf{either}\ (\mathbf{K}\ z)\ (\lambda p.\,\ldots)

\qquad (\mathbf{inr}\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}])) — раскрыли \mathbf{fold}

\twoheadrightarrow\ (\lambda p.\,\ldots)\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}]) — закон \mathbf{either} для \mathbf{inr}

Как работает fold на вариантах: [1, 2]

Законы пар достали голову и хвост. Снаружи остался f\ \mathbf{1}, внутри — тот же \mathbf{fold} на хвосте.

f 1 (fold [2] f z)

цепочка

\mathbf{fold}\ [\mathbf{1}, \mathbf{2}]\ f\ z

\twoheadrightarrow\ \mathbf{either}\ (\mathbf{K}\ z)\ (\lambda p.\,\ldots)

\qquad (\mathbf{inr}\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}])) — раскрыли \mathbf{fold}

\twoheadrightarrow\ (\lambda p.\,\ldots)\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}]) — закон \mathbf{either} для \mathbf{inr}

\twoheadrightarrow\ f\ \mathbf{1}\ (\mathbf{fold}\ [\mathbf{2}]\ f\ z) — законы пар

Как работает fold на вариантах: [1, 2]

Вторая вершина проходит так же: ещё один вызов f снаружи.

f 1 (f 2 (fold [] f z))

цепочка

\mathbf{fold}\ [\mathbf{1}, \mathbf{2}]\ f\ z

\twoheadrightarrow\ \mathbf{either}\ (\mathbf{K}\ z)\ (\lambda p.\,\ldots)

\qquad (\mathbf{inr}\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}])) — раскрыли \mathbf{fold}

\twoheadrightarrow\ (\lambda p.\,\ldots)\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}]) — закон \mathbf{either} для \mathbf{inr}

\twoheadrightarrow\ f\ \mathbf{1}\ (\mathbf{fold}\ [\mathbf{2}]\ f\ z) — законы пар

\twoheadrightarrow\ f\ \mathbf{1}\ (f\ \mathbf{2}\ (\mathbf{fold}\ [\,]\ f\ z)) — вторая вершина

Как работает fold на вариантах: [1, 2]

Дошли до \mathbf{inl}: закон \mathbf{either} для \mathbf{inl} выбирает \mathbf{K}\ z, и что бы ни лежало в конце, ответ z.

f 1 (f 2 (either (K z) (λp. …) (inl 0)))

цепочка

\mathbf{fold}\ [\mathbf{1}, \mathbf{2}]\ f\ z

\twoheadrightarrow\ \mathbf{either}\ (\mathbf{K}\ z)\ (\lambda p.\,\ldots)

\qquad (\mathbf{inr}\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}])) — раскрыли \mathbf{fold}

\twoheadrightarrow\ (\lambda p.\,\ldots)\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}]) — закон \mathbf{either} для \mathbf{inr}

\twoheadrightarrow\ f\ \mathbf{1}\ (\mathbf{fold}\ [\mathbf{2}]\ f\ z) — законы пар

\twoheadrightarrow\ f\ \mathbf{1}\ (f\ \mathbf{2}\ (\mathbf{fold}\ [\,]\ f\ z)) — вторая вершина

\twoheadrightarrow\ f\ \mathbf{1}\ (f\ \mathbf{2}\ (\mathbf{either}\ (\mathbf{K}\ z)\ (\lambda p.\,\ldots)\ (\mathbf{inl}\ \mathbf{0})))

Как работает fold на вариантах: [1, 2]

Ровно законы \mathbf{fold}: каждый \mathbf{cons} дал вызов f, \mathbf{nil} дал z. Список через варианты обходится рекурсией через \mathbf{Y}; список Чёрча делает то же сам.

f 1 (f 2 (z))

цепочка

\mathbf{fold}\ [\mathbf{1}, \mathbf{2}]\ f\ z

\twoheadrightarrow\ \mathbf{either}\ (\mathbf{K}\ z)\ (\lambda p.\,\ldots)

\qquad (\mathbf{inr}\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}])) — раскрыли \mathbf{fold}

\twoheadrightarrow\ (\lambda p.\,\ldots)\ (\mathbf{pair}\ \mathbf{1}\ [\mathbf{2}]) — закон \mathbf{either} для \mathbf{inr}

\twoheadrightarrow\ f\ \mathbf{1}\ (\mathbf{fold}\ [\mathbf{2}]\ f\ z) — законы пар

\twoheadrightarrow\ f\ \mathbf{1}\ (f\ \mathbf{2}\ (\mathbf{fold}\ [\,]\ f\ z)) — вторая вершина

\twoheadrightarrow\ f\ \mathbf{1}\ (f\ \mathbf{2}\ (\mathbf{either}\ (\mathbf{K}\ z)\ (\lambda p.\,\ldots)\ (\mathbf{inl}\ \mathbf{0})))

\twoheadrightarrow\ f\ \mathbf{1}\ (f\ \mathbf{2}\ (\mathbf{K}\ z\ \mathbf{0})) \twoheadrightarrow f\ \mathbf{1}\ (f\ \mathbf{2}\ z) — закон \mathbf{either} для \mathbf{inl}

Список и вариант вместе

Реализуйте \mathbf{safeHead}: голову списка как вариант, чтобы пустой список не был ошибкой, а возвращал значение по умолчанию. Спецификация:

  • \mathbf{safeHead}\ D\ \mathbf{nil} =_\beta \mathbf{inl}\ D
  • \mathbf{safeHead}\ D\ (\mathbf{cons}\ N\ M) =_\beta \mathbf{inr}\ N.

\mathbf{safeHead} := \lambda d\,xs.\,\mathbf{fold}\ xs\ \underbrace{(\lambda x\,t.\,\mathbf{inr}\ x)}_{\text{для } \mathbf{cons}}\ \underbrace{(\mathbf{inl}\ d)}_{\text{для } \mathbf{nil}}

Шаг игнорирует результат для хвоста r и оборачивает голову; для пустого списка \mathbf{fold} возвращает начальное значение \mathbf{inl}\ d. Работает с любым из двух кодирований — мы пользовались только законами.

Наш язык на сегодня

Две пары назад в языке были только переменные, абстракция и аппликация. Всё ниже собрано из них.

комбинаторы лекция 1 \mathbf{I}\quad \mathbf{K}\quad \mathbf{K}_*\quad \mathbf{S}\quad \mathbf{B}
пары П1 \mathbf{pair}\quad \mathbf{fst}\quad \mathbf{snd}\quad \mathbf{swap}
логика П1 \mathbf{true}\quad \mathbf{false}\quad \mathbf{if}\quad \mathbf{not}\quad \mathbf{and}\quad \mathbf{or}
числа П1, hw01 \mathbf{0}\quad \mathbf{suc}\quad \mathbf{natElim}\quad \mathbf{plus}\quad \mathbf{mult}\quad \mathbf{isZero}\quad \mathbf{isEven}
циклы П2 состояние-пара через \mathbf{natElim}: \quad\mathbf{fac}\quad \mathbf{pred}
рекурсия лекция 2, П2 \mathbf{Y}\quad \mathbf{fac}\quad \mathbf{fib}
варианты П2 \mathbf{inl}\quad \mathbf{inr}\quad \mathbf{either}
списки П2 \mathbf{nil}\quad \mathbf{cons}\quad \mathbf{fold}\quad \mathbf{safeHead}

Сегодня мы узнали много нового

  • Число итераций известно заранее — рекурсия не нужна
  • Число шагов решается по ходу — рекурсивное уравнение: абстрагировать по имени и аргументу, взять неподвижную точку через \mathbf{Y}
  • Проверяем законами, «большими шагами», а не раскрытием до \lambda
  • Переизобрели варианты (суммы) и списки (коллекции)

Материалы ☁

Выбор инструмента: цикл с фиксированным числом итераций vs рекурсия ⚙

  • Цикл с фиксированным числом итераций
    • Задаёт процесс из конечного, заранее заданного, количества шагов
    • Аналог цикла for in range в современных языках
  • Рекурсия
    • Количество шагов определяется в процессе (и никак иначе: halting problem)
    • Завершение процесса определяется выполнением произвольного условия (базы рекурсии)
    • В современных языках выражается рекурсией1 и циклом while condition: ...
  • Всегда нужно выбирать наименее могущественный из подходящих инструментов
    • Проще для рассуждений и доказательства свойств
    • Меньше пространство для ошибок
    • Скорее всего, код будет эффективнее исполняться
    • В частности, какие функции выражаются таким циклом, а какие — нет, рассказывает теория вычислимости (это и есть примитивно-рекурсивные функции)

Система рекурсивных уравнений

Взаимная рекурсия: две функции ссылаются друг на друга, а \mathbf{Y} ищет одну неподвижную точку.

\begin{cases} \mathbf{isEven}\ n =_\beta \mathbf{if}\ (\mathbf{isZero}\ n)\ \mathbf{true}\ (\mathbf{isOdd}\ (\mathbf{pred}\ n)) \\ \mathbf{isOdd}\ n =_\beta \mathbf{if}\ (\mathbf{isZero}\ n)\ \mathbf{false}\ (\mathbf{isEven}\ (\mathbf{pred}\ n)) \end{cases}

Две неизвестные упаковываем в одну пару p = \mathbf{pair}\ \mathbf{isEven}\ \mathbf{isOdd} и решаем уравнение на неё как обычно:

\begin{aligned} P := \mathbf{Y}\ (\lambda p.\,\mathbf{pair}\ &\underbrace{(\lambda n.\,\mathbf{if}\ (\mathbf{isZero}\ n)\ \mathbf{true}\ (\mathbf{snd}\ p\ (\mathbf{pred}\ n)))}_{\mathbf{isEven}\text{, где } \mathbf{snd}\ p \text{ — это } \mathbf{isOdd}} \\[1.4em] &\underbrace{(\lambda n.\,\mathbf{if}\ (\mathbf{isZero}\ n)\ \mathbf{false}\ (\mathbf{fst}\ p\ (\mathbf{pred}\ n)))}_{\mathbf{isOdd}\text{, где } \mathbf{fst}\ p \text{ — это } \mathbf{isEven}}) \end{aligned}

Тогда \mathbf{isEven} := \mathbf{fst}\ P, \quad \mathbf{isOdd} := \mathbf{snd}\ P. Пара третий раз за пару оказывается «состоянием»: в разминке, в \mathbf{pred} и здесь.

Объектно-ориентированная запись вариантов по Чёрчу

Как и у пар в П1: интерфейс с одним методом-элиминатором, по анонимному классу на конструктор. Захваченные аргументы конструктора — это то, что \lambda-терм \lambda f\,g.\,f\ x замыкает.

interface Variant<A, B> {
    fun <R> either(f: (A) -> R, g: (B) -> R): R
}

fun <A, B> inl(x: A): Variant<A, B> = object : Variant<A, B> {
    override fun <R> either(f: (A) -> R, g: (B) -> R): R = f(x)
}

fun <A, B> inr(y: B): Variant<A, B> = object : Variant<A, B> {
    override fun <R> either(f: (A) -> R, g: (B) -> R): R = g(y)
}

Тегированное кодирование в ООП — это поле tag и switch по нему в каждом месте использования. Кодирование по Чёрчу переносит выбор ветки в диспетчеризацию метода — паттерн «Visitor».

Объектно-ориентированная запись списков Чёрча

interface List<A> {
    fun <R> fold(s: (A, R) -> R, z: R): R
}

fun <A> nil(): List<A> = object : List<A> {
    override fun <R> fold(s: (A, R) -> R, z: R): R = z
}

fun <A> cons(x: A, t: List<A>): List<A> = object : List<A> {
    override fun <R> fold(s: (A, R) -> R, z: R): R = s(x, t.fold(s, z))
}

fun sum(xs: List<Int>): Int = xs.fold({ x, r -> x + r }, 0)

fun <A> concat(xs: List<A>, ys: List<A>): List<A> = xs.fold({ x, r -> cons(x, r) }, ys)

fun <A> safeHead(d: A, xs: List<A>): Either<A, A> = xs.fold({ x, _ -> inr(x) }, inl(d))

Списки в Си

struct Node {
    int value;
    Node * tail;
};

Node * nil = NULL;

Node * cons(int value, Node * tail) {
    return new Node { value, tail };
}

Что посмотреть в транспорте

Серьёзные материалы