Лекция 2. Семантика и доказательство

Теория моделей

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

В лекции 1 мы сравнили формальные языки математики и логики с языками, используемыми для программирования компьютеров. Различие между ними в семантике. Языки программирования используются для управления компьютерами, тогда как языки математики и логики используются, чтобы делать утверждения. Утверждения являются объектами потенциального доказательства. Следовательно, и доказательство, и смысл утверждений играет роль в математике и логике, и поэтому мы определяем их как системы доказательств.

Начнем с очень простого языка, который будет немного более продвинутым, чем язык $L_3$из лекции 1. Это язык $L_4$ алгебры средней школы. БНФ для языка приведен ниже.

$$\begin{aligned} \langle sentence \rangle &:= \langle arithexpr \rangle \\ \langle arithexpr \rangle &:= (^\wedge \langle arithexpr \rangle \langle op \rangle \langle arithexpr \rangle^\wedge) | \langle variable \rangle | \langle number \rangle \\ \langle op \rangle &:= + | - | * | / \\ \langle variable \rangle &:= w | x | y | z | \langle variable \rangle^{\wedge '} \\ \langle number \rangle &:= \langle digit \rangle | \langle digit \rangle ^ \wedge \langle number \rangle \\ \langle digit \rangle &:= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 \end{aligned}$$

Примеры предложений $L_4$: $4 = (2 + z)$, $(3 * x) = (w - (y / 2))$и так далее. В отличие от $L_3$язык $L_4$включает переменные.

Мы можем разделить символы системы доказательств на константы и переменные. Константы языка -- это те символы, значение которых считается фиксированным и понятным. Таким образом, мы можем предположить, что знаем, что означают $+$, $-$, $\ast$, $/$. Мы также предполагаем, что знаем, что мы подразумеваем под «0», «1», «2» и т. д. Это означает, что, рассматривая утверждение, полностью состоящее из констант, мы можем сказать, истинно оно или ложно. Так

$$4 = (2 + 2)$$

истинно, а

$$5 = (2 + 2)$$

ложно. Тем не менее, если мы заменим константу на переменную, то получится открытое предложение, как иногда говорят в логике. Примеры: $4 = (2 + z)$и $5 = (x + y)$.

Открытые предложения не являются ни истинными, ни ложными. Но мы можем спросить, есть ли решения этих уравнений, которые делают их истинными. Таким образом, для $4 = (2 + z)$решение $z = 2$ делает уравнение истинным, а для $5 = (x + y)$решения $x = 4$и $y = 1$ делают уравнение истинным.

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

$$4 = (2 + red)$$

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

Когда интерпретация делает открытое предложение истинным, она называется моделью этого предложения. Когда интерпретация делает открытое предложение ложным, она называется контрмоделью. Если у предложения есть хотя бы одна модель, оно выполнимо.

Здесь следует рассмотреть два особых случая. Открытое предложение общезначимо только тогда, когда каждая интерпретация этого предложения является его моделью. Открытое предложение контрзначимо только тогда, когда каждая интерпретация этого предложения является его контрмоделью. Например, предложение $x + y = y + x$общезначимо в языке $L_4$, потому что какие бы значения для $x$и $y$ мы ни нашли, предложение после подстановки будет истинным. Предложение $x + 1 = x$ является контрзначимым, поскольку оно неверно для всех значений $x$.

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

Упражнение 2.1. Классифицируйте следующие открытые предложения из $L_4$ как общезначимые, контрзначимые или как ни те и ни другие.

1. $4 = x$
2. $x = (x - 1)$
3. $(x * (y + z)) = ((x * y) + (x * z))$
4. $(- (- x)) = x$
5. $(x + y) = x$

Теория доказательств

Альтернативой объяснению систем доказательств в терминах моделей и интерпретаций является изучение ряда правил и аксиом, которые устанавливают, как утверждения доказываются в этой системе. Традиционно такое объяснение не рассматривалось как часть семантики, хотя были споры о том, что объяснение доказательства утверждения является одним из способов объяснения значения этого утверждения. В начале 20-го века группа философов, называемых логическими позитивистами, восприняла эту точку зрения достаточно серьезно, чтобы отождествить значение утверждений естественного языка со средствами для их проверки.

Логический позитивизм в этой форме в наши дни не получил широкого признания, но в контексте систем доказательств этот тезис более правдоподобен. Можно утверждать, что, объяснив правила, по которым доказываются алгебраические утверждения, мы предоставили адекватное объяснение их значения.

Теория доказательств для системы доказательств определяет правила, по которым строятся доказательства в этой системе. Но что такое доказательство? Если мы посмотрим на доказательства в математике, мы обнаружим, что доказательство -- это не утверждение, а аргументированный монолог о взаимосвязи между выводом, который нужно доказать, и предположениями, необходимыми для его доказательства. То есть доказательство обычно начинается с чего-то вроде "Теорема: если что-то, то то-то и то-то", после чего следует доказательство.

Если мы серьезно рассмотрим эту модель, то фундаментальным объектом доказательства будет не утверждение, а пара, состоящая из списка предположений (что-то) и того, что нужно доказать (то-то и то-то). Этот объект мы назовем секвентом.

Первым, кто рассмотрел секвенты как объекты доказательства и изучил их формально, был Герхард Генцен.

Герхард Генцен (1909 - 1945)

Герхард Генцен родился в немецкой семье. Будучи молодым студентом, Герхард показал, что он одаренный математик, и учился у Германа Вейля. Он разработал исчисление секвентов во время Второй мировой войны. В это время Герхарда отправили в Прагу в качестве преподавателя математики. Когда Чехословакия была захвачена советскими войсками, Генцен был помещен в концлагерь. Его телосложение всегда было хрупким, и к тому же Герхард страдал от переутомления. Он умер от истощения в 1945 году.

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

В системе доказательств, основанной на секвентах, понятие доказуемости определяется с помощью ряда правил секвентов. Правило секвента имеет вид

Пусть $\Delta$-- список предположений, $p$-- заключение, $n > 0$; тогда секвент формы $\Delta, p$доказуем, если секвенты $S_0, ... S_n$доказуемы.

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

Секвент $\Delta, (X + Y) = (X + Z)$доказуем, если секвент $\Delta, Y = Z$доказуем.

Переменные $X$, $Y$и $Z$заменяют произвольные алгебраические выражения как, например, $1$или $(x - y)$. Эти переменные, которые исчисление секвентов использует для обозначения выражений обсуждаемого языка, называются метапеременными.

Обычно секвент записывается не как$\Delta, (X + Y) = (X + Z)$, а, что более верно, $\Delta >> (X + Y) = (X + Z)$ или $\Delta \vdash (X + Y) = (X + Z)$, где символы$\vdash$и $>>$читаются как "поэтому". Ограничения клавиатуры сделали символ $>>$популярным выбором во многих научных статьях, так что мы будем использовать эту нотацию.

Общепринятый способ записать предыдущее правило:

$$\dfrac{\Delta >> (Y = Z);}{\Delta >> (X + Y) = (X + Z);}$$

В этом правиле предположения $\Delta$остаются неизменными. В таком случае часто убирают $\Delta >>$и пишут просто

$$Правило \space A \newline \dfrac {Y = Z;} {(X + Y) = (X + Z);}$$

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

Мы столкнулись с досадным фактом о логике -- перегрузка одних и тех же слов для обозначения разных вещей в разных контекстах. Другие авторы используют слово "предпосылки" для обозначения используемых предположений ($\Delta$в нашем правиле) и "заключение" для обозначения сукцендента. Мы возьмем на себя возникшую двусмысленность и будем надеяться, что контекст устранит неоднозначность использования слов.

Логическая система может быть описана в терминах набора правил вывода для секвентов. Если бы каждое правило вывода требовало доказательства с помощью одной или нескольких предпосылок, то любое доказательство было бы невозможно. Поэтому должны существовать правила секвентов, которые категорически и безоговорочно утверждают, что секвент доказуем, не требуя доказательства чего-либо еще.

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

Например, в логике самое основное безусловное правило состоит в том, что мы можем доказать $P$, если $P$-- предпосылка.

$$Правило \space B \newline \dfrac {} {P, \Delta >> P;}$$

Обычно $\Delta$отбрасывается, и правило записывается чуть проще:

$$\dfrac {} {P >> P;}$$

Теперь добавим правило сложения:

$$Правило\space C \newline \dfrac {(X + Y) = Z;} {(Y + X) = Z;}$$

Эти три правила определяют ограниченную систему доказательств для алгебры; вот наше первое доказательство.

Нужно доказать: если $x = y$, тогда $(x + y) = (z + y)$.

Доказательство: нужно доказать, что $x = y >> (x + z) = (z + y)$. По правилу C это может быть доказано, если может быть доказано $x = y >> (z + x) = (z + y)$. Это может быть доказано по правилу A, если может быть доказано$x = y >> x = y$, и по правилу B это может быть доказано однозначно.

Доказательство очень простое, но оно показывает некоторые элементы, которые можно встретить в более сложных доказательствах. В частности, мы начали с цели доказательства и двигались в обратном направлении, пока не пришли к чему-то, что можно разрешить с помощью безусловного правила. Этот стиль доказательства популяризировал математик Дьёрдь Пойа в своей книге "How to Solve It". В информатике такой подход называется backward chaining, а противоположный подход -- то есть, начать с чего-то несомненного и двигаться к цели доказательства, называется forward chaining.

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

Продолжим и добавим дополнительное безусловное правило -- аксиоматическую схему.

$$Правило \space D \newline \dfrac {} {(X = X);}$$

Проведем новое доказательство с использованием правила D.

Нужно доказать: $(x + y) = (y + x)$.

Доказательство: Можем доказать $>> (x + y) = (y + x)$по правилу C, если можем доказать$(y + x) = (y + x)$. По правилу D это сразу же доказуемо, потому что $(y + x) = (y + x)$-- аксиома.

Когда утверждение может быть доказано без предпосылок, как в случае выше, оно называется теоремой системы. $(x + y) = (y + x)$-- это теорема нашей скромной алгебраической системы.

Непротиворечивость и полнота

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

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

Семантика языков программирования

В этой лекции мы говорили только о семантике систем доказательства, но системы доказательств -- это только один случай формальных языков. Языки программирования также являются формальными языками, и программы имеют смысл. Как же тогда описать смысл программы?

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

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

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

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

Пожалуй, наиболее близок к материалу этой лекции аксиоматический подход. Идея аксиоматического подхода состоит в том, чтобы отобразить программу $P$в формальное описание $d$того, что она делает, в некоторой системе доказательства $S$. Идея в том, что $d$точно отразит выполнение программы, и мы сможем предсказать, как $P$будет работать, просто путем дедукции из $d$. В этом смысле аксиоматический подход к семантике программ сводит задачу объяснения всех формальных языков к задаче объяснения систем доказательства. Мы увидим пример этого подхода в лекции 17.

Дальнейшее чтение

Хенкин (1967) представляет собой хорошее обсуждение формальных систем, а Диллер (1990) рассматривает аксиоматическую семантику под названием Z. Гордон (1988) описывает аксиоматический подход, основанный на логике Флойда-Хоара, а Шмидт (1986) охватывает денотационную семантику. Подход, основанный на операционной семантике для ограниченного языка программирования Kλ, описан в главе 21 книги Тарвера (2014). Даффи (1991) рассматривает различные подходы к логике, включая последовательное исчисление.