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

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

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

181

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

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

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

3. На нулевом скобочном уровне ни запятая, ни | не встречаются.

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

цией по построению выражения.

В константу либо переменную ни скобки, ни запятая, ни

| не входят.

Значит, базис индукции состоит из импликаций с ложной посылкой и

тривиально верен.

Если выражение E является функциональным, то запятые, входя-

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

и E

i+1

, либо входят в

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

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

первом внутри E

, а значит, не менее чем на втором внутри самого E.

Символ | обязан входить в одно из E

и, таким образом, ни на нулевом,

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

Если выражение E является применением бинарной операции, то

оно имеет вид (E

⊕ E

). В нем, применяя предположение индукции,

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

тогда они были бы вынуждены входить на нулевом уровне в E

либо в

. А то, что их нет и на нулевом уровне, видно непосредственно.

Если E получается применением унарной операции, т. е. имеет вид

E

, то все сводится к рассмотрению E

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

леммы выполнены по предположению индукции.

И, наконец, если E — кванторное выражение, то рассмотрение про-

водится аналогично пункту для функционального.

Теперь заметим, что любое выражение, более сложное, чем после-

довательность унарных операций, примененная к константе либо пере-

менной, содержит скобки.

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

Пусть выражение построено применением бинарной операции (A⊕

B). Тогда оно не может представляться ни как функциональное, ни как

применение унарной операции, ни как переменная либо константа, по-

скольку начинается со скобки. Остается исключить лишь случай приме-

нения квантора, что производится при помощи леммы о разделителях.

Кванторное выражение содержит | на первом скобочном уровне, а дру-

гие содержать его на этом уровне не могут.

182

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

Значит, оно может представляться лишь в виде (C ? D), где ? — би-

нарная операция. Если C совпадает с A, то это — то же самое предста-

вление. Если же оно не совпадает с A, то оно может быть либо началом

A, либо включать в себя начало B. Если это начало A либо C содер-

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

и формулой не является. Таким образом, оба этих случая исключаются.

Значит, остается случай рассмотреть начало, не содержащее скобок и

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

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

чай, когда

C содержит начало B, поскольку “по дороге” оно прихватит

и бинарную операцию. Если эта последовательность не заканчивается

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

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

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

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

ки бинарных операций и не совпадающим с самим A. Следовательно,

A заканчивается функциональным выражением, поскольку лишь функ-

циональное выражение начинается с переменной либо константы. Но

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

ной либо константой следует открывающая скобка, а за C должна сле-

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

смотрение бинарных операций закончено.

Случаи унарных операций, функциональных выражений и кванто-

ров рассматриваются проще. Большую роль играет здесь лемма о разде-

лителях, исключающая все нежелательные разбиения функциональных

и кванторных выражений.

Конец доказательства теоремы.

Анализ доказательства позволяет сделать вывод, что обозначения

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

друга

В работах по логике часто встречается другое, специализированное

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

Сделаем еще одно ехидное и важное замечание о приложениях математики. На прак-

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

поскольку она просто не может быть в точности выполнена в реальном мире. Поэто-

му анализ доказательства необходим гораздо чаще, чем этого хотелось бы нам. Лишь

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

области, где она была доказана.

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

183

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

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

Сигнатурой

называется тройка непересекающих-

ся множеств

(P, C, F)

, где:

• P

—непустое множество

предикатных символов

.Каждому преди-

катному символу (сокращенно

предикату

)

P ∈ P

сопоставляется

его

арность a(P )

— натуральное число, указывающее количество

его аргументов.

• C

— множество (возможно, пустое)

констант

• F

—множество (возможно,пустое)

функциональных символов

,или

функций

. Каждой функции

f ∈ F

также сопоставляется ее арность

a(f)

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

специализацией

и опусканием фиксированных частей (например,опре-

делений логических связок и кванторов).

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

которого в информатике к настоящему времени наросло немало теоре-

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

форме заставляет писать много скобок. На практике порою пишут все

скобки подряд

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

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

того, чтобы допустить двусмысленность.

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

дующим соглашениям.

1. Внешние скобки в формуле могут быть опущены.

2. ⇒ применяется после & и ∨.

3. Если подряд идет несколько одинаковых связок

& либо ∨, то скоб-

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

Специализация — фиксация конкретных значений неизменных в данном контексте

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

менных и проведение после этого упрощений.

Особенно “отличился” в данном отношении язык ЛИСП. Там программисты уже

просто запоминают, сколько скобок (например, пять) нужно ставить в начале и в конце

того или иного стандартного выражения.

184

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

Таким образом, в первую очередь формула либо подформула в скобках

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

