Здесь мы разберём

  • элементы математической логики, связывающие её с языками программирования;

  • ключевой аспект логического программирования — автоматизация вывода искомого результата (конструктивного доказательства);

  • базовые принципы языка Пролог;

  • связь теории типов с математической логикой;

  • связь механизмов «неявности» в разных языках с логическим программированием.

Оглавление обзора

  1. Выбор стиля

  2. Теория

Содержание

Математическая логика

Решая задачи материального мира, мы моделируем предметную область — формализуем сущности и их взаимоотношения. Такая формализация есть не что иное, как математическое описание нового языка со своим алфавитом, синтаксисом и даже своеобразной «морфологией» — правилами изменения и согласования выражений, не нарушающими семантику. Разные языки задают собственные системы мышления с разными понятиями корректности суждений, доказательств, алгоритмов.

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

Синтаксис

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

Стандартом описания грамматики искусственных языков является форма Бекуса-Наура (БНФ). Она позволяет формулировать грамматические конструкции, из которых строятся абстрактные синтаксические деревья (АСТ). В качестве листьев этих деревьев выступают атомарные терминальные выражения (терминалы), а узлами — индуктивно определённые составные нетерминальные выражения.

Совокупность терминалов определяет лексику языка, в рамках которой они называются лексемами или токенами. Лексическая грамматика описывает структуру лексем и определяет алфавит, поэтому она обычно предваряет описание синтаксической грамматики. В разных языках применяется разный подход описания лексики, но в последнее время она часто совмещается с грамматикой в формате расширенной БНФ.

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

(* Правила лексической грамматики: лексемы-терминалы *)
ZERO = "z" ;
SUCC = "s" ;
LBR  = "(" ;
RBR  = ")" ;

(* Правила синтаксической грамматики: нетерминальные выражения *)
Nat  = ZERO | ( SUCC , LBR , Nat , RBR) ;

Согласно последней строчке, число «три» на этом языке выглядит как s(s(s(z))).

А так формулируется синтаксис нетипизированного λ-исчисления:

(* Лексемы*)
LETTER   = 'a'..'z' | 'A'..'Z' ;
DIGIT    = '0'..'9' ;
ID       = LETTER , { LETTER | DIGIT } ;
LAMBDA   = 'λ';
DOT      = '.' ;
LBR      = "(" ;
RBR      = ")" ;

(* Синтаксические правила *)
expr = variable
     | abstraction
     | application ;

variable    = ID ;
abstraction = LAMBDA , ID , DOT , TERM ;
application = TERM , LBR , TERM , RBR;

Каждое выражение здесь является либо переменной вроде x, либо λ-абстракцией наподобие λx.x, либо применением x(y).

Нотация Бекуса-Наура используется для описания самых разных языков:

  • языки описания данных: XML, JSON, YAML…

  • онтологические или философские языки: OWL, Ложбан…

  • математические языки: формальные логики, λ-исчисление и теория типов со всеми расширениями и т.п.

  • языки программирования: Scala, Prolog, Go, Python, SQL, XQuery…

  • и, конечно же, сама БНФ.

Одна только проверка синтаксиса позволяет отсечь синтаксически некорректные описания модели. Но алгоритмы можно проверить не только на синтаксис.

Семантика выводимости

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

Правила вывода принято формулировать в виде дробей: запись \frac{A}{B} означает, что если у нас есть A, то мы можем получить B. Например, математическая индукция для введённых выше натуральных чисел описывается таким правилом:

\frac{P(z), \quad \forall k \, (P(k) \to P(s(k)))}{\forall n \, P(n)}.

Буквально, если утверждение P истинно для z и из истинности P(k) для любого k следует истинность P(s(k)), то это утверждение истинно для всех натуральных чисел.

Такие же дроби используются и в исчислении секвенций где ключевое значение имеет понятие выводимости одних формул из других. Запись \Gamma \vdash \Delta говорит о том, что из списка формул (контекста) \Gamma выводятся формулы \Delta. Такие утверждения называются секвенциями и более формально их можно описать в БНФ так:

<секвенция> = <список_формул> "⊢" <список_формул>
<список_формул> = <формула> | <формула> "," <список_формул> | ""

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

\frac{\Gamma \vdash \Delta ,\mathbf{A}\quad \mathbf{A},\Theta \vdash \Lambda }{\Gamma ,\Theta \vdash \Delta ,\Lambda }.

Данное правило коррелирует с сутью термина «секвенция» — под записью \Gamma \vdash \Delta может скрываться целая последовательность промежуточных выводов.

Если в числителе нет ни одной секвенции, то такое правило определяет аксиому — безусловное утверждение, вроде тавтологии \frac{}{A \vdash A}. Наличие аксиом необходимо для самой возможности завершения алгоритмов вычисления (доказательства), хотя и не гарантирует этого. Такие алгоритмы строят дерево вычислений (многоэтажную дробь) как бы «снизу вверх» — от набора предпосылок внизу к «пустой» секвенции вверху. Без аксиом говорить о подобных алгоритмах вообще не имеет смысла.

Классическую логику определяют правила вывода, задающие поведение логических связок (конъюнкции \land и дизъюнкции \lor), отрицанию \neg, кванторам всеобщности \forall и существования \exists. Например, вот так выглядит «введение отрицания справа»:

\cfrac {A,\Gamma \vdash \Delta }{\Gamma \vdash \Delta, \lnot A}.

Оно утверждает, что если из списка исходных формул «исключить A», то итоговый набор формул должен пополниться отрицанием \neg A. Если \Gamma выбрать пустым, а \Delta = A, то в числителе получим A \vdash A, и комбинируя это правило с упомянутой выше аксиомой тождества, получим

\frac{}{\vdash A, \neg A}.

Это одна из форм записи закона исключения третьего — без всяких предварительных условий истинно либо A, либо его отрицание.

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

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

Программирование же прагматично, и требует языков, в правилах вывода которых нет выводимых альтернатив: в знаменателе правее «турникета» \vdash допускается лишь единственная формула. Такие разновидности исчислений и основанные на них математические дисциплины называются интуиционистскими или конструктивными. В них нет закона исключения третьего, аксиомы выбора и тому подобных неконкретных рассуждений, а доказательством истинности является предоставление объективного свидетельства.

Рассуждения

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

Одним из важных аспектов процедур рассуждений является направление.

  • Синтетический подход начинает с известных аксиом и строит дроби вывода сверху вниз. Обычно таким способом разворачивается дерево новых, синтезированных знаний. Но в Прологе этот алгоритм адаптирован для вычисления свидетельств противоречивости полного набора формул, собранного из начальных условий и отрицания проверяемой гипотезы.

  • Аналитический подход, наоборот, стартует с искомой секвенции и ищет правила вывода, которые проведут снизу вверх до пустой формулы в числителе. Успешный подъём говорит о корректности искомой формулы в контексте заданных условий. Такой подход используется компиляторами при поиске неявных значений и преобразований.

  • Двунаправленный подход сочетает в себе оба предыдущих и применяется при выводе типов в современных языках программирования (ЯП), где классического Хиндли-Милнера уже недостаточно.

Ещё один важный момент — стратегия обхода списка секвенций.

  • Прямой поиск в ширину на каждом шаге подбирает подходящие правила для каждой секвенции, и лишь затем (лениво) переходит к следующему шагу. В процессе потребляется большой объём памяти, но если доказательство существует, то оно гарантированно будет найдено.

  • С другой стороны, поиск в глубину «жадно» разворачивает каждую секвенцию до конца и лишь затем переходит к следующей. Поиск в глубину потребляет меньше ресурсов и обычно работает быстрее. Однако, «жадность» иногда может приводить к зацикливанию, и тогда правильное решение не будет обнаружено, даже если оно лежало по соседству. Поэтому большую роль тут играет порядок перечисления формул в секвенциях.

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

