Непейвода Н.Н. Прикладная логика

Подождите немного. Документ загружается.

7.1. СИНТАКСИС ЛОГИЧЕСКОГО ЯЗЫКА

171

кой, Семен Фурман явно сформулировал следующий технологический

прием

, который мы будем называть обобщение без потерь.

Пиши процедуру в частном, хорошо продуманном случае,

и тщательно, но без лишней оптимизации, а затем обобщай

ее на столь общий случай, насколько возможно без потери

эффективности.

Скажем, появление функционального анализа и топологии позволи-

ло обобщить без потерь множество частных теорем Коши в несколь-

ко общих утверждений. Появление теории категорий позволило превра-

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

использовать его,в частности,в теории абстрактных типов данных, при-

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

выше.

Мы проведем такую операцию обобщения для языка классической

логики, с тем чтобы, в частности, не говорить расплывчатые слова “ана-

логично” при переходе к построенным по такому же принципу языкам

неклассических логик. При обобщении мы выделим следующие черты

логического языка:

• Более сложные конструкции образуются из более простых четырь-

мя способами:

– Применение одноместной (унарной) операции к выражению.

Эта операция ставится перед выражением.

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

ставится между выражениями, и получившееся выражение

заключается в скобки.

– Применение квантора, который включает подкванторное вы-

ражение и переменную, по которой он навешен. Этот пункт

мы немедленно обобщим, чтобы включить и выражения ви-

да

n+m

i=1

(i + a)

либо {x ∈ X | A(x)}.

Формулировка была дана в личной беседе с автором; нам неизвестно, опубликовал

ли он что-либо по данному поводу.

172

ГЛАВА 7. ВВЕДЕНИЕ В СИНТАКСИС

Рассмотрим обобщенные кванторы следующей формы:

hKx | E

, . . . , E

| A

, . . . , A

где h i обозначают некоторую пару скобок.

Выражения

, . . . , E

называются ограничениями подкван-

торной переменной, а A

, . . . , A

— подкванторными выра-

жениями. Содержательно область действия подкванторной

переменной распространяется лишь на подкванторные вы-

ражения, ограничения остаются вне ее

– Функциональные записи вида F (E

, . . . , E

) .

• Выражения строго разделяются по типам (скажем, термы обозна-

чают предметы,формулы — высказывания).Каждая операция при-

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

определено,какого типа выражение получается после ее примене-

ния.

• Исходные понятия не фиксированы; заданы лишь способы обра-

зования более сложных из исходных.

Сразу заметим, что пункт, касающийся строгого разделения по ти-

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

вания. Скажем, операция

+ применяется и к целым, и к действитель-

ным, и к комплексным числам различной точности. Такая перегрузка

Именно разница между ограничениями и подкванторными выражениями приводит

к встречающимся в математическом анализе выражениям вида

f(x) dx.

В данной формуле верхнее x — свободная переменная, предел интегрирования, неиз-

вестное нам, но фиксированное значение. В

f(x) x имело бы тот же смысл, если бы

оно не попало в контекст, ограничиваемый квантором

dx. Вот это вхождение x (под-

кванторная переменная)в первую очередь влияет на понимание всех других возможных

вхождений

x в квантифицируемое выражение, именно оно заставляет x в f (x) пробе-

гать все значения в интервале

0 6 x

6 x

верхнее

, и оно же делает эти две переменные

абсолютно не имеющими друг к другу никакого отношения, кроме случайного (?) со-

впадения обозначений.

7.1. СИНТАКСИС ЛОГИЧЕСКОГО ЯЗЫКА

173

операций вызвала к жизни целую теорию разрешения возникающих не-

однозначностей, да и мы, грешные, воспользуемся перегрузкой в не-

скольких местах, явно ее оговорив.

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

ется перегрузка, но иногда она просто стучится в двери, если имеется

полное совпадение необходимых нам свойств операций над различны-

ми данными. Разница между использованием перегрузки в логике ли-

бо алгебре и в искусственном интеллекте либо программировании со-