& и ∨ не фиксируется; здесь скобки необходимо использовать. Следо-

вательно, формула

A & B ⇒ C ∨ D

читается “Из A и B следует C или D”, и наши сокращения согласуются

также с грамматикой русского языка. Еще одно часто используемое со-

кращение — связка ⇔.(A ⇔ B) определяется как (A ⇒ B) & (B ⇒ A)

и читается “

эквивалентны”. Связка ⇔ связывает так же слабо,

как ⇒.

Итак, на данном примере мы видим,что некоторые бинарные опера-

ции считаются ‘сильнее’ других, но это отношение не является полным

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

ждая из них требует скобок при сочетании с другой; далее, порою скоб-

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

и той же операции, скажем, A & B & C & D является сокращением

и для ((A & B) & (C & D)), и для (((A & B) & C) & D), и для других

подобных выражений. Но,конечно же, никому не придет

в голову опус-

кать скобки при сочетании нескольких ⇒, поскольку эта операция не-

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

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

ций.

Здесь язык логики раскрывает еще одну ловушку, в которую легко

угодить. Так и подмывает сейчас заявить, что скобки могут опускаться

в последовательности любых ассоциативных операций. Но рассмотрим

пример операции эквивалентности ⇔. Она в классической логике ассо-

циативна; в самом деле, постройте таблицу истинности для

((A ⇔ B) ⇔ C) ⇔ (A ⇔ (B ⇔ C)) .

Но практически любой, увидев запись A ⇔ B ⇔ C, подумает, что она

выражает равенство значений всех трех формул A, B, C. А формула,

скажем, (A ⇔ B) ⇔ C истинна не во всех таких случаях и не толь-

ко в таких, как можно убедиться, рассмотрев ее таблицу истинности.

(Пупышев В. В.):

— А мне придет!

(Автор):

— Тогда сам виноват!

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

185

Итак, математики понимают под A ⇔ B ⇔ C нечто совсем другое, а

именно: (A ⇔ B) & (B ⇔ C). Бог им судья, но предусматривать такие

несистематические “сокращения” мы просто не можем.

Итак, проанализировав практическое использование опускания ско-

бок, мы приходим к любопытной структуре на бинарных операциях,

промежуточной между строгим и нестрогим частичным порядком. Ее

можно назвать частично нестрогим порядком. Это — транзитивное от-

ношение, антирефлексивность которого опущена.

186

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

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

(Формулы)

a) Если

P ∈ P

—

-арный предикат,

, . . . , t

— термы, то

P (t

, . . . , t

)

— элементарная формула.

b) Если

— формулы, то

(A & B)

(A ∨ B)

(A ⇒ B)

¬A

— формулы.

c) Если

— формула,

— переменная,то

∀xA

∃xA

— формулы.

Формула, входящая в другую формулу, называется ее подформулой.

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

Практическая работа

Обучение работе с программой “Мир Тарского”. Нахождение синтакси-

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

Абеляра, Аккермана, Аристотеля, Буля, Бернайса,Бозо, де Моргана,До-

джсона, Джона Рассела, Лестрейда, Людвига, Пирса, Уайтхеда, Шейн-

финкеля, Шерлока, условные).

Упражнения к § 7.2

7.2.1. Студент Чудаков использовал при формализации этнографиче-

ского материала следующие предикаты:

удмурт

(),

отец

(),

жена

(, ),

брат

(),

вотяк

(),

жрец

(, ),

побратим

(, ).

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

7.2.2. Правильно ли сокращены формулы:

∀xA(x) & B(x) ∨ C(x) ⇒ D(x),

∀x∃y (A(x) ⇒ B(x, f(y)) ⇒ C(y, g(x)))?

7.2.3. Что имел в виду студент, написавший:

∀x (A(x)) : B(x)?

7.2.4. Покажите, что опустив скобки вокруг кванторных выражений,

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

7.3. ПОДСТАНОВКА

187

7.2.5. Покажите, что после опускания скобок кванторные выражения

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

одного ограничения

7.2.6. Покажите,что ни одно типизированное выражение не может быть

началом другого

§ 7.3. СВОБОДНЫЕ И СВЯЗАННЫЕ ПЕРЕМЕННЫЕ.

ПОДСТАНОВКА

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

ваются квантором. В формуле A(x) вместо x может быть подставлено

конкретное значение, чего нельзя сделать в ∀x A(x). Более того, одна и

та же переменная может быть свободна для подстановок в некоторых

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

Поэтому статус приписывается не самой по себе переменной, а ее кон-

