Нижние оценки сложности вычислений модельными программами на ограниченных областях тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

КОШШШЁ ОРДЕНА ЛЕВИНА, ОРДЕНА ОКТЯБРЬСКОЙ РЕВОЛЩГП1, ОРДЕНА ТРУДОВОГО КРАСНОЮ ЗНАМЕНИ ГОСУДАРСТВЕННЬШ УЩВЕРС1ГЙ? Ш81Ш М.В.ЛЖОНОСОВА

®ааультег ВМ и К

На правах рукопяоп

гп ' КОСОВСКИЙ

^ I $ Николай Кириллович

УЖ 519.712

НШНИЕ ОЦЕНКИ СЛОЖНОСТИ ШЧШЯЕНИ0 модальным ПГОГРАШАЫЙ НА ОГРАНЙЧЕШШХ ОБЛАСТЯХ

01.01.09 - математическая кибернетика

АВТОРЕФЕРАТ диссертации на соискание ученой степени доктора физико-математических науп

Москва - 1987

Работа выполнена на кафедре математического обеспечения ЗВ1 ыатематико-механического факультета Ленинградского ордена Ленина и ордена Трудового Красного Знамени государственное университета имеии А.А.Дданова

Официальные оппоненты - доктор физико-математических наук •• Абрамов С.А.

доктор физико-математических наук Анисимов A.B.

доктор физико-математических наук , , Барздинь Я.Ы.

Ведущее пргдпр^гне - Институт математики СО АН СССР

Защита диссертации состоится " " ' ; ." ' 1988

в '- чао._; мин. на заседании специализированного

Совета V- 4 Д.053.05.38 по математике при МГУ по адресу: II9899 ГСП, Москва, II7234, Ленинские Горы, ШУ, факультет Вычислительной математики и кибернетики, ауд, ' .

С диссертацией можно ознакомиться в библиотеке факуль тета Вычислительной математики и кибернетики,

Автореферат разослан " " 1Э8ЭТ.

Ученый секретарь специализированного Совета № 4 по математике при ШУ

доцент '—-? Н.П.Трифонов

- | ОБЩАЯ'ХЛРШДОКЯОД РАБОШ

•МЩяьность темы исследования. Работа посвящена раэра-^¿рГ^'спо^обоз доказательств некоторых существенных сеойств шде/ашх программ по проверке наличия решение у урата-шй некоторых типов в синтаксически ограниченной дасиреткой >бяами»

Одни иодежьтэ програюш предназначены для решения задач, ^опускащкх краткую катечаетгоескл точную формулировку, пото-зуэ иояю записать в кошгзнтаркн программы (в виде спэщфие-

. Другая моцельгаго. ярэграшн рйскшт^задачи, не пкеюорго та-юго тяпа сущосшлшо независимого 6т программы описания ре-?ультатсс р'боп програнш. В связи с Л'радиционнши шиоиати-исслэдоваянош наибольший интерес представляют аедош ~"эямо первого типа, которые и рассматриваются в настоящей ра-

Дзгсазательстал свойств отдельных программ кая правило ¡ттладававтея в ргыкя иссладовагосй но коррекетссте проррзАй*. 'га кшкя эмж исследований 2йходаго' получение шаних оц&кох кмабк-гшзрйотой: сяошости и. «ела патов любых 'возмоги®: программ, рвдаяярх г^ачу'проверки наличия ркггння у .уризяений с .вара-¡й&рехга в- кглэ' сграглчегтой дкекре-жй области. Над основных рззультатеэ палуиса йа основа использования скрктой ушговрса-сгзггуг:, ^одатарзвагсет вгпислешЛ одного типа другими вжшзла-ГШЖЗ 9 ПОЛЕХЮЭДМЛЬШ ОГргЯКЧСГШГОЙ ДЙСКрЗТНОЙ области. ЙЮТШ акэпет первоначальна доказнвазюся для ктисленяЯ-па каланах й®ряк№'. .010! .быть поронесеш на другоэ модели вдоиеяв-шщ.ЛЬпая возгкпясй'гь пзрепзевнйя установлена дяя ко>»бт;ацп-ваией.сгсш5М?а схеа'из йгйцронашаос. элементов. .

Х^ашгаа; цутей йзупгяия объема гарантированной Ьа^кеки^ кяяп- ввдейьшш' прогрзгшяаа задач в обяузттештшесках^фбрау-зкроагах' является нута: от доказательства невозможности постро-ейяя шггорйтаюв и ирограйм я доказательствам иевсзногности ви-ежугешй на оставэ иоделышх пр-згршш о теш ш шдги ограш-«ащоа рзсурсазга, яаоащсатса • прадеде верго числа еагов, числа пгапазьзуеиет: ячеез п т.к.

Вопроса епзцнфшЕЩШ! программ стоят весы га остро. Оки всзншсаюг при проектирований новых программных систем. При своп весьш полезнш является доказательство тех или 'шик свойств ыодвльшх програш (их корректности или нзшшх оцено: числа шагов любой недельной програвды, решающей поставленную задачу).

Особый вдтерсс представляй! воэмояности оптимизации ал-горашов, проворящих существовать решения (хотя бы у тех уравнений, у которых она пожег быть осуществлена конечный пе рсбороа кандидатов в решения), но программирование перзбора "и лоб" но позволяет провести вычисления на только на современных ШЦ, но и на 8В»1 блигайшэго будущего, кз-за катастрофа ческой нехватки необходимых ресурсов времени дяя проведения вычислений. . ■■■".'

Вз. установление шшшх оценок числа шагов проверки суще оизоваяия решетя у уравнений такого здгаа в значительной нор. направлена иасзсза-ая работа, В гех случаях, когда уравнения параметром рассматриваются г. дискретной обладая н имеется зависящая' от параметра верхняя граница длтш записи возыо.ж-г; реаший, предлагается называть их синтаксически ограниченным уравнениями с параметром (синтаксически явно указываемая вер няя граница искомого решения). Мошзо было бы называть их и переборными уравнениями. Только корни проведенных исследован уходят в вопросы алгоритмической разрешимости в алгебре и в математической логике. Саш исследования лежат в репсах 1штез сивно развивающейся метатеории.программирования, в той ее чш ти, которую обвешат математическая кибернетика и с которой тесно соприкасается математическое и программное обеспечение вычислительных машин и систем (специальность 05.13.II),

Цель работы. Работа носит теоретический характер. Ее целью является, в основном, разработка удобного подхода к доказательству свойств специфицированных програш ряда задач, "прозрачно" формулируемых в традиционных общематематических терминах, включая доказательство полиномиальных нижних оцешг числа шагов вычисления модельных программ, решающих эти зада-

чи (прзаде всего^ задачи установления существования реиояия у синтаксически ограниченных уравнений с парадатрота). Рассматриваются словарные, логико-арифметические и булевк функциональные уравнения, а такяо уравнения над битовыми строками.

Научная новизна. Ксторшо спецификации прогршл* можно начать с метода индуктивных утвервдений Р.Фяойда (1967 г.) и П.Наура (1266 г.). Состояние лреблеш в той ее части, которая соприкасается с практическим исяользозаккем кошеитаривв-спе-цификаций для доказательства коррэктностл прогрев.; кратко, но достаточно полно огргхена Р.ШАндерсоном (1979 г.).

Исторгло доказательств шик оценок числа шагов алгоритмов поу-штельно начать с работ Я.М.Барздиня (1952 г.) я Н.Ра-бяна (1963 г.). Полученные тогда оценки относились к таялч

вычислений, возмояности которых существенно урезаяы. Например, была доказана невозможность вычисления на точной счетчиковой машине .Смшзинв Минского) или на о,тщол:^. "т учной машине Тьир:пгга в реальное время для некоторых "прозрач-т" <£орыуляруешх в традищюгшах обчематеяатичеейизг тершнаж задач. Ешг разработал (и "вшатя" все его возможности) метод узкого песта (бутылочного горлышка).- Везязи с появлением новых методов получения гагагнх оценок изучение урезанных моделей вычислений представляет для метатеорий программирования в эсновном исторический интерес.

