Введение в соответствие Карри—Говарда для кофейников

[arseniiv]

Некоторые хотели бы задавать вопросы об этой вещи, но не считают себя достаточно сведущими; попытаемся исправить это.

§1. RTL

Начнём с двух классических формальных систем и разовьём их дальше достаточно естественным образом. Первая — пожалуй, самое легковесное небесполезное логическое исчисление, positive implicational calculus. Это исчисление умеет «обрабатывать» лишь импликацию в высказываниях — всё не содержащее импликацию считается атомарными высказываниями, берущимися из некоторого множества $S$ (sentences). Язык $\mathcal L_\to$, с которым работает это исчисление, крайне прост и задаётся такими правилами образования (formation rules):

$$\frac{s\in S}{s\in\mathcal L_\to}\;S\textsf{-form}, \qquad\qquad \frac{s_1, s_2\in\mathcal L_\to}{s_1\to s_2\;\in\mathcal L_\to}\;{\to}\textsf{-form}.$$

Эти правила эквивалентны индуктивному определению $\mathcal L_\to$ как наименьшего множества, включающего каждый элемент $S$ и для каждых двух своих элементов $s_1,s_2$ также конструкцию вида $s_1\to s_2$.

(Что такое «конструкция»?)

От подобных конструкций требуется естественные вещи:
(1) Надо чтобы $s_1\to s_2$ не совпадало ни с какой конструкцией не вида $s_1\to s_2$ — в данном случае с $s\in S$.
(2) Совпадение $s_1\to s_2$ и $s'_1\to s'_2$ экстенсионально, то есть эквивалентно одновременному $s_1\equiv s'_1$ и $s_2\equiv s'_2$.
То есть между собой эти штуки работают как кортежи, но мы можем ввести много видов разных кортежей и будем записывать их человеческим образом, а не в виде, например, $(\textsf{constr-id}, a_1,\ldots, a_n)$.

Индуктивность определения означает, что для любого $s\in\mathcal L_\to$ мы можем установить, по какому правилу оно было построено и, более общо, что нам доступна структурная индукция:

Если
$[S\textsf{-form}]\colon$ для любого $s\in S$ выполнено $P(s)$;
$[{\to}\textsf{-form}]\colon$ для любых $s_1,s_2\in\mathcal L_\to$, для которых $P(s_1), P(s_2)$ верны, выполняется и $P(s_1\to s_2)$;
то $P$ выполняется на всём $\mathcal L_\to$.

(Например, индукция (не «полная») по натуральным числам — это структурная индукция по языку, задаваемого правилами $\dfrac{}{0},\quad\dfrac{n}{Sn}$. «Курицу или яйцо», однако, обсуждать тут не будем — это просто пример, и корректный пример; сведение не эквивалентно переопределению.)

Вернёмся к исчислению. Язык мы задали — кстати, его элементы будем звать формулами — и теперь зададим выводимость формул. Итак, правила вывода (inference rules):

$$\frac{a, b\in\mathcal L_\to}{\vdash a\to(b\to a)}\;\textsf{K}, \qquad \frac{a, b, c\in\mathcal L_\to}{\vdash (a\to(b\to c))\to((a\to b)\to(a\to c))}\;\textsf{S}, \qquad \frac{a,b\in\mathcal L_\to \quad \vdash a \quad \vdash a\to b}{\vdash b}\;\textsf{MP}.$$

Значок $\vdash$ читается «выводимо». MP — сокращение от Modus ponens, восходящего к названиям правил вывода средневековыми логиками. (Оно пережило все остальные.) Правила вывода может быть удобно переписать более компактно, выкинув очевидные предположения:

$$\frac{}{\vdash a\to(b\to a)}\;\textsf{K}, \qquad\qquad \frac{}{\vdash (a\to(b\to c))\to((a\to b)\to(a\to c))}\;\textsf{S}, \qquad\qquad \frac{\vdash a \quad \vdash a\to b}{\vdash b}\;\textsf{MP}.$$