Алгоритм унификации может быть очень простым, но тогда он оказывается не слишком удобным. Жизнь программистам упрощают алгоритмы семантической унификации и их обобщения. Они умеют учитывать, например, алгебраические законы (коммутативность, ассоциативность и т.п.), что важно при работе и с числовыми выражениями, и с типовыми. Кроме того, при унификации могут применяться проверки на зацикливание (прежде всего при выводе типов). Они не гарантируют полную защиту, но на практике оказываются очень полезными.

Программирование

Пролог

Главным флагманом парадигмы логического программирования ещё с 1970-х годов является язык Пролог (PROgramming in LOGic). Его создатели смогли перенести исчисление секвенций из академических исследований напрямую в синтаксис программного кода. Пролог даёт возможность описывать собственные теории, чтобы компьютер помогал проверять любые гипотезы в них.

Синтаксис Пролога опирается всего на три (!!) синтаксические конструкции: факт (базовая аксиома), правило (логическая импликация) и запрос. Эти конструкции представляют собой разновидности хорновских дизъюнктов — утверждениям конструктивной логики, но с гораздо более строгими ограничениями, упрощающими алгоритм рассуждений.

Давайте опишем простейшую теорию, чтобы решить показательную задачу — найти дедушку:

% Факты (Аксиомы)
отец(иван, петр).                        % P₁
отец(петр, анна).                        % P₂

% Правило, единственное для нашей задачи
дедушка(X, Y) :- отец(X, Z), отец(Z, Y). % R

% Запрос
?- дедушка(Who, анна).                   % Q

Факты в прологе объединяются в исходный список формул, из которого необходимо вывести утверждение запроса, которое в нашем случае формально можно записать так: Q=\exists W. дедушка(W, анна). Таким образом задача сводится к доказательству секвенции P_1, P_2 \vdash Q. Для этого используются встроенные правила конструктивной логики совместно с нашим

R\colon \quad \frac{\Gamma \vdash отец(X, Y) \quad \Gamma \vdash отец(Y, Z)}{\Gamma \vdash дедушка(X, Z)}.

В Прологе используется так называемая SLD-резолюция — доказательство от противного. Иными словами, интерпретатор языка пытается вывести, что отрицание нашей гипотезы в сочетании с предпосылками приводит к противоречию. Запрос в исходной секвенции переносится левее турникета как отрицание: P_1, P_2, \neg Q \vdash \bot, где символ \bot обозначает пустую формулу, а отрицание запроса в нашей задаче имеет вид \neg Q = \forall W. \neg дедушка(W,анна) — «никто не является дедушкой Анны».

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

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

Также имеется набор встроенных и стандартных библиотек, предоставляющих популярные структуры данных, инструменты работы с базами данных, сетью и многое другое. Всё это делает Пролог применимым для решения широкого спектра задач коммерческой разработки. Как правило, логическое программирование востребовано в действительно сложных предметных областях вроде машинного обучения, систематизации знаний, планирования. Поэтому сейчас поддерживаются и развиваются сразу несколько диалектов Пролога, ориентированных на различные интеграции, оптимизации и расширения языка: SWI-Prolog, Scryer Prolog, Ciao, XSB Prolog, SICStus Prolog и другие.

Изоморфизм Карри-Ховарда

Первым языком функционального программирования считается Лисп (1960 год), основанный на λ-исчислении (1932 год). Лисп с его скобочками программами-списками оказал огромное влияние на всю индустрию, но обнаруживать ошибки типизации в таких программах можно было, лишь наткнувшись на них в процессе выполнения. Дело в том, что в базовой версии λ-исчисления вообще нет понятия «тип» и каждое выражение является просто функцией, принимающей и возвращающей аналогичные функции.

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

Параллельно развитию инженерной практики программирования Хаскелл Карри ещё в 1930-х годах, занимаясь комбинаторной логикой (ещё одной интересной системой исчисления), вводит своё понятие типа — это предикат (утверждение), определённый на термах (выражениях, обозначающих вычисляемые сущности). В такой системе комбинаторы имеют типы функций α → β, а связанные с ними аксиомы в точности соответствуют аксиомам интуиционистской логики!

