Программирование Теоретическое

Математическая дисциплина, изучающая математич. абстракции программ, трактуемых как объекты, выраженные на формальном языке, обладающие определенной информационной и логич. структурой и подлежащие исполнению на автоматич. устройствах. П. т. сформировалось преимущественно на основе двух моделей вычислений: последовательных программ с памятью, или операторных программ, и рекурсивных программ. Обе модели строятся над нек-рой абстрактной алгебраич. системой <D, Ф, П>, образованной предметной областью D, конечным набором (сигнатурой) функциональных и предикатных П= символов с заданным для каждого символа числом его аргументов (арностью). Определение класса программ слагается из трех частей: схемы программы (синтаксиса), интерпретации и семантики. Схема программы — это конструктивный объект, показывающий, как строится программа с использованием сигнатуры и других формальных символов. Интерпретация — это задание конкретной предметной области и сопоставление символам сигнатуры конкретных функций и предикатов (базовых операций), согласованных с предметной областью и арностью символов. Семантика — это способ сопоставления каждой программе результата ее выполнения. Как правило, с программами связывают вычисляемые ими функции. Интерпретация обычно входит в семантику как параметр, поэтому схема программы задает множество программ и вычисляемых ими функций, к-рое получается при варьировании интерпретаций над нек-рым запасом базовых операций. Схема программы с памятью, называемая также алголоподобной, или операторной, схемой, задается в виде конечного ориентированного графа переходов, имеющего обычно одну входную и одну выходную вершины, вершины с одной (преобразователи) и двумя (распознаватели) исходящими дугами. С помощью символов сигнатуры и счетного множества символов переменных и констант обычным образом строится множество функциональных и предикатных термов. Каждому распознавателю сопоставляется нек-рый предикатный терм, а преобразователю — оператор присваивания, имеющий вид y:=t, где у — символ переменной, а t — функциональный терм. Конечная совокупность всех переменных в схеме образует ее память. Интерпретация в дополнение к конкретизации базовых операций предписывает каждой переменной область ее изменения, а каждой константе — ее значение. Для программ с памятью наиболее обычна т. Пусть рассматривается логика Хоара, у к-рой в качестве языка для записи условий взят язык арифметики 1-го порядка. Утверждение о частичной правильности программы наз. выводимым, если оно выводимо в расширении этой логики посредством добавления истинных формул арифметики, и наз. истинным, если оно истинно по отношению к операционной (или денотационной) семантике программы. Логика Хоара наз. состоятельной, если каждое выводимое в ней утверждение истинно, и наз. полной (относительно арифметики), если каждое истинное утверждение выводимо в ней. Состоятельная и полная логика Хоара построена, в частности, для языка программирования, содержащего простые переменные и операторы присваивания, составной, условный, цикла и процедуры (возможно, рекурсивные, но с рядом ограничений) . Важным обобщением логики Хоара является т. н. алгоритмическая (или динамическая) логика. Пусть Q представлено в виде Р [A]Q, где [A]Qесть самое слабое предусловие, для к-рого справедливо утверждение о частичной правильности программы Ас постусловием Q. Аналогично для случая тотальной правильности пусть P<A>Q представлено в виде Р <А>Q. Формулы алгоритмич. логики строятся из формул базового логич. языка (для записи условий) и программ с помощью булевых операций, кванторов, а также операций вида [A]<Q, <А>Q. В алгоритмич. логике выразимы различные утверждения о программах, напр, их эквивалентность. Аналогично логике Хоара для алгоритмич. логики построена состоятельная и полная конечная аксиоматич. система в случае языка программирования, допускающего и недетерминированные программы. Для доказательства утверждений о рекурсивных программах часто используется специальная индукция, связанная с определением н. н. т. Пусть для простоты рекурсивная программа задается одним уравнением f=t(f), а ее денотационная семантика — н. н. т. fH. При естественных предположениях об условии Рсправедлив следующий принцип индукцпи: если формула P(W). истинна и из Р(ti (W)) следует Р(ti+1 (W)), то выполняется Р(fH) (здесь W — нигде не определенная функция). Для описания денотационной семантики языков программирования высокого уровня используется задание области данных в виде т. н. полных решеток Скотта. Задачу синтеза программы можно формализовать как задачу построения доказательства теоремы и последующего извлечения программы из этого доказательства. Построен алгоритм, к-рый по доказательству в интуиционистской логике дает программу на языке алгол-68. Если доказательство использует правило индукции, то ему соответствует в программе цикл вида for to ... do ... od. Извлекаемая программа будет приемлемой сложности, если использовать предположение, что она строится из стандартных (т. е. заданных) функций и предикатов, свойства к-рых описаны аксиомами специального вида. Алгебраическая теория программ. Примером применения алгебраич. методов в П. т. может служить проблема эквивалентности дискретных преобразователей Глушкова, в к-рые естественно вкладываются операторные схемы программ. Пусть — конечный автомат Мили с входным алфавитом Xи выходным алфавитом Y и с заданными начальным и заключительным состояниями. Пусть G — полугруппа с множеством образующих Yи единицей е. Пусть рассматривается автомат Мура Gm, (возможно, бесконечный) с множествами состояний G, входов Y, выходов X, начальным состоянием е, функцией выходов m(g). и функцией переходов q(g, y)=gy. Автомат , работающий совместно с Gm, наз. дискретным преобразователем, если воспринимает в качестве входа выход Gm, а воспринимает в качестве входа выход . Выходом считается при этом состояние Gm в момент остановки . Дискретные преобразователи эквивалентны относительно полугруппы G, если для каждого отображения m из G в Xони оба не останавливаются при работе с Gm либо оба останавливаются с одинаковым выходом. Установлена разрешимость проблемы эквивалентности дискретных преобразователей относительно полугруппы с левым сокращением, неразложимой единицей, в к-рой разрешима проблема тождества слов. Описаны также все разрешимые и неразрешимые случаи эквивалентности дискретных преобразователей относительно коммутативной полугруппы. П. т. оказывает свое влияние на практику прежде всего как концептуальный багаж при изучении программирования и — более технич. путем — через теорию формальных языков программирования. Здесь свойства абстрактных моделей вычислений используются для уточнения семантики языков программирования и для обоснования различных манипуляций с программами (см. Трансляция программ, Программ оптимизирующие преобразования). Лит.:[1] Глушков В. М., Летичевский А. А., в кн.: Избранные вопросы алгебры и логики, Новосиб., 1973, о. 5-39; [2] Ершов А. П., Введение в теоретическое программирование, М., 1977; [3] Котов В. Е., Введение в теорию схем программ, Новосиб., 1978; [4] Лавров С. С., "Программирование", 1978, № 6, с. 3-10; [5] Ляпунов А. А., "Проблемы кибернетики", 1958, в. 1, с. 46-74; [6] Непейвода Н. Н., "Программирование", 1979, М 1, с. 15-25; [7] Плюшкявичюс Р. А.; [и др.], "Кибернетика", 1979, № 2, с. 12-19; [8] Семантика языков программирования. Сб. статей, пер. с англ., М., 1980; [9] Скотт Д., "Кибернетический сборник", 1977, в. 14, с. 107-21; [10] Янов Ю. И., "Проблемы кибернетики", 1958, в. 1, с. 75-127; [11] Manna Z., Mathematical theory of computation, N.Y., — [а.