Выводом формулы $x$ в этом исчислении мы будем называть получение $\vdash x$ путём применения этих правил. Выводы можно изображать в виде деревьев, но это быстро станет неудобным, и я даже не хочу набирать вывод формулы $a\to a$ (где $a$ — вообще любая формула: вывод структурно будет один и тот же — применение одинаковых правил в одинаковых местах), хотя он небольшой.

Потому давайте подумаем, что можно сделать, чтобы писать проще. Можно заметить, что выводы точно так же можно считать индуктивно конструируемыми из других выводов, как это было с определением формул: каждое правило вывода порождает «правило образования вывода» механически. Расширим нотацию и будем писать $\vdash i : x$ для «$x$ получается выводом $i$» или, лучше «вывод $i$ показывает $x$». И:

• Правило $\dfrac{}{\vdash a\to(b\to a)}\;\textsf{K}$ превращается в правило $\dfrac{}{\vdash\mathsf K : a\to(b\to a)}\;\textsf{K-form}$.

• Правило $\dfrac{}{\vdash (a\to(b\to c))\to((a\to b)\to(a\to c))}\;\textsf{S}$ даёт $\dfrac{}{\vdash\mathsf S : (a\to(b\to c))\to((a\to b)\to(a\to c))}\;\textsf{S-form}$.

• Наконец, правило $\dfrac{\vdash a \quad \vdash a\to b}{\vdash b}\;\textsf{MP}$ даёт более интересное $\dfrac{\vdash i : a \quad \vdash j : a\to b}{\vdash \mathsf{MP}(j, i) : b}\;\textsf{MP-form}$ — тут мы собираем два вывода в один.

Теперь я могу вам сказать, что вывод $a\to a$ — это $\mathsf{MP}(\mathsf{MP}(\mathsf S, \mathsf K), \mathsf K)$. Из $\vdash\mathsf K : a\to((b\to a)\to a)$ и $\vdash\mathsf S : (a\to((b\to a)\to a))\to((a\to(b\to a))\to(a\to a))$ мы получим $\vdash\mathsf{MP}(\mathsf S, \mathsf K) : (a\to(b\to a))\to(a\to a)$, после чего возьмём $\vdash\mathsf K : a\to(b\to a)$ и применив снова MP получим $\vdash\mathsf{MP}(\mathsf{MP}(\mathsf S, \mathsf K), \mathsf K) : a\to a$. Эзотерично (например, я сейчас получил этот вывод, восстанавливая формулы по запомненной схеме самого вывода, и какое-то особое смысловое наполнение в структуре самих формул или вывода искать не стоит), но полностью корректно. И заметьте, что если принять импликацию правоассоциирующей (то есть позволять писать $a\to b\to c$ вместо $a\to(b\to c)$), прозрачность формул из как минимум этого вывода упростится (дальше я постараюсь опускать все скобки в таких случаях, крепитесь).

Теперь мы можем коротко (ну, почти коротко — дальше мы это дело чуть улучшим) записывать выводы формул с импликацией. Тут можно было бы доказать, что мы можем вывести все такие формулы, которые истинны при любых значениях истинности атомарных высказываний из $S$, но это другая история.

§2. LTR

Не эта. Эта история будет о другом формализме, λ-исчислении. Возникло оно далеко не с нуля, но мы будем считать его одной из формализаций вычисления, и по желанию формализацией подстановки. Оно чуть сложнее, и потому хорошо, что я показал вам определения с правилами выше.

Язык $\mathcal L_\lambda$ определим опять же основываясь на некотором множестве атомов — переменных $V$:

$$\frac{v\in V}{v}\;V\textsf{-form}, \quad \frac{t \quad u}{tu}\;\textsf{app-form}, \quad \frac{v\in V \quad t}{\lambda v.t}\;\textsf{abs-form}$$

(напоминаю, части «$\in\mathcal L_\lambda$» выше опущены!).