стоит в том, что “теоретики” точно обосновывают сохранение необхо-

димых свойств, а “практики” все время нарываются на неприятности,

либо просто не дав себе труда уяснить и проверить эти свойства, либо

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

математическим сущностям, а к их неточным реализациям.

Другая особенность языка логики, принципиально отличающая его

от имеющихся языков программирования и искусственного интеллек-

та, да и от языка, скажем, математического анализа, — отсутствие фик-

сированного базиса понятий. Если в “конкретных” языках нижний уро-

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

нужные нам построения, то в математической логике есть построения и

преобразования, которые можно “опустить” на любой подходящий нам

фундамент и, соответственно, сразу получить целый город.

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

логики можно охарактеризовать как строго типизированный язык без

нижнего уровня с функциональными, унарными и бинарными операци-

ями и кванторами.

Прежде всего, поскольку выражения у нас делятся на типы, нужно

определить необходимые нам конструкции над типами. Эти конструк-

ции были введены польскими логиками в 20-х годах под названием син-

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

стве современных работ по теории алгоритмических и других формаль-

ных языков, по философии и математической лингвистике.

Пусть задано некоторое множество исходных типов

Определение 7.1.1. (Иерархия функциональных типов)

Множество

типов

задается следующим индуктивным определением:

a) Исходные типы

τ ∈ T

— типы.

b) Если

, . . . , τ

, τ

— типы, то

(τ

, . . . , τ

→ τ )

— тоже тип.

c) Других типов в

нет.

174

ГЛАВА 7. ВВЕДЕНИЕ В СИНТАКСИС

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

сигнатуры рассматриваемого конкретного приложения (в случае логи-

ческого языка — конкретной теории). Дадим наиболее общее понятие

сигнатуры,базирующейся на иерархии типов T.Для этого сначала опре-

делим, какие типы из иерархии для каких целей подходят.

Определение 7.1.2.

(Классификация типов)

a) Тип

(τ

, . . . , τ

→ τ )

называется типом функции,если все

, τ

—

исходные типы.

b) Тип

(τ

, . . . , τ

→ τ )

называется типом функционала, если

со-

держит

→

c) Тип

(τ

, . . . , τ

→ τ )

называется высшим типом,если в нем боль-

ше одной

→

d) Тип

(τ

→ τ )

называется типом унарной операции.

e) Тип

(τ

, τ

→ τ )

называется типом бинарной операции.

f) Тип

(χ, τ

, . . . , τ

, (χ → π

), . . . , (χ → π

) → τ )

, где

l > 0

, назы-

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

Как и следовало ожидать, здесь наиболее сложен пункт, касающий-

ся кванторов.Но вспомним уже известные нам кванторы. Разве, скажем,

∀x имеет дело с отдельными значениями A(x)? Как обычно расплывча-

то выражаются математики и философы

, квантор имеет дело “со всей

совокупностью значений выражения A(x)”. Всю эту совокупность зна-

чений лучше всего выражает функция, перерабатывающая каждое зна-

чение x в значение A(x). Соответственно, χ является здесь типом пе-

ременной x, каждое из π

— типом соответствующего подкванторного

выражения, зависящего от x. А вот типы ограничений берутся в “голом”

виде, поскольку ограничения не подпадают под область действия пере-

менной квантора.

Определение 7.1.3.

(Обобщенная) сигнатура

— множество символов

s ∈ σ

, каждому из которых сопоставлен один из признаков — констан-

та, унарная операция, бинарная операция, квантор, и задана функция

Да и мы прибегли к подобному выражению при описании кванторных конструкций

естественного языка.

7.1. СИНТАКСИС ЛОГИЧЕСКОГО ЯЗЫКА

175

сопоставляющая каждому

s ∈ σ

тип

τ ∈ T

таким образом, что опера-

циям сопоставляются типы операций соответствующей арности, кван-

торам — типы кванторов.

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

зуют переменные. Чаще всего переменные бывают лишь по объектам

