1626435695-d1df5d2e6d953ce7ad4b4ccb5f4f4e30 (844296), страница 29
Текст из файла (страница 29)
Чтобы достичь (С2), заменим предварнтельпо всякий вход с номером 7 в С~ на луч, состоящий нз всех пересылок к1.— — к, с лг Е= Вь а всякий выход эакенвм на луч, состоящий из всех пересылок к,:= л„я„~л Я, где Я вЂ” множество аргументов этого выхода.
Вто можно сделать повторным применением схемы правил ЛТ7. Если теперь некоторая переменная л встречается в обоих фрагментах пары, а новые переменные уы у не встречаются в Сл и С„, то применением ЛТ4 заменвм на у, в Сл и на ул в Сл все вхождения переменной к, кроме тех вхождений, которые относятся к компонентам свяавости, содержащим результаты входов или аргументы выходов.
В результате будет достигнуто условие согласованности (СЗ). Добьемся, наконец, выполнения условия согласованности (С4).Для этого применим сначала описанный выше алгоритм распознавания автокатной эквивалентности к л-графам фрагмевтоз Сл и Сл. Из С, Сл следует, что Сл и С, подобны, поэтому этот алгоритм успешно завершится и даст результирующий граф, а тем самым и разбиения Уь..., У„' и Ум..., Ув множеств вершин исходных л-графов на кепустые н непересекающиеся классы, Здесь и — число вершин в результирующем графе, а У< в $7 — множества всех тех вершин первого в второго л-графов соответственно, которые склеиваются в 3-ю вершину результирующего графа. Построим фрагмент шн)Ф(бк б )по вашим подобным фрагмевтак Сл в Сл.
В качестве вершин л-графа фрагмента шп1ь (Сз, Сл) возьмем кножество () г( х Уь Вершине (о, о') в швЫ (6» Сз) з 1 в. К котла, и к. слзлллелльа припишем тот же оператор, который был приписан вершине о в 6 . Пусть Х вЂ” луч фрагмента Сг, начинающийся Л-дугой некоторого распознавателя о» сг е:— У~, и кончающийся либо дугой, ведущей к распознавателю, оператору петли вли заключительному оператору с;, либо выходом фрагмента С, с номером у. Тогда благодаря подобию Сг и С для всякой вершины о, ~ У~~ л-графа фрагмента Сэ ее соответствующая й-дуга также ведет к вершине сз, соответствующей распознавателю, оператору петли или заключительному оператору, либо является выходом Х,С (6 ) с тем же номером у.
Во фрагменте ши1$ (С„С,) в качестве луча, начинающегося Л-дугой вершины (и,, о,), мы возьмем тогда луч У, а его выходную дугу присоединим к вершине (о~, с,') нли, соответственно, объявим выходом с номером у. Пусть, далее, Х вЂ” луч фрагмента Ст, начинающийся входом с номером Ус и кончающийся либо дугой, ведущей к распознавателю, оператору петли или заключительному оператору о'„либо выходом фрагмента С, с номером у. Тогда в силу подобия С, и С, вход с номером й в УС (6 ) также ведет к некоторой вершние и,' или, соответственно, является выходом с номером у. В этом случае в качестве луча, начинающегося входом с номером й в ши1С (6„6,), мы возьмем луч Х, а его выходную дугу присоединим к вершине (о~, оэ) либо, соответственно, объявим выходом с номером у.
Иэ описанного построения следует, что фрагмент ши1$ (6, Сэ) может быть получен вз 6 применением схемы правил ЛТЗ (копировавне): каждый распознаватель, оператор петли н заключительшей оператор об= е'1 заменяется ~ еу~ копиями. Столько же копий нужно взять н для каждого из преобразователей тех лучей, которые начинаются выходными дугами вершины о, а соединение копий выполняется с использованием структуры л-графа второго фрагмента пары. Заметим, что количество вершин фрагмента ши1$ (С„Сэ) не превосходнт произведения количеств вершин 6, и 6.
Йз построения следует также ЬС(ши1$ (С, Сэ)) = Х,С(ши1с (6, Сг)). Взаимно однозначным соответствием вершин этих л-графов будет (о, о') (о', о). Кроме того, очевидно, ши1$ (См 6,) — Ст, а операция ши1$ не нарушает свойство приведениости фрагмента. Таким образом, фрагменты ши1с (С, Сэ) и ши1$ (См 6,) образуют согласованную пару. ( у На рис. 6.10 показан пример процесса согласования для двух приведенных схем Бел, Бел. 3.3. Полнота системы Х„,. Т е о р е м а 6.6. Система Х~ — лслнал система лт-эвеиеалентнмх вреобрамаанмй фрагменлим, т. е. лт ле 6 — С,с+6, С .
Д о к а з а т ел ь с т в о. С учетом теорем 6.3 н 6.5 достаточхт т во покивать Ст 6, для фрагментов 6„6, Сг — Сю составля- ИО (Рве. 6ЛС~. Согзасовааве двух првведевпмх схем Бел и оее ющих согласованную пару. Обозначим через Х, (е) луч, начвнавицийся Ь-дугой е распознавателя или входом е во фрагменте 6е (е = 1, 2) и ваканчивающийся дугой, ведущей к распознавателю, оператору петли, заключителъному оператору или к первой из пересылок выходного вектора пересылок этого фрагмента; И: 6г-+ 6е — взаимно однозначное соответствие входов, ааключителвных операторов, операторов петли, распознавателей и их ае тз~ выходных дуг, которое существует благодаря совпадению л-гра- 4 в С, и С,.
Преобразуем фрагмент С, во фрагмент Сп заменяя в нем всякое вхождение луча и И У, ~е) Е1(е) на луч 1 | Ут( ЛЕ(е)) 1 Ь Ь Это преобразование можно выполнить однократным применением ЛТ5, поскольку в силу условия согласованности (СЗ) результаты добавляемых преобразователей не встречаются в исходном фрагменте С, а потому и не могут влиять на распознаватели, заключительные операторы и выходы в С,. Пусть теперь и — произвольный распознаватель, заключительный оператор или одна нз пересылок выходного вектора пересылок в С„х — ее г-й аргумент, а у — ю-й аргумент вершины Ы (и) во фрагменте С,.
Покажем, что тогда инварианты всех дуг е, ведущих к о в Сп содержат равенство л = у. Действительно, предположение (х = у) ~ штат (С» е) означает существование такого пути иг, начинающегося некоторым входом и кончающегося дугой е в С, что г (ю, х) ~ г (ю, у). Последнее, в свою очередь, означает, что фрагменты С и Сз не являются логико-термально эквивалентными, т. е. мы получили противоречие с исходным предположением. Итак, применением ЛТ8 ю-й аргумент каждой из вершин-распознавателей, заключительных операторов и выходных пересылок о в С можно заменить на соответствующий ($-й) аргумент вершины Ео (г) из С .
В результате такого преобразования на каждом из лучей а Х (е) ~ Ю (Ы (е)) в Ь в С~ преобразователи из Х (е) становятся неиспользуемыми, и их можно удалить применением схемы правил ЛТ5. После этого преобразования фрагмент Сг окажется совпадающим с фрагментом Сз. ( ~ Итак, Х„, — полная система лт-эквивалентных креобразоваиий стандартных схем и их фрагментов. Заметны, что из описанного в доказательстве теоремы 6.6 процесса преобразования лт-эквивалентных фрагментов друг в друга можно извлечь и алгоритм распознавания лт-эквивалентности. $32 С л е д с т в и е 6.1, Сук)всжвуети алворитм расяовнаванил лт-ллвивалвняэностяи аиандаржных слэм (р)рлвмвнвмы). Д о к а з а т ел ъ с т в о состоит в описании алгоритма. 1.
Преобразуем исходные фрагменты Сэ и Сэ в приведенные фрагменты. 2. Распознаем подобие полученных фрагментов. Если они не лт подобны, то 6 )- Сэ. 3, ('троны согласованную пару фрагментов 6т = гпп)В (Сю Са) и'С,=ш )В(С„Сд. 4. По Ст и Сэ строки фрагмент 6, как зто описано в доказательстве теоремы 6.6, а затем его стационарную рааметку. 5. Если не выполнены условия некоторых аз упомянутых в докааателъстве теоремы 6.6 применений схемы правил ЛТ6, то лт лт Сг ) 6, в противном случае 6 С. 3 а д а н и е 6.4. Докажите, что с помощью преобраэозаннб иэ Х всякую стандартную схему можно преобраэокать з схему беэ пересылок [60), т.
е. беэ операторов зиэа %= у, где л, у ти х . 3 а д а и и е 6.6. Покажите, что для описанного выше алгорнтма распоэнааания лт-экоиэалеитности стандартных схем (фрагмеитоз) имеет место аерхняя оценка сложности 0(лт), где л — максимум раэмероа исходных схем )66). Краткий обзор и комментарии Логике-термальную эквивалентность ввел в рассмотрение Иткин )22), он же построил первый весьма сложный алгоритм ее распознавания. Буда описал (4) алгоритм распознавания с показателыюй верхней оценкой сложности, сводящий проблему к распознаванию эквивалентности в подклассе двухленточных .
автоматов. Описанный в этой главе полиномиалъный алгоритм был построен в работе (65). На возможность автоматического построения инвариантов впервые укааал Летичевский Р4), Килдел предложил )112) алгебраизацию для объектов, которые в настоящей главе трактуются как пометки, и описал алгоритм нахождения инвариантов. Описанное адесь представление инвариантов в виде функционалъных сетей, позволяющее строить полнномиалъные по сложности алгоритмы глобалъного аналиаа, заимствовано из работ (65, 5). гллвА т РАЗРЕШИМЫЕ ПОДКЛАССЫ СТАНДАРТНЫХ СХЕМ Реэультаты гл.
5 носят «отрицательный» характер — главные проблемы теории схем программ (проблемы эквивалентности, пустоты, тотальности, свободы) оказываются нераэрешимымв в классе стандартных схем. В этой главе мы концентрируем внимание на тех подклассах стандартных схем, для которых удалось установить разрешимость всех или некоторых главных проблем. Тот факт, что главные проблемы оказываются неразрешимыми для стандартных схем, ни в коей мере не дискредитирует идею схематизации программ, лишь устаналивает те границы, в рамках которых следует продолжить поиск разрешимых случаев путем сужения классов иэучаемых схем и выбора отношений эквивалентности более сильных, чем отношение функциональной эквивалентности.
Нера»решимость главных проблем для стандартных схем отражает сложность вэаимодействия логической и информационной структур программ, даже если для их построения используется неболыной набор программных примитивов, перечисленных в $1 гл. 5. Нера»решимости в схемах проецируются на практические программы в образе тех трудностей, которые приходится преодолевать при создании достаточно развитых систем автоматизации программирования. Поэтому особый интерес представляет обнаружение разрешимых подклассов стандартных схем, выделение тех причин и ситуаций, которые ответственны эа разрешимость нли неразрешимость. Хотя сужение класса исследуемых схем представляется естественным направлением поиска «хороших» подклассов, само по себе око не гарантирует успеха, н отличие разрешимого подкласса от нераэрешимого может оказаться довольно тонким.
Достаточно напомнить, что в гл. 5 была выявлена неразрешимость очень у»кого подкласса О» ставдартных схем, базис которого содержит лишь две переменные, константу, один функциональный и один преднкатный символ, а операторы присваивания имеют вид х,:= а или х,:= ~(л,), где ~ = 1„2. Можно определить класс,У так, чтобы он отличался от Э', лишь тем, что он не содержит констант (и операторов засылки констшп), но содержит оператор пересылки х:= лп В этом классе проблемы пустоты и эквивалентности не являются частично раэрешимыми. Далее, можно удалить и оператор пересылки, считая, что каждая схема в полученном классе д'» начинается фрагментом (старт (хт), 1: хз ." = ~ (хг), 2: хг:=1(хг), -), где оператор х:= ~ (хг) встречается не более одного раза в еле ме.
Этот класс также ве является частично разрешимым в отно- шении проблем пустоты в эквивалентности. Однако если в базис класса Уг добавить еще одну константу Ь и соответственно оператор засылки этой константы х:= Ь и начинать все схемы одинаковым фрагментом (старт, 1: х:=а, 2:х,:=Ь, -) (константы нигде в схеме болыве не встречаются), то получим класс Р„в котором проблемы пустоты и эквивалентности разре- шими. Легко видеть, что тогда оказывается разрешимым и под- класс Уз стаццартвыл схем с базисом Мз = ((хм хт), ((Ф), (р®), (хг . = ( (хг), хт . '= ~ (хз), р (хг), р (хз), стоп (хм хз))).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