Немного о семантике (в §1 семантику импликации вы наверняка уже знали заранее). Элементы этого языка, λ-термы, можно понимать как некоторые вычисляющие устройства, могущие принять что-то на вход и построить какой-то результат, вход и результат притом те же λ-термы. Терм $tu$ — это применение $t$ (функции) к $u$ (аргументу), а терм $\lambda v.t$ — это функция такая, что $(\lambda v.t)u$ — это результат замены в $t$ всех свободных вхождений $v$ на $u$, причём как раз выражения $\lambda t.v$ считаются связывающими $t$ в $v$. Если обозначить упомянутую выше замену как $t[u/v]$ (слэш при этом можно читать как «вместо»), можно определить её рекурсивно. Сначала определим свободные переменные терма $FV(t)$:
• $FV(v) = \{v\}$;
• $FV(tu) = FV(t)\cup FV(u)$;
• $FV(\lambda v.t) = FV(t)\setminus\{v\}$.

Теперь подстановка $t[s/w]$:
• $v[s/w]$ есть $s$, если $v\equiv w$, в противном же случае $v$;
• $(tu)[s/w]$ есть $t[s/w] u[s/w]$;
• если $v\equiv w$, $(\lambda v.t)[s/w]$ есть $\lambda v.t$.
• иначе, в случае $v\notin FV(s)$ имеем просто $(\lambda v.t)[s/w]\equiv\lambda v.(t[s/w])$;
• наконец, если $v\in FV(s)$, то $(\lambda v.t)[s/w] \equiv (\lambda v'.t[v'/v])[s/w]$, где $v'$ не встречается свободно нигде в $t, s, w, v$, «свежая», — это делается, чтобы не замкнуть свободные вхождения $v$ из $s$. Этого неприятного случая можно было бы избежать, отказавшись от связанных переменных, но в данном тексте альтернативный подход (приписывается де Брёйну) скорее всего будет менее понятным. Переименование связанной переменной $v$ в $v'$ носит ещё название α-конверсии.

Итак, неформально терм $(\lambda v.t) u$ «вычисляется» в $t[u/v]$. Формально это описывается правилами β-редукции:

$$\frac{}{(\lambda v.t)u\to u[t/v]}\;\textsf{redex-eval}, \quad \frac{t_1\to t'_1}{t_1t_2\to t'_1t_2}\;\textsf{app}_1\textsf{-eval}, \quad \frac{t_2\to t'_2}{t_1t_2\to t_1t'_2}\;\textsf{app}_2\textsf{-eval},$$

и стрелка $\to$ здесь означает отношение вычислимости за один шаг (а для рассмотрения вычислимости за произвольное число шагов можно использовать его рефлексивное транзитивное замыкание $\to^*$).

Можно заметить, что есть термы, которые можно вычислять бесконечно, например $\Omega\equiv(\lambda x.xx)(\lambda x.xx)$, для которого имеем $\Omega\to\Omega$ (за шаг!). Эти расходящиеся термы неизбежны, если мы хотим использовать это исчисление как тьюринг-полный вычислительный формализм, но можно поставить и другие цели. Например можно захотеть, чтобы любой терм без свободных переменных (замкнутый) мог интерпретироваться как функция из (и в) какого-то более узкого, чем всё $\mathcal L_\lambda$, множества.

(Да?)

Да. Например, мы можем выделить множество замкнутых термов, которые не редуцируются дальше — считать их чем-то вроде констант. Или расширить язык, включив туда настоящие константы типа $0, 1, 2,\ldots$ или $\mathsf{true, false}$.

Подобно конструкции $f\colon A\to B$ мы можем захотеть сопоставить «функциональному» терму тип: $t : \alpha\to\beta$, притом так, чтобы если $u : \alpha$, то $tu : \beta$, ну и кроме того чтобы вычисление не меняло типа: если $s : \alpha$ и $s\to^* s'$, то $s' : \alpha$. Это возможно.

Определим множество типов $T$ следующими правилами:

$$\frac{\alpha\in TV}{\alpha}\;TV\textsf{-form}, \quad \frac{\alpha \quad \beta}{\alpha\to\beta}\;{\to}\textsf{-form},$$

где $TV$ — некоторое множество переменных-типов. Так как мы не добавляем в язык никаких посторонних констант (см. спойлер чуть выше), без этих переменных не обойтись — надо с чего-то начинать построение.