Лишь доказательство такой нижней оценки числа шагов, ко-горая не выроздается в тривиальную оценку при изменении моде-га вычислимости, представляет наибольший интерес, особенно зелл эта оценка - кубическая (или любая другая полиномиальная щенка, с полиномом более высокой степени) для числа аяецептоз з схеаах из функциональных элементов или для числа шагоё й.т-ишйний ка иааинэ Тьюринга (в том числе к дня недэяарлширо-' з г мной, поскольку она допускает существенно нзогра-л;тчешсо эасггарздлоливздио процесса тше зияя, чзо стаповхгся ссобен-ю актуальным в связи с ростом возможностей приложения таких кдагедоваакй). При решении проблекн скну&а схем из функцио-гвльиих элементов с заранее ограничений?« -«слом элементов в

схеме получение нижних оценок имеет существенное значение, характеризуя степень оптимальности применяемого метода синтеза, . Программистский интерес могут иметь такие задачи с пара-шаром, у алгортюв решашри которые, число шагов заведомо ограничено сверху функцией, например, экспоненциального вида, или, ецэ лучше, полиномом, поскольку тогда при многих значениях параметра ыояет оказаться перспективный решение этих задач на ЭВМ.

Среда таких задач оказываются универсальные переборные задачи (здесь для краткости эти задачи называются переборными задачами). Понятие переборной задачи было введено С.А.Куком в I97X г. По' существу оно формализует понятие полиномиальной взаимной представимости двух классов предикатов. '

Всплеск математических исследований в близкой области произооел в 1972 г., когда А.Р.Мейер предложил метод экономной записи протоколов работы машины Тьюринга кванторными средствами "естественно1' формулируемой теории (по существу иетод дву-ступенгаатого моделирования формулами логической теории вычислений с ограниченными ресурсами).

Развитию методов, доказательств для получения нижних оценок числа шагов алгоритмов установления разрешимости синтаксически ограниченных уравнений щло от изучения сложности логических теорий к установлению нижних оценок числа шагов проверки истинности формул теорий с теш или иными дополнительными ограничениями на структуру используемых формул (например, ограничивается число перемен кванторов), Наиболее важным частным случаем утверждений логических теорий, используемых в обширных областях математики, является полное отсутствие перемен кванторов. В этом случае рассматриваются только уравнения и тождества. Проверку тождеств легко свести к установлению существования решений у уравнений. Все это вызывает дополнительный интерес к изучению проверки существования решения у синтаксически ограниченных уравнений.

Системы, описываемые уравнениями, используются при исследованиях в областях системного программирования. Например, це-

лую монографию посвятил О'Доннел программированию в системах, описываемых уравнениями (1977 г.).

Отметим, что рассматриваемые ниже логико-арифметические уравнения включают в себя в качестве частного случая задачи по репюншо систем неравенств целочисленного линейного программирования. Исходные данные математических задач могут быть различного вида, тем не менее они могут быть закодированы (с помощью достаточно простой функции) натуральными числами. Любая переборная задача погружается в задачу по установлении разрешимости, синтаксически ограниченных логико-арифметических уравнений.

В 1976 г. автор предложил иетод экономного представления протоколов работы машины Тьюринга булевыми функциональными уравнениями (бескванторное двуступенчатое моделирование булевыми Зугасциональными уравнениями вычислений с числом шагов, ограниченным сверху функцией экспоненциального вида). Полу-теки нижние оценки числа шагов экспоненциального вида, в частности, и от параметров, адекгатных поставленной задаче. В качестве следствия впервые в 1981 г. удалось привести простые примеры переборных задач, являотросся задачами установления существования решения у булевых функциональных уравнений из некоторых классов и тлеющих полиномиальные нижние оценки (и полиномиальные верхние оценки) числа шагов недетерминированного вычисления. Это было выполнено, в частности, на основе предложенного способа установления низших оценок числа шагов алгоритмов посредством получения предварительной нижней:оценки числа шагов, зависящей от параметров, адекватных задаче (для последующей трансформации этой нижней оценки числа шагов в такую/которая зависит от длины исходных данных). .

До доказательства этих результатов получение полгагошгаль-ннх (более чем квадратичных) нижних оценок числа шагов для вычисления предикатов, "прозрачно" и кратко формулируемых в тра-дициишых общематематических терминах,.наталкивалось на значительные трудности. Их не удавалось преуделеть и за счет использования э, формулировке задачи скрыто:'; .универсальности различ-

кого рода. Какие-то результата получались лишь за счет значительного сужения рассматриваешх алгоритмических моделей вычислений. Следует отметить, что это общее явление, проявляющееся при изучении управляющих систем, начиная с известных работ О.И.Нащшорука,

Как показал автор, полином любой наперед заданной степени ыоггег быть нижней оценкой числа шагов машины Тьиркнга, решающей соответствутацуи степени полинома переборную задачу по установлению существования решения у синтаксически ограниченных логико-арифметических уравнений (.решения в натуральных числах, длшш записи которых в "позиционной системе счисления ограничены соответственно выбранным полиномом). Обширны даогае библиографии работ, посвященных переборным задачам, одето полиномиальные нижние оценки одела шагов переборных задач еще не успег ли включить в етл бибдиогра<|ш (для полиномов степени больше двух).

А.-Адахи, С.Ивата, ТЛСасаи (из Японии) в 1984 г. (краткое нэлонение в 1981 гЛ получили полиномиальные нижкио оценки числа шагов вычислений на ыазшнах Тьюринга для задач, которые формулируются в терминах существования выигрывающей стратегии для некоторых достаточно сложно формулируемых специальных игр, а да в терминах существования решения у уравнений. Доказательство же переборное?!! этих задач привело бы к решению одной из труднейших задач алгоритмической математики (к доказательству совпадения класса полиношаяьно вычислимых предикатов с классом предикатов, вычислимых недетерминированными шшшиаин Тьв-ринга за полиномиальное число шагов). Практический интерес к решению этой труднейшей задачи в существенной чадти устранили полиномиальные нижние оценки числа шагов ряда переборных задач, доказанные автором.

Дальнейшее развитие разработанных автором диссертации методов позволило предложить простой пример последовательности булевых функций максимальной (по порядку) схемной сложности. Каждая булева функция не допускает схемной реализации с числен элементов, являющимся экспонентом Лпри некотором основании) с

аргументом, рапным числу аргументов булевой функции. Ярмэр представляет собой установление существования решения," дана которого ограничена двукратной энспонентой от дополнительного параметра, у догико-архфлетического уравнения. Любые две булевы функции предлагаемой последовательности совпадают, если фясировать дополнительные аргументы функции,-имеющей большее число аргументов. Первый несравнимо более сложный примор такого рода, допускающий схе!лную реализации только с экспоненциальным числом элементов, был основан на алгоритмически неразрешимой тоории и принадлежит Л.Дя.Стокмейеру (1974 г.) (подробное описание п:а русском языке имеется в монографии Р. Г, Нип.'атул,тша). Важность задачи построения индивидуальных последовательностей булевнх функций, имеющих высокую сложность' рс':.с-1зац;п5 в классе схем из (функциональных элементов, отмечалась ранее С.В.Яблонским в 1969 г. и О.Б.Лупановнм в 1970 г.

При использовании спецификаций программ, радполоашжс з гаде комментариев-описаний текущих значений переменных (л(.;.>»в вшолизкия оператора, предаестзуицвго ст&щфямгуш) потребовалась разработка семантики корректности (правильности) таких программ со спецификациями. 8та сема/.тика предназначена для практического доказательства правильности учебных программ.в. процессе их написания. Семантика Ч.Хоара для языка утверждений о частичной корректности программ оказалась явно недостаточной. Поэтому подход Ч.Хоара развивался одновременно в нескольких направлениях, в частности, З.Дейкстрой. Общематематичзское обобщение подхода Ч. Хоара в рамках индуцированных программа™ преобразований множеств было подробно изучено С.А,Абрамовым. • . "... ; -' .V. :' ' ' ' • '

Б ^твмаэшёсюйГййбёр1в'5Рйюе с^рии^ваясй 'подход »- понятию алгоритма, как к сложной - управляющей системе . Шя-ая концепция кибернетических управляющих систем била развита С.В.Яблсн-.еккм (1959 Д7.),."0а ввел и уточнил такие понятия кибараетичас-гагзс систем как управлеаге, память, реализация, езеека, сложно нссть и ряд других. Нэ только теягачёские устройства обработки информации являются конкретным воплощением разнообразных алго-

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

Первоначальным этапом развития теории программирования можно считать метод представления алгоритмов, разработанный в 50-х годах нашего столетия А.А.Ляпуновым. Операторный метод оказался удобным аппаратом исследований. Значительный вклад в развитие операторного подхода и теории схем программ, родившейся на его основе, внесли А.П.Ершов, Н.А.Криницкий, В.Е.Ко-тов, Р.И.Подловченно, С.И.Янов.

Дня изучения соответствия математических описаний возмоа-ности их использования на 8ВД автор считает полезным изучать такие программы, математически точные спецификации которых могут быть предложены. В свези с этим необходимо отлететь практическую полезность разработки такой семантики, которая бы позволила локализовать проверку правильности модельных программ с комментариями. Именно такая семантика была разработана автором. Ее преимущества могут быть использованы при обучении программированию студентов и даже школьников. Ваяно, что при этом программа специально не подгоняется под те или иные удобные средства доказательства, а остается в традиционном удобном для использования на ЕШ виде.

Семантика метода индуктивных утверадений (по «шеш» автора вместо слова утверждение точнее было бы использовать слова описание или условие) была формализована автором в концепции понятая корректности почти в цело** для программ со спецификациями-комментариями.

Юдиным направлением, разрабатываемым автором, является исследование спецификаций модельных программ доя обеспечения получения нижних оценок числа шагов явно ограниченных вычислений, содержащих параметры. Преаде всвго демонстрируютсявоз-можности спецификаций модельных программ ддя доказательства их корректности в целом. Изучается установление существования решения в явно ограниченной параметром дискретной области у уравнений с параметром. Наибольший интерес при этомвызывает возможность получения полиномиальных нижних оценок числа шагов вычислений. На пути к этой цели и былиполучены основные

результаты. Была применена единая идея выявления скрытой универсализации с помощью уравнений, рассматриваемых над дискретной область», полиномиально ограниченной параметром уравнения.

Выбор машины Тьюринга как модели вычисления связан прежде всего с тем, что как правило необходимые ресурсы для любой кодели вычисления сравниваются с таковыми ресурсами для машин Тьюринга. Сказанное позволяет преобразовать нижние оценки чис-аа шагов, полученные для вычислений на машинах Тьюринга, на цругие модели вычисления, " включая схемы из функциональных эле-¿ентов.; ЕЬследнее Обеспечивает широкую полосу возможных кибер-1втетеских применений полученных результатов.

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

Методы исследований. Выявление среда задач тех, для кото-юс удается доказать высокую сложность реализации в классе хеа из функциональных элементов относится к традиционно слоз-ни вопроса« математической кибернетики. В атих вопросах уда-тся добиться органического единства традиционных и новейших входов исследования алгоритмов, намечаемых для многократного спользоваяия в виде программ для ЭВМ. Для получения нижних ценок слоетости реализации в классе схеи из функциональных педантов предложена эффективная техника доказательства, ссно-анаая на новом подходе - концепции синтаксически ограничевдо-> уравнения (уравнения, рассматршаемого над даскретной син-ассичдскн явно ограниченной областью). Исследование нижних1 щнок слолнссти реализации в классе схем из функциональных гененгов дня проверки существования решеккя у таких уравнений шяэтся фундаментальной модельной задачей.

Сравнение с другими предикатами в "Прозрачной" и краткой рцулировле позволяет, во-пераых^ ^пере^стаг модифицированную

гезгдау доказательств также для получения нижних оценок числа иагов полиномиального вида (с достаточно высокой степенью по-лкиоиа) по сравнения) с экспоненциальными границами, полученными ранее другими исследователями, и главное, во-вторых, использовать. предаоааюше методы для решения разнообразных задач об-Е55Ш2еыатцчвзкой формулировка по установления нижних оценок числа кагов разрешающее эти задачи алгоритмов - границ пешшо-шалыюго вида С с достаточно высокой степеньа полинома). Такие шшпю оценки позволяэт отделить формулировки задач, при рэае-ш которых невозможно эффективно использовать ЭВМ для доста-тес-ю большого разнообразия многих исходных данных.

В работе созданы новые ор1гтеальше методы исследования, позволяющие получать актуальные: для натештической кибернетики' результаты. Развитие предложенной теоретической концепции для выявления шаш оценок числа шагов алгортюв, провержергх С^щзетвовашэ решння у рассматриваемых уравнений* сштаксичос щ ограниченных по величине, позволяло создать и практически апробировать ряд новых методологических подходов для решения проблем, имеющих прикладное значение в ыотатеорил програширо-вакия.

Практическая значимость. В прикладном аспекте синтаксически ограниченные уравнения отражают модельным образом основные свойства гарантированной возможности удачного завершения поиска мнфорлации и, в частности, дада для переборных задач единую методологию понимания и анализа нижних оценок числа шагов вычислений полиномиального вида (в том числе и вычислений с использованием недетершшировшшых шнаш Тьюринга, имеющих существенные возможности распараллеливания вычгглений). Поэтому развитие предлагаемо^ концепции имеет разные выходы в конкретные практические проблемы.

Реализация результатов. В последние годы исследования про водились в рамках теш "Развитие методов и средств системного программирования", выполненной в XI пятилетке кафедрой математического обеспечения ЗВМ математико-механи^еского факультета Ленинградского госуниверситета, а также в теме "Теоретико-ал-

эрктмическиз оценки сложности вычислений", выполненной тзл s под руководством автора.

Основные результаты работы внедрены в учебный процесс в эшнградском государственном университете.

Публикации и апробация. Основные результаты докладывались 1 Втором Международном совещании по искусственному интоллек-г {.Репино, IS80 г.), на семшгаре кафедры вычислительной натё-1тики и вычислительной техники фааультзта естественных наук швзрситета кы. Лоранда Зтвеша (Будапешт, 1982 г.), на УШ ;адунаро,цном конгрессе по логике, методологии и (философии наги (Москва, Î987 г.), а также на "конференциях и симпозиумах: i шеетсй международной конференции "Основы теории вычислений" [азань, IS87 г.), на четвертой, шестой, седьмой и восьмой :сеожзкых конференциях по математической логике (Кишинев, ¡76 г., Тбилиси, 1982 г., Новосибирск, 1984 г., Москва, . 65 г.), на первом и втором Всесоюзных семинарах !'0це:па cms-ст-и выделений" (Ленинград, 193£ г., Гродно, 1983 г.), ira , Бсезокзной конференции по теоретическим проблемам киб-грнэ-нн (Саратов, 1983 г.); были представлены на УТЛ Всесоюзной нференции "Логика и методология науки" (Паланга, 1982 г.), УП Мездународшзм конгрессе по логике, методологии и филосо-и науки (Зальцбург, 1983 г.), на УП Всесоюзной конференции роблеиы теоретической кибернетики" (Иркутск, 1985 г.); издались на первом и втором Всесоюзных с ем:-шарж по дискретной тематике и ее прило.т.ещ1Ям (Москва, 'Ï984 г., 1987 г.), на зеоюзной школе-семинаре "Нижние оценки сложности"-(Казань, 35 г.), на постоянных семинарах Ленинградского отделения Фанатического института им. В.А.Стеклова АН СССР, Лейдагреде-го • госуниверситета, Института киберкеттоси. Ш ЭССР и на'с.еми-эах по кибернетики и по системному программированию з МГУ; торкались в специальных курсах, читавшихся автором на мате-гехо-мёханическсм факультете Ленинградского госуназорситета -.гстично изложены в книгах автора "Элементы математической тляк и ее прияоженкя к теории субрек}фсивнн>: алгоритмов" шквград, 1981 г.), "Основы теории влё^гёнтаркзд: алгоритмов"

(Ленинград, 1987 г.). Основные результаты работы отражены в 24 публикациях.

Структура и объем работы. Диссертация состоит из введеш пяти глав, объединенных в два раздела, заключения, списка использованной литературы и приложения. Объем работы 191 е., включая 9 страниц списка использованной литературы, наечимда щвго 80 наименований. Приложение состоит из двух справок о внедрении полученных результатов в учебный процесс.

ОСНОВНОЕ СОДЕВШШИЕ РАБОТЫ .

Во введении содериится обзор проведенных автором ксслед ваний. Работа имеёт два раздела.

В первой главе первого раздела для доказательства свойс модальных программ вводится понятие корректности в целом для специфицированных программ. Это понятие обеспечивает техноло гическое удобство доказательства корректности программ (на о нова использования локализованных комментариев-спецификаций)

Предлагаемая семантика корректности специфицированных программ развивает метод индуктивных утверадений, восходящ^ Р.8яойду, П.Наура и достаточно подробно описанный Р.Андерсон В остальных главах первого раздела достаточно полно hsj гаются фундаментальные исходные результаты о задании еловар предикатов посредством синтаксически ограниченных уравнений над строками. Изучению невозможности такого задания для нек< торых предикатов, доцускающих краткую "прозрачную" форь$глир< ку в простых традиционных общематематических терминах"nocBHi на третья глава первого раздела. Результаты этой главы непо< родственно используются в следующем разделе, обосновывая не' ходимость введения побитовых операций.

Второй раздел является основным в диссертации по получ нию тзхнически наиболее сложных результатов. Он посвящен ак альным в настоящее время вопросам доказательства нижних оце комбинационной сложности (и нижних оценок числа шагов) пров ки существование решений у синтаксически., ограниченных уравн вий ущЕййщй, щ, -величину

еиений которых накладываются явно задаваемые (синтаксические) граничения). В этом разделе разработаны основы для получения шших оценок числа шагов алгоритмов по проверке существования етений. Первая глава этого раздела направлена в основном на зучение уравнений над битовыми строками, логико-арифметичес-их уравнений (длина записи решений ограничена сверху функцией, ависящей от длины записи параметра).В последнем параграфе той главы изучается реализация проверки существования двукрат-