Более или менее законченную форму это соответствие обрело лишь в 1969 году благодаря работам Уильяма Ховарада, опубликованным лишь в 1980 году. Основные положения изоморфизма Карри-Ховарда сведены в следующую таблицу:

Интуиционистская логика

Теория типов

Высказывание T

Тип T

Доказательство высказывания T

Терм (значение) типа T

Утверждение T доказуемо

Тип T обитаем (могут быть получены значения)

Дизъюнкция A\lor B

Тип суммы A+B

Конъюнкция A\land B

Тип произведения A\times B

Импликация A\Rightarrow B

Экспоненциальный тип A \to B

Истинная формула

Тип-единица 1

Ложная формула

Нулевой тип 0

Отрицание \neg A

Экспоненциальный тип A \to 0

В 1970-х годах Жан-Ив Жирар и Джон Рейнольдс независимо разработали теорию параметрического полиморфизма, а Пер Мартин-Лёф заложил основы интуиционистской теории типов, зависимых от значений (и популяризировал обозначение a: T, чтобы дистанцироваться от теории множеств). Эти обобщения соответствуют логикам второго и более высоких порядков.

Академические исследования соединились с инженерной практикой в 1975 году, когда Робин Милнер разработал язык ML для системы автоматического доказательства теорем. В нём были реализованы параметрический полиморфизм и строгая статическая типизация (проверка типов). Синтаксис ML стал основой для целого семейства языков функционального программирования, таких как OCaml и F#. Но повлиял он и на многие другие языки благодаря самому важному нововведению — алгоритму вывода типов, разработанному Милнером на базе наработок Роджера Хиндли и получившему в дальнейшем имя обоих учёных.

Система типов в языке ML умеет логически выводить тип программы, даже если программист не указал его явно. Если это удаётся, то сама программа считается доказательством корректности типизации. Более того, реализованный там чистый алгоритм Хиндли-Милнера позволяет писать код вообще без указания типов! При этом код остаётся статическим типизированным, но типы приписываются термам неявно.

Но оказывается, что для рекурсии задача вывода типа не разрешима в общем случае. Поэтому программист зачастую обязан вручную указывать типы рекурсивных функций, а компилятору остаётся лишь проверить корректность таких аннотаций (type checking), используя алгоритм Хиндли-Милнера лишь как вспомогательный инструмент. Автоматическое доказательство корректной типизации становится двунаправленным.

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

Неявности

Давайте внимательнее посмотрим, как работают перегрузки методов. Имя у них одинаковое, но типы аргументов (и возвращаемого значения) разные. Каждое такое имя формирует свой контекст, в котором каждому набору типов аргументов сопоставляется реализация метода и тип результата. Когда компилятор встречает в коде вызов метода по имени, он смотрит в соответствующий контекст и самостоятельно выбирает, какой конкретно метод будет вызван.

С преобразованиями типов ситуация аналогичная. Когда компилятор понимает, что в контексте имени метода нет реализации с подходящими типами аргументов, он начинает искать (уже в другом контексте) способы преобразовать входящие термы к доступным типам. Формально, это аналогичный поиск терма типа A => B, даже если он оказывается тривиальным, как, например, при приведении типа от класса-наследника к базовому. Но обычно есть возможность определять и пользовательские операции приведения типов, которые добавляются в тот же контекст компилятора наравне с предустановленными. Найдя подходящее преобразование, компилятор неявно встраивает его в уже закодированную последовательность действий.

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

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

Существуют языки (Coq, Lean, Agda, Idris), в которых контекстные абстракции сочетаются с самыми мощными обобщениями теории типов, такими как исчисление конструкций. С такими инструментами можно реализовать логический вывод не просто наподобие того, что предлагает Пролог, но даже гораздо мощнее!

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

Промежуточный итог

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

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

Результаты работы такого автоматического вывода мы видели в предыдущей части обзора, а в продолжении будет рассказано, как именно автоматизировать этот вывод.