Чтобы теперь сделать термы типируемыми, подействуем наиболее прямым способом: чуть изменим сам язык термов и будем указывать тип аргумента: $\lambda v:\alpha.t$. Кроме того нам понадобится типировать незамкнутые термы, а потому указывать приписанные переменным типы. Это можно делать слева от знака выводимости, например, $x : \alpha\vdash (\lambda v : \alpha.v)x : \alpha$, и в общем случае слева скопится какое-то множество $\Gamma$ таких утверждений о переменных; заодно давайте писать коротко $\Gamma, v:\alpha$ для $\Gamma\cup\{v:\alpha\}$, когда $v:\alpha\notin\Gamma$, и не писать $\varnothing$ слева от $\vdash$. Правила типирования очень похожи на правила образования термов:

$$\frac{v\in V\quad v:\alpha\in\Gamma}{\Gamma\vdash v:\alpha}\;V\textsf{-type}, \quad \frac{\Gamma\vdash t:\alpha\to\beta \quad \Gamma\vdash u:\alpha}{\Gamma\vdash tu:\beta}\;\textsf{app-type}, \quad \frac{v\in V \quad \Gamma, v:\alpha\vdash t:\beta}{\Gamma\vdash(\lambda v:\alpha.t):\alpha\to\beta}\;\textsf{abs-type},$$

а также надо будет чуть поправить правила $\textsf{abs-form}$ и $\textsf{redex-eval}$ (туда входит λ-абстракция, форму которой мы усложнили).

Надо заметить, что мы немного испортили язык: у нас теперь, например, для каждого $\alpha\in T$ есть свой отдельный терм $\lambda x:\alpha.x$ типа $\alpha\to\alpha$, когда в бестиповом исчислении был один. Это ничего, и даже бывает полезно. Зато можно убедиться (структурной индукцией, разумеется), что вычисление не портит тип. Кроме того можно видеть, что $\Omega$ не типируется: мы не можем найти никаких типов $\alpha$, даже для типирования его «половинки» $\lambda x.xx$. Без введения конструкции let (которую мы не будем здесь рассматривать) мы не сможем написать и типируемый комбинатор неподвижной точки (такой замкнутый $Y$, что $YF\to^* F(YF)$), это косвенный признак потери тьюринг-полноты. Ещё надо отметить, что если терм типируется, то единственным образом (по поводу этого и многого другого можно смотреть например [TaPL]).

[TaPL]: Benjamin C. Pierce. Types and programming languages.

Теперь если бы мы например добавили тип $\mathbb B$ со значениями $\mathsf{true, false}$ (два правила образования термов и два правила типирования) и по функции $\mathsf{if}_\alpha:\mathbb B\to\alpha\to\alpha\to\alpha$ для каждого $\alpha\in T$ (опять по правилу для того и сего), и дополнили бы правила редукции правилом вычисления выражений $\mathsf{if}\;b\;t\;u$, мы бы могли точно знать, что терм типа $\mathbb B\to\mathbb B$ реализует (здесь пока не частичную, при дальнейшем расширении не обязательно) функцию $\mathbb B\to\mathbb B$, и т. д..

§3. → ←

Надеюсь, вы к этому моменту покрутили пост туда-сюда и заметили сходство правил $\textsf{MP-form}$ и $\textsf{app-type}$ и сходство индуктивных определений $\mathcal L_{\to}$ и $T$? Вот. Вы переоткрыли соответствие Карри—Говарда в самой минимальной форме и наверняка даже видите, что удивляться (по крайней мере сейчас тут) особо нечему.

Назовём тип $\alpha\in T$ населённым, если мы можем показать какой-то замкнутый терм с таким типом, то есть $\vdash t:\alpha$. Теперь мы можем читать эту последнюю запись как «$t$ — доказательство населённости $\alpha$». Мы можем установить, что термы $K\equiv\lambda x.\lambda y.x$ и $S\equiv\lambda x.\lambda y.\lambda z.(xz)(yz)$ типизируемы и показывают соответственно аксиомы $\textsf{K-form}$ и $\textsf{S-form}$ выше. Показывают в том смысле, что если сформулировать логическое исчисление из §1 полностью аналогично λ-исчислению, эти две аксиомы станут не нужны (в отличие от правила MP и нового правила дедукции, соответствующего $\textsf{abs-type}$).