исходных типов, да и то не по всем; если же у нас есть переменные и

кванторы по типам, содержащим →, то говорят, что определяемый язык

высшего порядка. Переменные по различным типам не пересекаются.

Для единообразия переменные типа

τ обозначаются x

, y

, z

и т. д.

Cчитается, что переменных каждого типа потенциально бесконечный

запас. Как обычно, если у нас всего один тип, по которому разрешено

иметь переменные, тип переменных опускается. Подмножество типов,

по которым имеются переменные, обозначается T

Заметим одну тонкость в данном определении. Функциональные сим-

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

быть и константы высших типов, они применяются в языке так же, как

функциональные символы, но по крайней мере один из их аргументов

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

несколько примеров.

Пример 7.1.1.

В теории групп исходные типы данных

—объекты,

—

истинностные значения. Сигнатура состоит из логических связок, логи-

ческих кванторов, бинарных операций

◦

и унарной

Inv

, константы

Их типы следующие.

χ(e) = o χ(=) = (o, o → t)

χ(◦) = (o, o → o) χ(Inv) = (o → o)

χ(⇒) = (t, t → t) χ(&) = (t, t → t)

χ(∨) = (t, t → t) χ(¬) = (t → t)

χ(∀) = (o, (o → t) → t) χ(∃) = (o, (o → t) → t)

Переменные имеются лишь по типу

Предикат

стандартно интерпретируется как равенство, константа

как единица группы,

a ◦b

как умножение,

Inv a

как обратный элемент

Пример 7.1.2.

Можно несколько видоизменить сигнатуру из предыду-

щего примера, добавив к

еще две константы:

Mult

Inv

и удалив опе-

рации

◦

Inv

. Тип

Mult

есть

(o, o → o)

. Этот пример показывает воз-

можность перехода между одноместными и двуместными функциями и

операциями.

176

ГЛАВА 7. ВВЕДЕНИЕ В СИНТАКСИС

Пример 7.1.3.

Фрагменты математического анализа можно описывать в

языке со следующей сигнатурой:

Имеется три исходных типа:

,интерпретируемые, соответствен-

но, как действительные числа, целые числа и логические значения.

Логические связки остаются теми же самыми.

Для работы с действительными и целыми числами имеются следую-

щие бинарные операции:

+, −, ∙, /, ⊕, , ×, ÷, =

, >

, =

, >

и унарные

exp

sin

cos

real

round

Кроме того, зададим следующие константы:

e, π, 0, 1, 0, 1

Кванторы данной сигнатуры следующие:

∀

∃

. Типы

всех перечисленных выше операций, констант и кванторов следующие:

χ(e) = χ(π) = χ(1) = χ(0) = r χ(0) = χ(1) = i

χ(+) = χ(−) = (r, r → r) χ(⊕) = χ() = (i, i → i)

χ(∙) = χ(/) = (r, r → r) χ(×) = χ(÷) = (i, i → i)

χ(real) = (i → r) χ(round) = (r → i)

χ(∀

) = (r, (r → t) → t) χ(∃

) = (r, (r → t) → t)

χ(∀

) = (i, (i → t) → t) χ(∃

) = (i, (i → t) → t)

χ(

) = (r, r, r, (r → r) → r) χ(

) = (r, i, i, (i → r) → r)

χ(=

) = χ(>

) = (r, r → t) χ(=

) = χ(>

) = (i, i → t)

Здесь видно, что мы вынуждены вводить кванторы всеобщности и су-

ществования по отдельности для каждого типа объектов, по которым

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

ся типом переменной, следующей непосредственно за ним, перегрузка

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

числе и нами. Аналогично перегрузка напрашивается и для общеупо-

требительных предикатов типа

или

, и для операций типа

или

−

Но здесь ситуация намного сложнее, поскольку допущение перегрузки

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

Несколько иной тип перегрузки мог бы возникнуть при применении

квантора суммирования к выражениям типа i. Здесь подкванторная пе-