кретному вхождению в выражение (т. е. тексту выражения, в котором

выделен один из экземпляров переменной). В свою очередь, если она

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

ствовавшее на данный экземпляр переменной.Все эти тонкости отража-

ются следующим определением.

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

(Свободные и связанные вхождения)

1. Вхождение переменной в переменную (т. е. в саму себя) свободно.

2. Если переменная

входит свободно (связанно) в

либо



—

бинарный оператор, то соответствующее ее вхождение в

(A  B)

также свободно (связано соответствующим квантором).

3. Если переменная

отлична от

— квантор, то ее вхождение в

hKx A

, . . . , A

(x), . . . , B

(x)i

имеет тот же статус, что и ее вхождение в

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

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

λ-исчислении.

Здесь есть скрытая ловушка в выражениях,начинающихся с унарных операций.Най-

дите ее. Ее не обойти без привлечения иерархии типов.

188

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

4. Если

была связана в

, то она остается связанной тем же

вхождением квантора в

hKx A

, . . . , A

(x), . . . , B

(x)i.

5. Если

была свободна в

(x)

,то она становится связанной самым

внешним вхождением квантора в

hKx A

, . . . , A

(x), . . . , B

(x)i.

6. Если

была свободна в

(x)

, то она остается свободной и в

hKx A

, . . . , A

(x), . . . , B

(x)i.

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

(Замкнутые выражения) Переменная

называет-

ся

свободной

в выражении

, если у нее есть хотя бы одно свободное

вхождение в

. Выражение

A замкнуто

(является

постоянным

), если

у нее нет свободных переменных.

Только замкнутые выражения могут иметь при интерпретации точно

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

менных.

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

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

бодных переменных. Ее определение требует аккуратности, поскольку

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

ременные, входящие в выражение, подставляемое вместо переменной,

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

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

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

зии.

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

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

рования, произведения и интегрирования. Например, при попытке пря-

мой замены переменной y на x + y в

xy dx

В случае формул говорят предложением.

7.3. ПОДСТАНОВКА

189

получаем неверный результат

x (x + y) dx

(должно быть

z (x + y) dz ).

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

Подстановка терма

вместо свободных вхождений

переменной

в выражение

Subst(E, x, t)

i) Если

есть константа

, то

Subst(c, x, t) = c

ii) Если

есть переменная

y 6= x

, то

Subst(y, x, t) = y

iii) Если

есть переменная

, то

Subst(x, x, t) = t

iv) Если

есть выражение

F (t

, . . . , t

)

, то

Subst (F (t

, . . . , t

) , x, t) = F (Subst (t

, x, t) , . . . , Subst (t

, x, t)) .

v) Если

есть

(B  C)

, где



— бинарная связка, то

Subst(E, x, t) = (Subst(B, x, t)  Subst(C, x, t)) .

vi) Если

есть

⊕B

, где

⊕

— унарная связка, то

Subst(E, x, t) = ⊕Subst(B, x, t).

vii) Если

есть

hKy | D

, . . . , D

| E

, . . . , E

то рассматриваются следующие подслучаи:

190

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

x 6= y

не входит свободно в

. Тогда

Subst (hKy | D

, . . . , D

| E

, . . . , E

i, x, t) =

hKy | Subst (D

, x, t) , . . . , Subst (D

, x, t) |

Subst (E

, x, t) , . . . , Subst (E

, x, t)i

x = y

Subst (hKx | D

, . . . , D

| E

, . . . , E

i, x, t) =

hKx | D

, . . . , D

| E

, . . . , E

x 6= y

входит свободно в

(случай коллизии), то

Subst (hKx | D

, . . . , D

| E

, . . . , E

i, x, t) =

hKz | Subst (D

, x, t) , . . . , Subst (D

, x, t) |

Subst (Subst (E

, y, z) , x, t) , . . . , Subst (Subst (E

, y, z) x, t)i

где

— переменная, отличная от

и не входящая в

Данное определение корректно, поскольку каждый раз мы ссылаем-

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

в пункте 7 и дважды). Оно не уточняет конкретного выбора переменной

z в том же пункте, но это необязательно, поскольку связанная перемен-

ная должна пробежать весь универс. Более того, эта недоговоренность

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

конгруэнтности выражений, отличающихся лишь заменой связанных

переменных

(обозначается A

∼

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

(Конгруэнтность)

∼

b) Если

∼



— бинарная связка, то

(A  C)

∼

(B  D)

c) Ecли

∼

, то

⊕A

∼

⊕B

d) Ecли

∼

то

hKx | A

, . . . , A

| E

, . . . , E

∼

hKx | B

, . . . , B

| D

, . . . , D

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