Такая теория называется натуральной дедукцией (тут мы получим её урезанный вариант, говорящий только об импликации), и в классическом представлении имеет в правилах вывода посылки не только в виде формул, но и в виде подвыводов из гипотез, где последние «заряжаются» специальными маркерами и «разряжаются» вместе с ними при использовании правила дедукции, и любой вывод зависит ото всех ещё не разряженных в нём гипотез. Контексты типирования в λ-исчислении — это как раз перечисление таких маркеров (имена переменных) и гипотез (их типы).

§4. ???

-- Ср июн 26, 2019 03:11:51 --

Да, тут ещё должно будет появиться описание того, чему соответствует вычисление в логическом формализме — мы его показали только в §2, а в §1 его аналога нет. Это позже.

-- Ср июн 26, 2019 03:19:45 --

Ещё будет показано это:

arseniiv в сообщении #1401556 писал(а):

Однако у этой парочки есть смысл в переписывании произвольного комбинатора, записанного как λ-терм, в запись из K и S без лямбд. И эта процедура соотносится с доказательством леммы о дедукции. Да, надо будет это тоже включить в ту тему.

[Munin]

В конце §2 опечатки в формулах.

[arseniiv]

Исправил, спасибо.

-- Ср июн 26, 2019 03:38:14 --

Да, ещё переименовал тему в «…соответствие…» вместо изоморфизма, мне как-то так больше нравится, но иногда пишу по привычке как раньше. «Изоморфизм» надо бы по-хорошему строить явно и точно, а настолько абстрагироваться я не готов (на все случаи, которые открыты!), и никому такого не надо. «Соответствие» же видится менее формальным.

[Munin]

arseniiv в сообщении #1401555 писал(а):

§1. RTL...
Вернёмся к исчислению. Язык мы задали — кстати, его элементы будем звать формулами — и теперь зададим выводимость формул. Итак, правила вывода (inference rules):

$$\frac{a, b\in\mathcal L_\to}{\vdash a\to(b\to a)}\;\textsf{K}, \qquad \frac{a, b, c\in\mathcal L_\to}{\vdash (a\to(b\to c))\to((a\to b)\to(a\to c))}\;\textsf{S}, \qquad \frac{a,b\in\mathcal L_\to \quad \vdash a \quad \vdash a\to b}{\vdash b}\;\textsf{MP}.$$

Тпру! Что такое выводимость? Чем $\vdash a$ отличается от $a\in\mathcal{L}_\to$?

[arseniiv]

О, ура, вопросы!

Выводимость — это пока что свойство элементов $\mathcal L_\to$ (определяемое индуктивно) и обозначаемое для какого-то $a\in\mathcal L_\to$ как $\vdash a$. Это как раз позволяет не маркировать правила, определяющие выводимость, как-то особенно по сравнению с правилами, определяющими состав $\mathcal L_\to$.

[buddy]

В помощь.

Соответствие Карри—Ховарда:
от математической логики к программированию и обратно
Записи лекций на XVII Летней школе «Современная математика»
В. Н. Брагилевский
Дубна, 19–30 июля 2017 года
https://www.mccme.ru/dubna/2017/notes/b ... -notes.pdf

[Munin]

arseniiv в сообщении #1405227 писал(а):

О, ура, вопросы!

Извините, что разочаровываю, но пока у меня щёлкает между режимами "всё понятно" и "ничего не понятно". Боюсь, особо творческих вопросов не будет.

[arseniiv]

Ну ещё ту длинную

Morten Heine Sørensen, Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism

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

[Nezaam]

arseniiv, будет-ли продолжение?

[arseniiv]

Будут вопросы и пожелания — будет продолжение, а так я не знаю чем продолжать и имею потому недостаточно желания. Потом, книжка, указанная постом выше, наверно сделает это всё лучше меня, просто она длинная (но зато она и берёт большую часть того, чего я не собирался здесь показывать, потому что целью было понятное введение в то, с чем это вообще едят).