XIX Белоусов А.И., Ткачев СБ. Дискретная математика (1081422), страница 110
Текст из файла (страница 110)
700 8. КОНТЕКСТНО- СВОБОДНЫЕ ЯЗЫКИ Построим, например, доказательство записанного выше выражения: а,Ь,с,й,е,д — аксиомы; — правило вывода (1); — (2); — (1); — (2); — (1) (е+ д) (дх(е+д)) (с+ (Ых (с+д))) (Ьх (с+(дх(е+д)))) (а+ (Ь* (с+ (Их (е+ д))))) Замечание 8.15. В этой связи полезно заметить, что и правила вывода формальной теории следует трактовать как просто „правила замены" (в полной аналогии с порождающими грамматиками), согласно которым разрешается от определенных цепочек (в левой части правила) переходить к новым цепочкам (в правой его части).
Тогда по правилам вывода можно получать из цепочек, не обязательно теорем или аксиом, какие-то другие цепочки, т.е. строить выводы, не являющиеся доказательствами. Это опять- таки аналогично грамматикам, в которых применение продукций, вообще говоря, не обязано быть выводом из аксиомы. Такал широкая и чисто синтаксическая трактовка правил вывода позволяет в теории формальных систем и в связанной с нею теории доказательств строить выводы из „гипотез"— цепочек, которые предполагаются доказанными. Если затем удается действительно доказать их, то построенное первоначально „относительное" доказательство превратится в „абсолютное" (т.е. начинающееся с аксиом). ф Нетрудно видеть, что мы определили тот же язык другим способом.
Множество доказуемых утверждений совпадает здесь с множеством всех утверждений, и, таким образом, семантика в данном случае совпала с синтаксисом: утверждение имеет смысл тогда и только тогда, когда может быть доказано, т.е. тогда и только тогда, когда является арифметическим выражением, порождаемым приведенной вьппе грамматикой.
Д.8.2. Самавтака формалалых ааыкоа Построив аксиоматическую семантику языка, мы можем на этой базе определить семантику уже экстенсионально, положив, что экстенсионал утверждения есть множество всех его доказательств (если утверждение не имеет доказательства, то его экстенсионал считается не определенным — формально мы включаем тогда в предметную область специальный „неопределенный элемент" с тем, как уже отмечалось, чтобы можно было вводимую семантическую функцию считать отображением). В заключение рассмотрим экстенсиональное определение семантики простейшего языка программирования, который будем называть МПАМ (М1пПАХр~аяе). Синтаксис языка определим посредством форм Бэкуса — Наура: (программа) зж (последовательность операторов) (последовательность операторов)::= (оператор) ~ (оператор) (последовательность операторов) (оператор) с= (присваивание) ~ (условный переход) ~ (цикл) (присваивание) с= (переменное):= (терм) (условный~переход) с= ау (условие) реп (последовательность операторов) еЬе (последовательность операторов) ~ а,( (условие) $Ьеп (последовательность операторов) (цикл) з= юЫе (условие) Ио (последовательность операторов) еЫ (переменное) з= х1~...
~х„ (терм) с= (функциональный символ) ((последовательность термов) ) ~ (переменное) ~ (константа) (последовательность термов):зм (терм) ~ (терм) (последовательность термов) (функциональный символ)::= ~~ ~... ~ ~„, (константа) с= с1 ~... ~ са (условие) з= (предикатный символ) ((последовательность термов) ) (предикатный символ)::= р1 ~...р 702 8. КОНТЕКСТНО-СВОБОДНЫЕ ЯЗЫКИ Заданная таким образом КС-грамматика определяет так называемый абстрактный синтаксис М1ЬАХа: мы игнорируем некоторые синтаксические детали, такие, как слова Ьед1п, ети1, обрамляющие последовательность операторов, а также то, что операторы разделяютсл точкой с запятой, что между термами в последовательности термов ставитсл запятая и т.п.
Мы также не уточняем структуру переменных (идентификаторов), констант, функциональных и предикатных символов, считая, что эти нетерминалы „пробегают" каждый свой алфавит. Чтобы формально описать экстенсионгльную семантику введенного посредством написанных выше синтаксических правил языка, нужно определить универсум. В зависимости от того, какой универсум рассматривается, в рамках экстенсионального подхода различают 1) денотпационную семантпику, 2) операциональную семантпику и 3) тпрансЯормационную семантпику (семантпику смешанных вычислений). Здесь мы рассмотрим только денотационную семантику. В денотационной семантике языка, подобного МПАХу, универсум определяется как множество преобразователей состояний памяти. К построению этого множества и переходим.
Определение 8.17. Состпо*ние памлтпи — это произвольное отпображение множества переменных 1 языка программирования в множество Р данных (значений). В силу сформулированного определения мы отождествляем память с множеством переменных (идентификаторов, „ячеек", имен) данного языка программирования (конкретно — языка М1ЬАХ), а состояние памяти о есть отображение вида о: 1-+Р, сопоставляющее каждой переменной значение, принадлежащее некоторому множеству значений (данных) Р.
Последнее можно рассматривать как объединение некоторого семейстпва множестве, служащих носитпеллми многосортпной алгебры данных Д.8.2. Сеыавтика форыатьвых языков 70З языка. Их можно отождествить с типами данных, используемыми в рассматриваемом языке: числами, массивами, строками, стуктурами и т.п. В множество Р включен также неопределенный элемент О (неопределенное значение). Множество всех состояний памяти обозначим Е. Определение 8.18.
Преобразователь состполний памяти — это произвольное отображение множества Е состояний памяти в себя. Множество всех преобразователей состояний памяти обозначим (Е -т Е). На множестве Е определяется структура индркотивного упорядоченного множвсптва (см. 1.8). Областпь определенностпи состояния памлти и— это множество, обозначаемое Р(п), всех переменных х, таких, что п(х) у~ О. Тогда положим для двух произвольных состояний и и р о ( р ео (Р(п) С Р(р))3с((Ух Е Р(тт))(тт(х) = р(х))). Очевидно, что отношение < есть отношение порядка. Далее, множество Е имеет по отношению < наименьший элемент, а именно такое состояние О, что (Чх Е 1)(О(х) = О). Его называют всюду неопределенным состоянием памяти; ясно, что Р(О) = И.
Кроме того, для любой неубывающей последовательности состояний памяти о1 ( пг ( ... ( и„< ... состояние пв, такое, что пв(х) =по(х) оьхеР(п„), есть тпочная верхняя грань этой последоватпельностпи, причем Р(пв) = 0 Р(пп) о>1 704 8. КОНТЕКСТНО-СВОБОДНЫЕ ЯЗЫКИ Таким образом, множество состяний памяти Е, снабженное отношением порядка <, является индуктивным упорядоченным множеством. С учетом результатов, полученных в 4.5 (см. теорему 4.11), отсюда следует, что и множество преобразователей состояний (Е -+ Е) есть индуктивное упорядоченное множество.
В этом множестве отношение порядка < определяется условием ~ < д ев (Чп е Е)(~(о) < д(о)), наименьшим элементом является стиираюиВий преобраэовагпель О, такой, что 0(п) = О для всякого о е Е, а точной верхней гранью неубывающей последовательности преобразователей состояний У~ ( (Ь ( (...У„< ... является преобразовв тель 1в, определяемый следующим образом: (Уа е Е)(Ух е 7)(ув(п)(х) = у„(о)(х) с~ х й 1У(уп(п))), причем 11(Ув( )) = 0Р(Ь.( )) п)1 Более того, оказывается, что композиция преобразователей состояний (как отпобраэсениб) непрерывна в смысле сохранения точных верхних граней (см.
1.8), точнее, для любой неубывающей последовательности преобразователей состояний и произвольного преобразователя состояний д дозирати = вир(д о уп), вир 1п о д = вир(уп о д). Докажем первое из этих равенств. Для произвольного о Е Е имеем д овир 1„(о) = виру„(д(сг)). 705 Д.8.3. Семавтяяа фораааьяых яэьиов Тогда для всякого х Е Ю(д о ~д,(п)) давпр~д(п)(х) = зпрУ„(д(п))(х) = У„(д(п))(х) = д о 1„(п)(х), т.е. поскольку, как можно показать, композиция монотонна в смысле определения, данного в 1.8, то 17(д И.( )) — Ц П(д'Ы(п) д о вар ~„= яир(д о Д„). Имея в виду все рассмотренные вьппе свойства множества (Е -+ Е), определим денотационную семантику языка МП АХ.
Семантическая функция есть отображение 1 1 множества фраз в множество (Е ~ Е) преобразователей состояний памяти. 1. Семантика оператора присваивания: ~п(д), д~х; 1а где через Ф~ обозначено значение терма $ в состоянии о., равное О, если котя бы для одного переменного, входящего в терм, его значение не определено, и равное значению терма при подстановке на место каждого его переменного х его значения п(х). Суть записанного вьппе семантического правила очень проста: оператору присваивания х:= Ф сопоставляется преобразователь состояний, меняющий состояние таким образом,что все переменные, кроме х, сохраняют свои значения, а новое значение переменного х есть значение правой части оператора присваивания (терма $) в состоянии о.
706 8. КОНТЕКСТНО-СВОБОДНЫЕ ЯЗЫКИ 2. Семантика оператора условного перехода: $21 р($1,...,Ц) 2йепЯ1 е1веЯ2Д(н) = Р1Д( ) Ф1," 2')=1. ДЯ2Д(Ю) р(Ф1,... 8~ ) =О, Это правило написано в предположении, что значения всех термов в состоянии и определены. В противном случае оператору условного перехода сопоставляется стирающий преобразователь О. Подобное же соглашение принимается и далее в аналогичных ситуациях. Семантика условного перехода без еЬе-альтернативы записывается аналогично, но при условии ложности предиката р в состоянии и берется тождественный преобразователь состояний 1Р. 3. Семантика цикла: ДшЬь|ер(11, ",8~,) НоЯепИД(о) = ДЯД 0ДшЫер($1,...,$„) йоЯепЦ(о), р($1~,...,8„~) = 1; 1Р(а), р(21",...,2„~) = о.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
