На фото грустный Арсений, потому что он предпочёл сделать интерпретатор “вовремя”, а не расписать билет

Сегодня мы отправимся в Африку и побольше узнаем о том, чем занимаются любители [верблюдов](<https://www.youtube.com/shorts/fd6yI2HwS0k>)

• Микро предисловие

Трассы

ДелательТрасс3000: https://github.com/toadharvard/Lambada/

ДелательТрасс3001: https://capra.cs.cornell.edu/lambdalab/

ДелательТрасс3002: https://github.com/kinokotakenoko9/fp-practice

Понятие исчисления. Аксиомы, правила вывода, посылки и заключения. Доказательства

<aside> 💀 Понятие исчисления(не лямбда). Аксиомы и правила вывода

Допустим у нас есть какой-то язык(не важно какого порядка) $L$ и с помощью него можно записать, некоторые выражения $P_i$ и $C$. Выражение $C$ можно вывести при помощи определенного количества $P_i$ или вообще без их использования, тогда это будет называться аксиомой.

Количество $P_i$ необходимых для вывода $C$ + 1 определяет “место” правила. Таким образом, $(n + 1)$-местные правила вывода имеют формулу

$$ \displaystyle \dfrac {P_1\ ... \ P_n} C\ название $$

Название позволяет как-то именовать правило(спасибо кэп)

Всё это выражение, описанное выше, называется правилом вывода

Таким образом, исчисление состоит из:

• Непустого множества аксиом
• Множества правил вывода </aside>

<aside> 💀 Посылки и заключения

В выражении, описанном выше, то, что поверх черты называется посылками, а то что снизу заключением

$P_i$ – посылки (premises) $C$ – заключение (conclusion)

Это можно интерпретировать, как “Если всё то, что выше черты, то можно вывести то, что ниже черты”

</aside>

<aside> 💀 Доказательство

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

Можно провести аналогию, как следуя из аксиом в математике, можно доказать любую теорему

• Легче понять на примере из слайдов Какаду.

Из примера выше можно также представить правило вывода, как дерево:

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

Естественно, листья и узлы могут повторяться в пределах дерева

• Ремарочка про доказательство и аксиомы </aside>

‡ Определение языка лямбда-выражений. Три правила (α, β, η) преобразования лямбда-выражений

<aside> 💀 Язык лямбда-выражений

Переменные

Для определения языка лямбда выражений необходимо определить язык переменных $\nu$. Обычно используются два варианта

• Непустая последовательность букв, например: $[a-z]^+$
• Безымянные представления

Но в сущности язык переменных может представлять из себя чё угодно, это не суть важно, главное чтоб был

Алфавит

Когда мы определили язык переменных мы можем построить алфавит для $\Lambda$. Он будет представлять из себя следующий набор $\left\{),\ (,\ .,\ \lambda\right\}\cup \nu$

Слова(они же лямбда выражения или лямбда термы)

Определив алфавит, мы можем составить слова на языке $\Lambda$. Они имеют следующий вид

$$ \langle expr \rangle := \langle varname \rangle\ |\ \langle \lambda \langle varname \rangle.\langle expr \rangle \rangle \ |\ \langle expr \rangle \langle expr \rangle $$

где $\langle varname \rangle \in \nu$

Таким образом, слова делятся на три группы:

• Вхождение переменной
• $\lambda$-абстракция
• Применение

Из этих слов можно строить предложения, то есть какие-то осмысленные(ну или не очень) конструкции с кучей вот таких вот выражений

• Парочка аналогий с программирование

Немного про запись или так называемый синтаксический сахар

В язык входят скобки, но они часто опускаются из-за чего в этом пиздеце ещё сложнее разобраться

$$ E_1E_2E_3 \equiv (E_1E_2)E_3 $$

Выражения, в которых только лишь переименованы переменные и их вхождения называют синонимами(они $\alpha$-эквивалентны, об этом далее)

$$ (\lambda x.x) \equiv (\lambda y.y) \equiv (\lambda z.z) $$

Подстановка(об этом поподробнее тоже далее) может записываться разными способами

$$ [A/x]B = B[x \rarr A] = [x \rarr A]B = B[x := A] $$

Формально это означает подставить $A$ вместо всех вхождений $x$ в тело $B$. То есть слева от слеша в скобках, что подставить, справа от слеша в скобках вместо чего подставить и за скобками куда подставить. Наглядный пример

$$ (\lambda x.x)y = [y/x]x = y $$

</aside>

<aside> 💀 Три правила (α, β, η) преобразования лямбда-выражений

Все лямбда выражения можно разбить на $\alpha\beta\gamma$ классы эквивалентности соответственно

• $\alpha$-эквивалентность — два $\lambda$-выражения $\alpha$-эквивалентны, если можно переименовать связные вхождения так, что получатся синтаксически одинаковые выражения.
• При фиксированной стратегии два $\lambda$-выражения $\beta$-эквивалентны, если они редуцируются к одной и той же нормальной форме.
• Можно свободно заменять $f$ на $(\lambda x.fx)$ и наоборот
• Пояснения </aside>

Редексы. Стратегии вычисления лямбда-термов: CBN, CBV, CBNeeded, NO, AO. Достоинства и недостатки

<aside> 💀 Свободные и связные вхождения

Да, этого нет в билете, но нужным будет понять механику

Формально про свободные:

• Имя $n$ свободно в $\lambda$-выражении $n$.
• Имя $n$ свободно в $(\lambda x.E)$, если имя $n \not = x$ и $n$ свободно в $E$.
• Имя $n$ свободно в $\lambda$-выражении $(MN)$, если либо оно свободно в $M$, либо оно свободно в $N$
• Пояснения

На слайде есть одна штука, я если честно её вообще не понял мб кто-то умный объяснит

N.B. В одном λ-выражении одно и то же имя может входить и свободно, и связанно

• N.B.
• Некорректный пример подстановки </aside>

<aside> 💀 Редексы и стратегии

Редекс – это подвыражение (подтерм) вида $((\lambda x.e1)e2)$. Ну то есть залупа, которую можно вычислить($\beta$-редуцировать, упростить). По сути, применение к $\lambda$ -абстракции

Стратегия вычисления - способ, по которому мы выбираем какие редексы и в каком порядке будем упрощать (вычислять, β-редуцировать).

То есть у нас есть предложение, в нем куча этих вот редексов, их можно вычислять в разном порядке. Например, сначала средуцировать, всё что внутри или идти снаружи внутрь. Подробнее об этом далее

Будем $\beta$-редукцию обозначать следующим образом $e \longmapsto _{\beta} e'$. Редукция $e$ в $e'$

Каноничные определения:

• Редекс находится левее, если его λ в записи левее.
• Редекс самый левый внешний (leftmost outermost), если он самый левый и не содержится ни в каком другом редексе.
• Редекс самый левый внутренний (leftmost innermost), если он самый левый и не содержит ни какого другого редекса.
• ПоясненияОт </aside>

<aside> 💀 Классификация стратегий

</aside>

<aside> 💀 Call By Name(aka weak head normal form, aka CBN)

</aside>