ременная в любом случае имеет тип i, и разрешение двусмысленности

зависит от типа подкванторного выражения. Это уже похуже, и на по-

добных примерах в теоретическом программировании выросла целая

теория.

Теперь можно определить язык над обобщенной сигнатурой

σ. Его

выражения строятся из констант и переменных как обобщенные термы,

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

7.1. СИНТАКСИС ЛОГИЧЕСКОГО ЯЗЫКА

177

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

сложных объектов через более простые. Синтаксис логического языка

был первым местом, где осознанно использовался этот класс определе-

ний, ныне занимающий центральное место в формальных языках (в том

числе в языках программирования и искусственного интеллекта).

Определение 7.1.4.

Выражения типизированного языка с кванторами.

a) Константа

сигнатуры

— выражение типа

χ(c)

b) Переменная типа

— выражение типа

c) Если

, . . . , E

— выражения типов

, ... ,

соответствен-

но,

— выражение типа

(τ

, . . . , τ

→ τ )

, то

E(E

, . . . , E

)

—

выражение типа

d) Если

— выражения типов



— бинарная опера-

ция сигнатуры

, такая, что

χ() = (τ

, τ

→ τ )

то

(A  B)

—

выражение типа

e) Если

— выражение типа



— унарная операция сигнатуры

, такая, что

χ() = (τ

→ τ )

то

A

— выражение типа

f) Если

— квантор сигнатуры

χ(K) = ($, τ

, . . . , τ

, ($ → π

), . . . , ($ → π

) → τ ) ,

— переменная типа

, ...,

,...,

— выражения ти-

пов

, ...,

, соответственно, то

hKx | D

, . . . , D

| E

, . . . , E

— выражение типа

Чтобы данное индуктивное определение было корректным, необхо-

димо доказать единственность анализа выражений, т. е. что каждое вы-

ражение представляется в одном и только в одном из перечисленных ви-

дов и что соответствующие операции и компоненты определяются одно-

значно. Здесь это достаточно тривиально, поскольку мы использовали

скобки во всех сомнительных случаях. Тем не менее доказательство од-

нозначности будет проведено в следующем параграфе как для того, что-

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

выявить некоторые неявные, но практически важные предположения.

178

ГЛАВА 7. ВВЕДЕНИЕ В СИНТАКСИС

Пример 7.1.4.

В языке теории групп имеются следующие выражения:

(Inv a ◦ Inv b) (7.1)

(оно имеет тип

h∀x | h∀y | ((Inv x ◦ Inv y) = Inv(y ◦ x))ii (7.2)

(оно имеет тип

). Как говорилось в части 1, в математической логике

выражения предметного типа называются термами, а выражения логи-

ческого типа — формулами. В стандартной теоретико-групповой и ло-

гической записи первое и второе выражения представляются как

−1

◦ b

−1

(7.3)

∀x∀y



−1

◦ y

−1

= (y ◦ x)

−1



(7.4)

соответственно.

Пример 7.1.5.

Рассмотрим теперь, как представляются в нашей форме

выражения языка математического анализа.



| round 1, round x



| 0, real i

| exp sin((1 + real 1) ◦ (π ◦ x

))





(7.5)



∀



0) ⇒



| 1, x

| 1/x



= ln x



(7.6)

или же в обычной форме представления

round x

i=1

exp sin 2πx dx, (7.7)

∀x





(x > 0) ⇒

1/x dx = ln x





. (7.8)

7.2. КОРРЕКТНОСТЬ СИНТАКСИЧЕСКИХ ОПРЕДЕЛЕНИЙ

179

Из данных примеров видно, к чему приводит строгое различение ти-

пов. Случайно взяв не ту константу 1, мы вынуждены явно преобразо-

вать ее к другому типу. Далее, показывается один из способов, как дей-

ствовать с величинами, не попавшими в сигнатуру. 2 было просто пред-

ставлено как

(1+1)

. Анализируя определения и рассматривая примеры,

можно сделать вывод, что мы не рассматриваем операции, кванторы и

