1626435695-d1df5d2e6d953ce7ad4b4ccb5f4f4e30 (844296), страница 36
Текст из файла (страница 36)
Ратледж [х36) упростил доказательство разрешимости проблемы эквивалентности, моделируя простые схемы е) Янова конечными автоматамв. Наиболее известно переналожение теории схем Янова, вмполненное Ершовым [хб[. В этой работе лвнеиное представление схем, идущее от операторного метода Ляпунова, заменено графовой формой схем, что поаволнло упростить и сделать более наглядной систему эквивалентных преобразованвй. 3 а д э в в е 7.7. Покэжвте, что система преобрээоээвкй, содериащая мрээвлэ, порождаемые схемами правил ЛТ1, ЛТ2, ЛТЗ, Ф1 в Ф2, представляет лобок колкую систему преобрээоээвкй для фуккцвовэльиой экэвээлевтвостк схем Якова.
Уяаэаяиг. Проследите ээ процессом преобрээоээвия, с помощью которого решается ээдэвве 7.6, к учтите те упращеиля, которые можно ввести э этот процесс е севов с тем, что всходкые схемы являются схемэмв Якове. Работа Ершова дала импульс новым исследованиям схем Янова, особенно научению различных обобщений этих схем. Система преобразований схем Янова содержит схемы правил двух ввдов: локальные (для применении которых к данному фрагменту достаточно иметь информацвю о некоторой его заранее фиксированной окрестности) и нелокалъные (для применения которых необходима информация о «почти всейэ схеме в целом). Например, схемы правил ЛТ7 (см.
гл. 6) и Ф2 (см. задание 7.6) являются локэльнымн, а, скажем, ЛТх, ЛТ2 (см. гл. 6) и ПЗ у Ершова [хб) иелокалъны. Янов [79) исследовал вопрос о том, можно ли вамекить нелокалъвые схемы правил конечным числом локальных правил. Он установил, что в общем случае этого сделать нелъая, и нашел положительное решение задачи для класса Яэ простых схем Янова.
удовлетворяющих следующим трем условиям: (1) условия схем из ߄— это проиэволъные выражения. ааписанные с использованием логических операций ~, /~, ~/ над элементарными условиями из множества (рт (х), ..., рэ (л)); (2) все преобразователи схемы достижимы, т. е. выполняются хотя бы при одной интерпретации; (3) схема вмеет уянверсальвыв сдвиг (з нашем варианте определения схем Янова все схемы имеют универсальный сдвиг). Сабельфелъд [62) нашел общий критерий локалъкоств системы эквивалентных преобразований схем Янова. Иткнв [2[) и Каплан [110) докааалн разрешимость проблемы эквивалентности для схем Янова с повторными вхождениями одного и того же преобразователя.
Иткин построил также полную систему прсоб° ) Схема Явоээ кээыэеется простой, если в вей эсэ оперэторы првсээвеэвкл рээлвевы, т. е. схема ве содержат двух эхождеккй едкого ° того же фувщвовэльвогосвмэолэ (вменил простые схемы ршсметрлээлвсь Яновым). 165 раэований для этого случая. Тузов [72, 73) исследовал схемы Янова с перестановочнымн преобразователями. В этом случае вместе с простой схемой Янова задается конечное число соотношений вида Иу — 61, где 1п 1~ — функциональные символы. Тем самым ограничиваются воаможности интерпретации функциональных символов.
При определении отношения эквивалентности схем (с использованием понятия свободной интерпретации) считается„ что термы-результаты равны с точностью до заданных соотношений перестановочности. Например, терм 1з1,1з[гт равен терну ~,Цз1 х, если задана система соотношений Щ =— 1з1,, 1т1з ав = — 1зЯ. Тузов установил разрешимость такого обобщенного отношення эквивалентности схем Янова. Аналогичный результат был получен Летичевскнм как частный случай полугрушювой эквивалентности [33[. Непомншций [461 установил раарешнмость проблемы эквивалентности схем Янова с системами соотношений, заданных полугруппами с определеннымн ограничениями. Зти системы включают соотношения перестановочности.
Подловченко [54, 55[ ввела и исследовала недетерминировавные схемы Янова (В-схемы). В этих схемах вершины-распознаватели заменены вершинами-фильтрами. Фильтр представляет собой логическое выражение, однако между распознавателем и вершиной-фильтром имеется различие, состоящее в следующем: а) из вершины-фильтра выходит не ровно две дуги, как в схемах Янова, а произвольное конечное число дуг; б) при выполнении интерпретированной Я-схемы после вычисленвя авачения предиката в фильтре возможен переход по любой иэ дуг, выходящих иэ фильтра„если зто значение равно т, а в противном случае вычисления обрываютсн и текущее состояние памяти объявляется результатом.
Подловченко показала, что для любой схемы Янова можно построить эквивалентную недетермнкированную схему„продемонстрировала разрешимость проблемы эквивалентности и построила полную систему эквивалентных преобразований. Как уже говорилось, включение в базис схем Янова едвисз венной переменной можно трактовать как исключение нэ схемы информации о структуре памяти: каждый оператор присваивания изменяет состояние всей памяти, значение каждого предвката вычисляется для состояния всей памяти. Таким образом, каждый преобразователь автоматически влияет на все последующие распознаватели. Чтобы сделать такое влияние более избирательнымз Янов ввел понятие сдеизя, которое на уровне схем программ моделирует структуру памяти реальных программ.
Каждому преобразователю сопоставлен набор предикатных свмволов, называемый сдвигом этого оператора. Сдвиг накладывает огранвчення на класс возможных интерпретаций, а именно — если предикатный символ р не входит в сдвиг некоторого оператора х:= 1(х), то при любой интерпретации Е должно иметь место равенство 1 (р (1(т))) = Е(р (г)). Иткнн расширил [23) класс схем Янова, обобщив понятие сдвига таким образом, что сдвиг может содержать 466 яе только предикатные, но и фуякциоиалъные символы. Тем самым обобщенный сдвиг позволяет моделировать информационные связи между операторами схемы. В классе обобщенных схем Янова Иткин ввел отношение так нааываемой комбинированной эквивалентности, более сальное, чем функциональная эквивалентность, но допускающее, тем не менее, выполнение как яновских эквивалентных преобразований, так и преобрааовавий, сохраняющих логико-термальную эквивалентность.
Показано, что комбинированная эквивалентность разрешима для обобщенных простых схем Янова. Гарланд и Лакхэм [[02), а также Летичевсквй [35) доказали, что проблема функциональной эквивалентности остается разрешимой для класса схем Янова с засылками констант, т. е. когда разрешены операторы присваивания х:= а, а Е= у, я (а) = О. Тот же самый аффект получается в результате добавления к базису схем Янова специальной переменной, используемой только для органиэации вспомогательных пересылок и в условных операторах [[40). Для практики программирования главный интерес представляют не отрицательные результаты о нераэрешимостн таких проблем, как эквивалентность, тотальность, пустота или свобода, а положнтелъные результаты, связанные с выделением классов схем, в которых такие проблемы разрешимы. Они исполъзуются в оптимвэацни программ, при доказателъстве правилъвости и построении инструментальных систем преобразования программ.
Патерсон [[26, $27, И9[, доказав совместно с Лакхэмом и Парком неразрешимость проблемы фуякционалъвой эквввалевтности стандартных схем, предпринял одновременно попытку выделить разрешимые подклассы. Определив понятие свободной схемы, он высказал гипотезу о раэрешвмости проблемы эквивалентности в классе свободных схем, однако эта гипотеза не подтверждена до сих пор, хотя и поддерживается многими исследователями. Сама же проблема свободы неразрешима(см. гл. 5, зЗ), н ие для всякой стандартной схемы существует эквивалентная свободная схема. Патерсон выделил класс либеральных схем. Стандартная схема 8 называется либеральной, если для любой свободной ивтерпретацвв У любые термы-зкачевия, вырабатываемые правыми частями операторов присваивания (не пересылок) в протоколе программы (8, 1), не равны, т.
е. някакон терм не может фигурировать дважды в протоколе как значенне, присваиваемое (не пересылкой) переменным иа памяти схемы. Отметим здесь, что в силу доказанного Непомнящим и Сабелъфельдом [50) результата для каждой стандартной схемы существует эквивалентная (в довольно сильном смысле, более сильном даже, чем логико-термалъная эквиваленткость) схема беа пересылок. В отличие от проблемы свободы проблема либеральности оказалась разрешимой.
установлена следующая связь между свободой и либеральностью: всякую либеральную схему можно пре- образовать в эквивалентную свободную схему, но не наоборот. Поскольку проблема либералъностя оказалась «проще» проблемы свободы, а либералъные схемы преобразуются в эквивалентные свободные, проблема эквивалентности в классе либеральных схем приобретает особый интерес: если она окажется неразрешимой, то автоматически устанавливается неразрешимость проблемы эквивалентности и в классе свободных схем. Пока обе этн проблемы открыты. В классе либеральных схем Патерсок выделил два интересных подкласса — ирззрессивнмз и консеряпвкзяме схемы.
В любой цепочке прогрессивной схемы переменная, являющаяся резулътатом оператора присваивания, всегда исполъауется в качестве аргумента в следующем операторе цепочки, если только он есть. Проблема эквивалентности оказывается разрешимой в классе прогрессивных схем.
Сложнее обстоит дело с другим подклассом. Назовем оператор присваивавня невырожденным, если его переменная-результат встречается среди аргументов, например х:= 1 (х, у, з). Схема называется воясервативиой, если все встречающиеся в ней операторы присваивания являются невырожденными. Патерсон только обратил внимание на класс консервативных схем, но не исследовал его, и проблемы пустоты и эквивалентности остаются открытыми для этого класса.
Интересно, что большинство предложенных разными авторами подклассов стандартных схем с разрешимой функциональной зквивалентностъю оказались или подклассами класса консервативных схем, нли близкими к нему. В начале атой главы отмечалось, что разрешимым является класс ~ с базисом Я = ((хп х»), Ц), (р), (л»:= ~(х), л»:= : = ) (х»), стоп (хп т»), р (л»), р (л»))).
Характерным для этого класса является то, что все функциональные и предикатные символы одиоместны (такие схемы называют упаря»ъви, или яокадичесяими) и переменные х, и х разделены (независимы) в том смысле, что при любой свободной интерпретации символ х, не входит ни в один терм-значение переменной х«, а х«не входит ни в один терманачение переменной х,. Более общий класс схем У„, обладающих этими двумя свойствами, нааывается классом моиадичесяих слав с и иезазисимм.ви яч«йками и имеет следующий базис: Ж„= = ((хп..., х„), Ц~ ', ...), (р~~»~, ...), (х;:= 1~ (т;) ~ » ( 1 ~ и, ! ) О) ( ) (р> (х«) ~ т ~( « ~ и, у ~ О) Ц (стоп (х,..., х„))). Легко убедиться, что класс У„является подклассом консервативных схем для любого к ) О. В работе [1»9) показано, что унарные схемы с в независимыми ячейками можно моделировать я-ленточными автоматамн таким образом, что схема пуста (тоталъна) тогда и толъко тогда, когда пуст (тотален) моделируввций автомат, и две схемы эквивалентны тогда и только тогда, когда эквивалентны моделирующие их автоматы.
Отсюда сразу следует решение проблем пустоты и тотальности в этом классе схем— они разрешимы, так как разрешимы проблемы пустоты и тоталь- «63 ности для многоленточвых автоматов (см. гл. 3, $2). В гл. 3 было докааано, что проблема эквивалентности двухленточных автоматов разрешима (этот результат получен Бердан [851 два года спустя после публикации работы И[91), но она остается открытой для автоматов с тремя и более лентами. Следователъно, проблема эквивалентности разрешима в классе д'«унарних схем е двумя независимыми ячейками, но ждет решения для унарних схем е тремя и бблъшим количеством независимых ячеек.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