0 экспоненциально ограниченных сверху решений у догико-ариф-етических уравнений схемами из функциональных элементов. Ус-анавливаатся экспоненциальная нижняя оценка числа необходимых дефектов. Это один нз основных результатов диссертации.

В последней (второй) главе изучаются булевы функциональна уравнения, установление существования решения у которых меет традиционно кибернетическую интерпретацию (непротиворе-ивость описания свойств схемы из функциональных элементов),

В целом содержание диссертации направлено на выявление вязи мегаду прикладным кибернетическим направлением в теории ¡лгоритмов и теоретическими вопросами изучения коделышх прог-аи!. Прикладное направление в теории алгоритмов заставило ¡зглянуть на понятие алгоритма с новой точки зрения, что пришло к постановке нового круга актуальных проблем, связанных,

1 частности, с. нижними оценками возможности оптимизации алго-итиов и. схем из функциональных элементов.

При рассмотрении задач, просто формулируемых в общематэ-¡атических терминах, наибольшую трудность для большинства мо-[елей вычислимости достаточно общего вида вызывает получение кжнгос оценок (числа шагов) полиномиального вида в случаях,' . :огда степень полинома больше двух. В этом случае верхнйя Ъцен-:а экспоненциального ввда должна ограничивать друг рассматря-¡аймых задач. Эта ситуация является достаточно общей в совре-генной декретной математшее и в математической кибернетике.

Одним из сагшх просто формулируемых.^ общематематичееннх •срглЕгах примеров задач, для которых автором доказано, что юяккй алгоритм, рэпающий ее, требует бо'лзе, чем |Х| шагоЕ

вычисления (го есть не коает рзшть задачу на недетерминиро-. ванной машине Тьюринга ва |X | шагов для любого натурального числа X ), является следующая задача: по натуральным числен К, X а многочлену Р с целыми коэффициентами от переменных , в котором используется дополнительная операция поразрядного увдогешш двоичного представления аргументов, провеять, можно ли найти такие натуральные числа Х^,.., сумма длин двоичной записи которых не превосходит |Х| , что имеет место равенство , где переменные

используются дяя натуральных чисел и Е - большее нуля рациональное число (IXI означает длину записи натурального числа в двоичной'системе счисления) ъ

Отметим, что дяя уравнения В=0 , где Р имеет вид, опк санный в этом примере, автором используется термин "логако-арыфметическое уравнение". Доказано, что уравнение Р=0 гдш в этом призере зафиксировать (при введении дошшштельного а] х^мента). Это фиксированное уравнение иоквт быть построено простым регулярным'образом при ограничении сверху на степень Р и число его переманных.

Далее, число К в этой задаче может быть сведено к одш щ, если вместо логико-арифметического уравнения использовать равенство нулю функций, являюсросся суперпозициями следующих-функций: ушошзния, выделения целой части квадратного норш, поразрядного умножения двоичных представлений аргументов и в: числбшш максимума из разности двух аргументов и нуля. Вообщ! говоря, равенство нулю функции указанного здесь вида ыошо в этом примерз зафиксировать, добавив дополнительный аргумент (подстановка натуральных чисел вместо дополнительного параме ра обеспечивает бесконечное число частных случаев задачи).

Описанные задачи носят универсальный характер. К ним, в частности, могут быть сведены ¿шогие переборное задачи, если алгоритм, решаюг^й ее, и алгоритм, выполняющий сведение, при вычислении на недетерыинировиаюй односторотге-одноденточной кашке Тьюринга в совокупности имеют число шагов, ограшчьш; поташомом степени Т . Наиболее удобно применять полученные

низкие оценки для многих моделей вычисления в тех случаях,когда достаточно показать, что степень полинома и низшей оценке очень велика (тысячи или сотни). Тогда доказывается невозможность получения гарантий практического вычисления.на ЭВМ (для достаточно представительного разнообразия длинных исходных данных) задач с такой нишей оценкой.

Сказанное поясняет возможность оценочного использования полученных результатов для отделения таких задач, гарантии практического вычисления за ограниченное число шагов которых на 2ВМ никогда не смогут быть даш (при разадобр^ны^ достаточно длинных исходных данных).

Если у уравнений в словах исключить поразрядной 'умножение п учитывать только такие решения, для записи которых требуется меньше места, чем степень дйинн записи уравне:г;я, ¡го-'т^йз^аеу-ся задача, пзрзборность которой доказали Л.Эдлкмэн й дере в работе, представленной на 16-ел симпозиуме по" осмеаяя? ям иокпьвдер сайенс (1975 г.). Однако нижние оценки на число,'", " шагов машины Тьэрикга, реи&'зщяй. вту задачу, до сих пер еще не получены. Вярбчбн, для -метатеории щюгуамшровюшя талая задача, являясь линь одной из многочисленных переборных задач, не прздак ¿хяв'л особенного интереса. .

Полученные результаты диссертации существенно уточняют теорему, аннексированную Л.Вдяимэном и К.Д.Маадерсои (в статье 197о г., содержание которой изложено на русском языке в айда добавления переводчика к переводу другой их статьи). . Уточнение касается степени полинома в ограничении дайны записи ройэннй лоппго-арифгетическю: уравнений. Доказательство этой геореш ими не опубликовано до сих пор, хотя и анонсировано ещэ в 1976 г. (возможно, она была сформулирована в слишком сильной форме). Эти автора использовали в своих исследованиях-конструкции доказательств, полученных Ю.В.Матипсевипем для установления даофантовоста перечисятшх множеств.

Если будет доказано, что класс Р равен классу предикатов, зычиагооах за полиномиальное число шагов на недетерйяш-рованных малинах Тьюринга (и тем самым будет положительно рз-

шена считающаяся одной из труднейших задач современной теории алгоритмов), то предлагаемые в диссертации примеры переборных задач с нижними полиномиальными оценка!® будут иметь также и верхние полиномиальные оценки на число шагов детеринированной малины Тьюринга, решающей эти задачи. Если же будет доказано, что такое предположение неверно, то предлагаемые в диссертации примеры переборных задач с нижними полиномиальными оценками на число шагов не будут принадлежать классу Р (т.е. будет доказано, что предлагаемые задачи являются еще более сложными).

Изучение нижних оценок числа шагов синтаксически ограниченных вычислений, существенно проясняя теоретическую картину, отражает важную тенденцию современного этапа развития математической кибернетики, заключающуюся в акцентировании внимания на качество алгоритмов, предлагаемых для программирования на ЭВМ. Абстрактную иерархию предикатов, вычислимых за существенно различное число шагов недетерминированных вычислений, детально изучил еще С.А.Кук в 1973 г. К согляонию/ его классификация не позволяет непосредственно по .сяктакбвПгскш свойствам записи предикатов получат.» нижние оценки числа шагов недетерминированных вычислений для предикатов, "прозрачно" формулируемых е общэыатематичеакт терминах, Различные,методы решения, логических уравнений предлагали еще основатели математической логики: ^.Вуль, з.Шредер, П.С.Порецкий. Новый вариант поста-ковки задачи решения логических уравнений, состоящий в поиске таких формул, замена которыми неизвестных превращает.уравнение в выводимую формулу, предложил А.Таутс, который дал, в частности, метод решения логических уравнений, не содержащих ивдивидов и кванторов.

К рассматриваемой в диссертат;иад?здаче установления разрешимости булевых функциональных ур&нений близка постановка задачи, сформулированная А.Таутсом, однако в своей исходной формулировке решаемая здесь-:задача естественным образом описывается в терминах прототетики ЛесьнеЕского, описаяной также в книге А.Черча. Дуловы функциональные уравнения Представляют собой частный случай синтаксически ограниченных вычислений.

- -

Булевы функциональные уравнения рассматривал A.B.Кузнецов еще до i960 р.

С дальнейшей историей изучения булевых функциональных уравнений можно познакомиться по обстоятельной монографин С.Ру-дяну (1974 г.), посвященной булевым уравнениям. В этой монографии отмечается, что булевы функциональные уравнения можно свести к системам булевых уравнений, правда при стон число переменных преобразованной системы возрастет экспоненциально с ростом числа аргументов функции, играющей роль неизвестной в булевом функциональном уравнении. В связи с этим на стр. 206 этой монографии ставится следующая проблема: развить спедаайь'ную.таорив булевых функциональных уравнений, избегающую сведения к системе обычных булевых уравнений со слишком многими уравнениями.

В диссертации доказана невозможность такого сведения .'Действительно, разрешимость системы булевых уравнений vö^ö* Ifjjib установлена недетерминированной машиной Тьюринга задедлмо за квадратичное число шагов, от длины исходных данных. В то же' врет, из доказанные автором границ оптимизации числа шагов для решения даже ряда подклассов булевых функциональных уравнений существенно превосходит квадратичную функцию.

Интерес к доказательству 'нижних оценок числа шагов алгоритмов установления существования решений у синтаксически ограниченных уравнений обусловливается многими причинами.

Во-первых, масс предикатов вида "синтаксически ограниченной уравнение имеет решение" достаточно обширен и включает в себя многие, в том числе переборные, задачи, представляющие значительный практический интерес.

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

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

Наконец, синтаксически ограниченные уравнения являются частным случаем уравнений общего вида. Поэтому разработанная

методология способна изменить традиционную методологию установления существовании решений у.уразнений, приблизив ее к практическим реализациям* на ЗЙ.1.

Трудности установления нижних оценок числа шагов алгоритмов связаны с необходимостью "обозреть" все множество алгоритмов. По существу речь идет о возможности существенно оптимизировать явно задаваемый перебор. Доказательство полиномиальной (очень большой степени) нияней оценки числа шагов алгоритма позволяет экономить время программистов, направив их на решение задач, допускающих более массовое использование.

Изучение сложностных свойств различных предикатов в настоящее время является обширнейшей областью. Для целей болзе краткого введения может послужить обзорная статья С.А.Кука, написанная в связи с присуждением ему премии Тьюринга за 1'982г, Для этой статьи были выбраны только 92 научные работы (с: нззх-нешгем перед теми учеными, которые ко упомянуты в этой статье), Обзор С.А.Кука выделяет сяедугацей (второй в пзрзчкв) раздел метатеории сложности вычислений: шгдаке оцоя'ск (он:; имеэт существенное <хяфикоенов&-ше с уафшйчёоки цздЗоюе сложади результатами диссертации). ' ■';■•;' •

Этот второй раздел разбит С.А.Куком на подразделы, среда которых более тесно касается настоящих исследований, во-первых, подраздел, посвященный. доказательствам для "естественных" раз- . репимых задач практической неосуществимости их разрешимости (в диссертации используется следующая характеристика: задачи в "прозрачной" общематематической формулировке) и, во-вторых, подраздел, посвященный универсальным переборным задачам. На пересечении этих подразделов автором диссертации и получены результаты, имеющие важное прагматически-математическое знале-ние. '. '

Настоящая работа позволяет пролить свет па то, насколько бесконечность может проникать в конечный объект посредством представления универсальн6:''слок!1ых. предикатов. 8то позволяет выявить новые аспекты в изучении управляющих систем, предлагая примеры последовательностей булевых функций, которые можно ре-

аднзовать схемами из фушщноналышх элементов в базисе из штриха . Шзффвра и притом только схемами максимальной (по порядку) сложности.

Опишем более детально содержание диссертации. Раздел I. содержит исходные' рассмотрения. В первой главе этого раздела предлагается способ эквивалентного пргобразования утверждения о зорреятности в, целом спец;:&щирозанней программы ¡с утварт-дешян о корректности в цэлои специфицированнйх программ, содержащих в путях гичлеленяя по крайней мере на один оператор каньпе. Рассматриваются условию операторы и оператор ютила.

Докаливается теорема о взахщозаменлмости нефш-чй:кх пра-еил для. доказательства корректности оператора цикла.

Рсссматриваатсл правила для рекурсивных процедур-операторов без параметров, запетая итеративнкэ процедуры, хотррщ по существу моделируют оператор перехода с возврате-л.

Вводится понятие полной зоррэктности э целок спецы; гл;тро< mnstx программ, обоопячягамтэо проверку огсутстыш зациилява« скосги в-процессе вшисяидая.

Дяя проверка щйшкльшсти программ, подтверждая гозмоэс-пость использовании 2ВМ в учебном процессе для доказательства правильности арограш, написании* на Паскале, А.В.Сочияпна создала программную реализация генератора условий правильности программ. Предложенная методика сопровождения программ спецификациями, для которых ворна корректность в целом, является основой для доказательства цростойшх свойстя программ.

В случав рассмотрения програл.!, функционально совпадающих с плассои всех примитивно рзкурсивтгых функций, можно предло-П1?ь исчисление равенств программ, взшиовлотшмое с исчислени-еа равенств пркмитиЕно peücypciroirax функций, введенным и деталь -ш изученным Р.Л.ГУдстейиом. В формулировке описываемого исчисления автору щйпадлезшт празияо индуктивного равенства прог-раня и здея использования локализованных переменных. Доказательство взаимовлохимости этих двух исчислений было проведено В.Я.Вочершковын при прохождении аспирантуры под руководство« автора.

Следующие две главы (последние в этом разделе) посвящанк изучению уравнений в словах (или, что одно и то же, уравнений в свободных полугруппах) относительно решений, ограниченных сверху по величине. Решен вопрос о представимости такими урав нениями предиката симметрии, интенсивно исследовавшегося с то ки зрения получения оценок числа шагов его вычисления на различных вариантах машн Тьюринга (широко известны работы Я.М. Барздиня (1962 г.) и А.О.Слисенко (1977 г.) ). В диссертации доказана непредставимость предиката симметрии уравнениями в словах и длинах слов (и, следовательно, уравнениями этого же типа, но с решениями, ограниченными по длине записи). Этот результат показывает, что эти уравнения обладают крайне ограниченными возможностями. Поэтому их изучение представляет в настоящее время лишь методический вспомогательный интерес для метатеории программирования и математической кибернегшск. В связи с этим к операции конкатенации в следующем разделе дня уравнений над битовыми строками добавляются опершая« побутзвн-ного максимума и минимума. Без такого доб-нвжагаш согласно доказанной здесь теореме швозкшно будез? обой1ись при моделировании произвольных вычислений га огракичшщое число шагов.;

Раздел 2 посвящен установлений существования решений у синтаксически ограниченных уравнений некоторых сигнатур как модельной задаче для получения нижних оценок числа шагов алгоритмов. Этот раздел делает основной шаг по получению технически сложных математических результатов, обеспечивающих получение нижних оценок числа шагов по проверке существования решений некоторых видов уравнений.

В главе 2.1. устанавливаются нижние оценки числа шагов проверки существования решений у ^шгачсически ограниченных логико-арифметических уравненлй.'-.ййтажсически ограниченные уравнения над битовыми строками и логико-арифметические уравнения были предложены автокод для взаимного моделирования вычислений на недетерминированных машинах Тьюринга за ограниченное число шагов и проверок существования решений у уравнение в натуральных числах, дайна записи которых в позиционной системе

числения ограничена значением функции, зависящей от параметра равнения»

Доказываются теоремы о моделировании недетерминированных лчислений на одноленточной машине Тьюринга за число шагов, рраниченное некоторой функцией от длины исходных данных, пос-эдством установления существования решений у синтаксически Траниченных уравнений над битовыми строками к логико-арифме-гаеских уравнений (синтаксическое ограничение на длину записи шгений этих уравнений с точностью до мультипликативной коне- . «ты !федставляет собой квадрат функции, ограничивающей, число 1гов вычисления). '

На языке синтаксически ограниченных диофантовых утдо;1ений втея описание каждого класса предикатов иерархии А.йкегорчи-натшная с класса всех элементарных по Калькару прзадкашв. едствиеы его является неэлементарность любого алгоритм* ттро-. рхи существования у полиномов целочисленннх корней," ьь ггрв- / сходящих кратно экспоненциальных ограничений, сти результаты ' пользуются для уменьшения количества операций ограниченного датровшпш и других операций (включай операции одноместного гегагого. суммирования), на которых может быть основано поставив „ункций каждого класса иерархии Г&егорчика, начиная с этьего.

Предложена серия переборных задач с высокими полиномиаль-ш нижними оценками числа шагов их вычисления (на однолен-иоЯ недетерминированной нашего Тьюринга). Эта граница имеет [ о точностью до мультипликативной константы. При

м верхняя граница числа шагов (с точностью до цультигшика-«ой константа) может иметь вид (х! ^ ' при любом поло-ельноы рациональном числе Е (при использовании многоленных недетердшированных машин Тьюринга).

Последний параграф этой главы наиболее существенен для днционной проблематики математической кибернетики. В ней взывается экспоненциальная сложность любой схемы, реализую-проверку существования решений у логико-арифметическюс вненкй. Развитая в предыдущих параграфах техника использу-

ется для получения нижней оценки числа элементов в схемах из функциональных элементов (в базисе из штриха Шафера). Для задачи установления существования также рзазний у логико-арифметических уравнений, длина записи которых в позицио1шой системе счисления ограничена двукратной экспонзнтой, доказывается экспоненциальная сложность любой схемы, реализующей каздув булеву функцию последовательности для решения этой задачи. Пр этом для моделирования вычисления значений наименьшей в лекси кографической записи булевой функции от Ы аргументов среда отличных от всех функций, имеющих сложность, не превосходимую экспоненты (с некоторой мультипликативной константой при аргу менте), используются логино-арфюгические уравнения.

Последняя глава диссертации посвящена шшшм оценкам чис ла шагов установления непротиворечивости описания контактных схем из функциональных элементов. Вычисления, произведшее не детерминированной машиной Тьгоринг-а за эксшнеда,иайькоа число шагов, моделируются булевыми.фунЕциопаякваш уразяешиЕЖ,, дли на которых ограничена сверху гтолиноа.;-« <ц*.-г»6% стзкшк. В качестве следствие получас гоя у.сапсшанциол»куго гида низшйя оценка числа патоа уотаковленгя (,р\етмьовтт рэшеник у булевых $унациоаальных уравнений. Дакьнейзсэд рассуждения испошгз т установленную С.А.Куком (1973 г.) иетрквиэльность иерархи! ь'здетермулшровшных машин Тьюринга. по степени полинома, ограничивающего число их шагов. Удачный выбор параметров, от поте шх зависит оценка, позволил произвести разбиение класса Есе;-булевых функциональных уравнений таким образом, что проверка существования решения у уравнений из каждого подкласса являе5 ся переборной задачей и для каздого подкласса доказывается пс линомиальная нижняя оценка числа, каг^в..алгоритма (оценка, зависящая от длины уравнения). •

Предлагается иерархия всех булевых функциональных уравн« ний (примеры простых переборных задач с полинолиальными шшп ми оценками числа шагов алгоритмов их решающих). Разбиеже нг подклассы имеет следующий вид: К-ый подкласс - это такой под-

ласе, для уравнений которого выполняется неравенство 1^2ЙАХ(Н',Р)/К ^ гдз у» _ хщцпо аргументов булевой функции, ходящей в уравнение в качестве неизвестного, Р - число гтро-озициональннх переменных, входящих в уравкениа, и Т - длзша улеиа функционального уравнения. Этот результат позволяет по-олнить впервые опубликованные автором примеры универсальных эрэборных задач в общематематической формулировке с полиноми-шшми шшшгш оценками на число шагов их вычисления недетер-шированнши 1и тем более деторщпшроЕанншз) нагинами Тыо-Я1га.

Отметин, что следующие пять результатов диссщй:?й$21 являйся основшш.

1. Выработана обеспечивающая локализованную проверку, се-лтика теорем вида: корректна в целом (а такяэ поякссг!>п"0р-агана в целом) программа, содержащая внутри себя ецификацки, язлягщиеся математичэски точтгии условии,',: . отношения мегэду значениями переменных после работ онератс- • з,- прэдшествующих кеммеотарйям. '

2. Предложены иравила-экБивалектнооти для установления рректности в целом оператора цикла, оператора рекурсивной оцедлгт-епбратора без параметров, соответствующие разработан-аной. сематине корректности в целом рассматриваемых программ.

3. Доказаны полиномкалъшз шетние оценки для числа шагов .'орнтаов решения переборных задач по установлению существо-шя решешш синтаксически ограниченных уравнений двух типов.

4. Доказаны экспоненциальные оценки сложности схем из шциональнИх элементов, реализующих проверку существования !вшй у логико-арифметических уравнений с двукратно зкепо-щиальными ограничениями сверху на длину записи (в позицион-I системе счисления) решений (ограничениями, зависящими от ш строки, являющейся запись» уравнения).;

5. Решена проблема, поставленная.С-Рудйну. Доказана ие-ыожность сведения булевых функциональных уравнешШ к не-ьаоиу числу обычных булевых уравнений. у

ЛИТЕРАТУРА

1. Абрамов С.А. Элементы анализа программ, М., 1986. 128 с.

2. Андерсон Р. Доказательство правильности программ. М.,1982. 168 с.

3. Барздинь Я.М. Об одном классе машин Тьюринга (машины Минского) // Алгебра и логика. 1952. Т. I. Ю 6. С. 42-51.

4. Пкегорчик А. Некоторые классы рекурсивных функций // Проблемы математической логики. Сложность алгоритмов и классы вычислимых функций: Сб. переводов / Под ред. В.М.Козмиди-ади и А.А.1$учника. М., 1970. С. 9-49.

5. Дейкстра 3. Дисциплина программирования. М., 1978. 275 с.

6. Кук С.А. Сложность процедур вывода теорем // Кибернетический сботник. Новая серия. М., 1975. Вып. 12. С. 6-15.

7. Лупанов О.В. Об асимптотических оценках сложности управляющих систем // Международный конгресс математиков в Ницце. 1970. М., 1972. С. 162-167.

8. Дупанов О.В. Асимптотические оценки сложности угтравлетцих систем. М., 1984. КГ. с. w

9. Матиясевич Ю.В. Новое докезатольство теоремы, об скспонвн-циально диофантогом предомшлегйш перепиедишх: предикатов // Зап. научн. семинаров Ленкнгр."отд-ния Мат. ин-та им. В.А.Стеклова АН СССР. 1976. Т. ёО. С. 75-92. ■

10. Мейер А.Р. Слабая сингулярная теория второго порядка функции следования не элементарно рекурсивна // Кибернетический сборник. Новая серия. М., 1975. Вып. 12. С. 62-77.

11. Нечипорук Э.И. О реализации дизъюнкции и конъюнкции в некоторых монотонных базисах // Проблемы кибернетики. М., 1970. Вып. 23. С. 291-293.

12. Нигматуллин Р.Г. Сложность булзв^''$$нкц..й. Казань, 1983. 208 с. ''"""

13. Порецкий П.С. О способах решения логических равенств и обратном способе математической логики. Казань, 1884. 170 с.

14. Слисенко А.О. Упрощенное доказательство распознаваемости симметричности слов в реальное время на машинах Тьюринга//

Зал; научн. семинаров Денкнгр. отд-ния Мат. ин-та им. В.А. Стеклова АН СССР. 1977. Т.68. С. 123-139. 5. Таутс А, Решение логических уравнений типа высказываний // Труды Ш-та физики и астрономии АН ЭССР. Тарту, 1963. Т.20. С. 3-13.

5. Черч А. Введение в математическую логину. М., I960. 484 с. ?. Яблонский С.В. Обзор некоторых результатов в области дискретной математики // Всесозззная нонф." но проблемам теорет. киберн.: Инфсрм. материалы. 5(42) / Научный совет по ковд-лексной проблеме "Кибернетика". Н., 1970. С.-.0-15. , ■ Яблонский С.В. Основные понятия кибернетики /&Цк&яеш " кибернетики. 1959. Вып. 2. С. 7-38. ■ .

>. Янов Ю.И. О лок&яьпых преобразованиях схем алгоритмов. // Проблемы кибернетики. М., 1968. Вып. 20. С. Adaohl 4e, Iwata S«» Kasai Т. Sens ocaMnatiom.l, ргоЫеиз require _i"2. (n51) time // J. Aaaoo. for "Cocp., . Ilaob. 1284. Vol. 31, Ho. 2, P. 361-376. . Mleaan Ь., Handera Й. The ooEpuiatlenal ooraplexity of uo-oialon procedures for polinomiala // Proo. 15th Aim. 12SS . Symp. on Sound, of Сошр. Soi. Ней York, 1975. P. 169-177. . Cook 3.A. L hierarchy for nondetermlnistie time оoaplaxity // J. of Сотр. and Syet. Sol. 1973. Vol. 7, Ho. 4. P. 343-353.

0 Cook 2.4. An overview of computational complexity // Сошзшн. Assoc. for Соир. Maoh. 1983. Yol.26, Bo. 2. P. 401-408.

, O'Donnell iloJ. Computing in systems described Ъу equations // Lecture notes in computer aoienoe. Berlin, 1977. Vol. 58. 111p.

1 Budeanu 3. Boolean functions and equations, tostег<3aai London, 1974. 442 p.

, Stockmeyer L.J. the coaplexity of decision problems in automata theory and logic // MAC leohn. Rep. 133, M.I.2., 1974.

. РАБОТУ АВТОРА ПО ТЕМЕ ДОСЕРТАЩИ

1. Косовский Н.К. О диофаитовых представлешшх последовательности решений уравнений Пелля // Зап. научн. сезсшаров Ленингр. отд-ния Мат. ин-та им. В.А.СтекЛова АН СССР. 1971. Т. 20. С. 49-59.

2.Косовский Н.К. Некоторые свойства решений уравнений в свободной полугруппе // Зап. научн. -семинаров Ленингр. отд-ши Мат. ин-та им. В.А.Стенлова АН СССР. 1972. Т. 32. С. 21-28.

3. Косовский Н.К. 0 решении систем, состоящих одновременно из уравнений в словах и неравенств в длинах слов // Зап. научн. семинаров Ленингр. отд-ния Мат. ш-та им. В.А.Стэкло-ва АН СССР. 1974. Т.40. С. 24-29.

4. Косовский Н.К. Возможности операций одноместного суширо-ваник к одноместного ограниченного умножений // Зап. научн, семинаров Ленингр.- отд-ния Мат. ин-та т. В.А.Сх-ойЛова âH СССР. 1975. Т. 49. С. 3-5. ;

5. Косовский Н.К. 0 разрюикояга булезш ф'тай^адглъкк уравнений // 1У Всесоюзна.:, uciïî зрес-аде со метекгеической гаке: Тезисы докладов к Ккьжшз, 1976.'С, 67.

6. Косовский Н.К. 0 класс?.« <§уахцйЯ, 01^9дадиких';0 помощь» ' сшрацгш суммирования // Вычислительная техника и вопросы" кибернетики. Л., 1978. Вып. 14. С."54-60.

7. Косовский Н.К. Сложность разрешимости булевых функциональных уравнений // Вычислительная техника и вопросы кибернетики. И., 1978. Вып. 15. С. I04-III. ■

8. Косовский Н.К. Эквивалентность правил для доказательства свойств оператора цикла // Вычислительная техшка и вопросы кибернетики. Л. -, 1979. Вып. .Т6..Д, 67-74.

9. Косовский Н.К. Зльмента катзйа^^ьесйой логики п ее .пряло-' кения к теории субрекурСЕК-шх'Ш(Го^1Тмов. Л., 1981. 192 с.

10. Косовский Н.К. Частичная- корректное^ итератявннх процедур кногокра-иаши аннотациям^ V/ ВсесЬязн^коифэрзщкя ,"Сйн-тез, тестирование, верификация и ог.чздт• прогрей,^-®„ Rira, IS8I. С. 132.

11. Косовский H.H. Полиномиальные предзлы эффектззиэации перебора при поиске решений логико-арн'^метагшскизс уравнений // Логика и основания- математики: Тезисы УШ Всесоюзной конференции "Логика и методология науки" (г, Паланга). Вильнюс, 1982. С, 36-39.

12. Косовский H.K. Серш; простых переборных задач с нишами полиномиальными границам» времени ipc решзния // Шестая Всесоюзная конференция по математической логике. Тбилиси, 1982. С. 85. . .

13. Косовский И.К. Частичная корректность в целом.рпещдициро-вашшх утверзденвдмн рекурсивных процедур 6вэ:$$}%ш&троз// Математическая логика и ее применения. Еияыиос/'1983;г Еуп. 3. С. 23-33,

14. Косовский Н.К. Полиномиальные низшие оценки слой^гц; установления разрешимости логано-арифметичсских ураЩоЩЙ IJ Аяаейэз TJalversitatls SieaSlarur. Buflapei/biennia' <}ö ДсЗз^Ъ TOvSje aoaiaatiae , äepsaratuu ssotio cooputato^ica. ВиаьдорК 1933« 4. 2. 67-73*

15. Косовский H.K. Частичная корректность почти з целом прогреми, спедафицированных уа'взрзденияш // ¡11 конференция "Црго'знентй? методов математической логики". Таллин, 1983. С. 138-139.

[6. Косовский Н.К. Логико-аргфгатическао представление неде-терглгалроЕйшшс вычислений // Архитектура и программное оснащение цифровых систем. М., 1984. С. 77-84.

[7. КЬсоеский Н.К. Экспоненциальная нижняя оценка сложности реализации установления разрешимости некоторых уравнений// Седьмая Всесоюзная конференция по математической логике: Тезисы докладов. Новосибирск, 1984, С. 77.

'.в. Косовский Н.К. Примеры простых переборных задач с полиномиальными нижними границами времени их решения // Кибернетика, 1984. № 2. С. I09-II0.

9. Косовский Н.К. Полиномиальная сложность любых схем, реализующих некоторые предикаты, вычислимые на полиномиальной ленте // УП Всесоюзная конференция "Проблемы теоретическое'

кибернетики": Тезисы докладов I часть. Иркутск, 1935. С. 100- 101. ,

20. Виноградов А.К., Косовский Н.К. Иерархия диофантовых пред ставлоний примитивно рекурсивных предикатов // Вычисли тел ная техника и вопросы кибернетики. Л., 1975. Вып. 12.

С. 99-107.

21. Косовский Н.К., Сочилина А.В. Об обучении доказательства!! корректности в целом программ на паскале // Аппаратные и программные средства применения 8ВМ в учебном процессе: Материалы конференции "Применение ЭВМ в вузе". Л., 1984. С. 22-23.

22. Бочернинов В.Я., Косовский Н.К. Исчисление равенств программ модельного языка программирования // Весты. Ланикгр,

. ун-та. 1934. IP 19. С. 5-9.

23. Kcatiovaky П.К. Scmo Giuplc examples of problem тк-itii iare« vable lower bounds // VI International ooajyreae «С Logic, Hethoflolcgi & thiloaophy of 6о1ее.ээ (Abetruets), esg'iioa 1-4, Hacnovor, I1«. 1£5~18Ь* W«

24. Eoacovofcj E.K. А anculeiсjsr-isAet ic C'cxpctfjicc. as e«lvatl? ty of a lcglo-oritkabtl&^l s<j4s,tiaa it Baoia&im jFunsticc Theory» newsletter. 1934, Eo. 31. P.15-16.

УЧАСТОК МНОЖИТЕЛЬНОЙ ТЕХНИКИ В0НЦ AiW СССР

пода« ПЕЧАТИ 24.41.87 Л -4S204 З&СуввТИРАК ICtt