функции с переменным числом аргументов. Это соответствует и согла-

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

число аргументов появляется, оно, как правило, влечет неприятности.

Далее, мы не разрешаем произвольным образом пополнять теорию но-

выми константами, что также находится, в частности, в соответствии

с традициями языков спецификаций и языка

Пролог

. Конечно же, для

расширения возможностей теорий и методов работы с ними мы обяза-

ны предусмотреть средства расширения теорий, но это — отдельная и

достаточно интересная тема, развившаяся в целую теорию в традицион-

ной логике и приближающаяся к такому состоянию в математической.А

чтобы квалифицированно применять теорию определений, мы обязаны

уметь хорошо различать, что же можно выразить исходными средства-

ми.

В искусственном интеллекте свободно вводятся подходящие сигна-

туры для конкретных классов задач или даже отдельных задач. Напри-

мер, для задачи, связанной с описанием родства, можно ввести преди-

каты

Отец

(a, b),

Родственник

(a, b). В таких формализациях константы

соответствуют собственным именам.

В современной лингвистике вынуждены вводить весьма сложные

типы данных для придания математического смысла таким, казалось

бы, элементарным понятиям, как местоимения.

Переходим к доказательству формальных теорем.

§ 7.2. КОРРЕКТНОСТЬ СИНТАКСИЧЕСКИХ ОПРЕДЕЛЕНИЙ

Предложение 7.2.1. Любое выражение типизированного языка одно-

значно представляется в виде, соответствующем пп. 1) – 6) определе-

ния 7.1.4.

Доказательство. Предложение опирается на следующие леммы о

счете скобок.

Лемма 7.2.2. В любом выражении число открывающих скобок равно

числу закрывающих.

180

ГЛАВА 7. ВВЕДЕНИЕ В СИНТАКСИС

Доказательство. Индукцией по построению.Переменные и константы

скобок вообще не содержат. Если выражение A имеет вид F (t

, . . . , t

то, поскольку по предположению индукции все t

сбалансированы по

скобкам, в нем также число открывающих равно числу закрывающих.

Точно так же для всех пунктов определения выражений.

Лемма 7.2.3. В любом начале выражения открывающих скобок не мень-

ше, чем закрывающих.

Доказательство. Индукцией по построению выражения.

Определим скобочный баланс слова как

число открывающих скобок

− число закрывающих.

Переменные и константы скобок вообще не содержат. Если t получен

как f(t

, . . . , t

), то любое его начало имеет одно из следующих пред-

ставлений. Оно либо есть ‘f ’, либо имеет вид ‘f(’, либо ‘f (Ξ, Ξ

’, ли-

бо ‘f(Ξ Ξ

,’, либо есть сам t. Здесь Ξ есть последовательность выра-

жений, разделенных запятыми, Ξ

есть начало выражения. По преды-

дущей лемме, в выражении открывающих скобок столько же, сколько

закрывающих. Значит, скобочный баланс Ξ есть 0. По предположению

индукции, скобочный баланс Ξ

> 0. Следовательно, скобочный баланс

начала больше 0, если оно не является f либо не совпадает с самим t.

Точно так же подводится скобочный баланс для выражений осталь-

ных форм,но здесь сбалансированы могут быть также префиксы, соста-

вленные из знаков унарных операций и заканчивающиеся переменной

либо константой.

Следствие.

Начало выражения, содержащее скобку и сбалансиро-

ванное по скобкам, совпадает с самим выражением.

Скобочным уровнем некоторого вхождения подвыражения в выра-

жение называется число пар скобок, в область действия которых оно

попадает. Таким образом, если выражение не имеет окружающих его

скобок, то его уровень — 0, если имеет одну — 1, и т. д.

Лемма 7.2.4. Лемма о разделителях на первом скобочном уровне.

1. Если на первом скобочном уровне встречается символ ‘,’,то выра-

жение является применением последовательности

унарных опе-

раций к функциональному либо к кванторному выражению.

Возможно, пустой.