Студопедия

КАТЕГОРИИ:


Архитектура-(3434)Астрономия-(809)Биология-(7483)Биотехнологии-(1457)Военное дело-(14632)Высокие технологии-(1363)География-(913)Геология-(1438)Государство-(451)Демография-(1065)Дом-(47672)Журналистика и СМИ-(912)Изобретательство-(14524)Иностранные языки-(4268)Информатика-(17799)Искусство-(1338)История-(13644)Компьютеры-(11121)Косметика-(55)Кулинария-(373)Культура-(8427)Лингвистика-(374)Литература-(1642)Маркетинг-(23702)Математика-(16968)Машиностроение-(1700)Медицина-(12668)Менеджмент-(24684)Механика-(15423)Науковедение-(506)Образование-(11852)Охрана труда-(3308)Педагогика-(5571)Полиграфия-(1312)Политика-(7869)Право-(5454)Приборостроение-(1369)Программирование-(2801)Производство-(97182)Промышленность-(8706)Психология-(18388)Религия-(3217)Связь-(10668)Сельское хозяйство-(299)Социология-(6455)Спорт-(42831)Строительство-(4793)Торговля-(5050)Транспорт-(2929)Туризм-(1568)Физика-(3942)Философия-(17015)Финансы-(26596)Химия-(22929)Экология-(12095)Экономика-(9961)Электроника-(8441)Электротехника-(4623)Энергетика-(12629)Юриспруденция-(1492)Ядерная техника-(1748)

Теоретические результаты




Инварианты программ

Программы, интерпретированные над алгебрами данных

Пусть A – алгебра с сигнатурой операций S = <s1, …, sk> и носителем A. Пусть, далее, X = < x1, …, xn > - вектор переменных, которые мы интерпретируем как переменные программы. Для краткости мы будем называть X памятью программы, а векторы a = < a1, …, an>, ai Î A - состояниями памяти. Множество U = An образует пространство - универсум состояний памяти программы. Вычисляющий оператор – это отображение F: U à U, определенное покоординатно системой присвоений

x1:= f1(X), …, xn:= fn(X) (2)

Вычисляющий оператор мы будем записывать в векторной форме X:= F(X), а вектор координатных функций (вычислений) – в форме F = <f1, …, fn>. Отметим, что в таких обозначениях вычисляющий оператор интерпретируется как одновременное присвоение вектору переменных значений – правых частей покоординатных операторов присвоений.

Мы будем говорить, что программа P определена линейно (интерпретирована над векторным про­странством), если A – некоторое поле (область целостности), а все ее вычисляющие операторы имеют вид

X:= F*X + b, (3)

где F – линейный оператор, действующий в векторном пространстве U, а b Î U.

Мы будем говорить, что программа P определена полиномиально (интерпретирована над полиномиальным кольцом), если A – некоторое поле (область целостности), а все ее вычисляющие операторы имеют вид

X:= F(X), (4)

гдеfi Î A [X], т.е. многочлены с коэффициентами из A.

Мы будем говорить, что программа P определена рационально (интерпретирована над полем рациональных выражений), если A – некоторое поле, а все ее вычисляющие операторы имеют вид

X:= F(X), (5)

гдеfi Î A (X), т.е. рациональные выражения с коэффициентами из A.

Условия определяются как предикаты в некотором специальном языке L условий. Во всяком случае, этот язык включает предикаты равенства и их отрицания (=, ¹).

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

Многочлен g(X) Î A[X] называется полиномиальным инвариантом программы P, если при любом начальном состоянии памяти a = < a1, …, an>, если программа P завершает работу, для заключительного состояния памяти b выполняется равенство g(b) = 0.

Множество всех полиномиальных инвариантов рационально определенных программ образует радикальный идеал кольца A[X], который мы будем обозначать через .

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

 

Теорема 1. Если ch(A) = 0 и язык условий L включает предикаты равенства и их отрицания (=, ¹), проблема построения базиса в классе линейно определенных программалгоритмически неразрешима.

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

 

, . (6)

 

Основной результат [3] настоящей работы, состоит в следующем:

Теорема 2. Пусть P - программа, интерпретированная над полиномиальным кольцом A[X], и .

Тогда:

а) Проблема принадлежности алгоритмически разрешима.

б) Проблема построения базиса векторного пространства алгоритмически разрешима.

Доказательство. (Индукция по структуре регулярного выражения, представляющего программу)

Пусть все вычисляющие операторы, встречающиеся в программе P, и .

Доказательство утверждения а) будем вести индукцией по структуре редуцированной программы P, т.е. по структуре ее регулярного выражения в сигнатуре (6), в которой вычисляющие операторы – суть атомы .

Пусть w = yj1*yj2**yjk программа, представляющая собою последо­ва­тельность вычисляющих операторов. Мы будем говорить, что w Î P, если P допускает вычисления, описанные w. Mы будем также называть w словом P. Собственно программа P ассоциируется тогда со множеством принадлежащих ей слов (множество слов – это множество всевозможных путей вычислений P).

Введём следующие обозначения. Через g(w), , обозначим многочлен , а через - множество многочленов вида g(w), . Идеал, порожденный множеством , обозначим через .

Мы покажем, что для каждой программы существует и может быть эффективно построено конечное подмножество слов такое, что . Поскольку g - инвариант программы P тогда и только тогда, когда g(w) = 0 для любого , проверка инвариантности g сведётся к проверке равенств g (w) = 0, .

1. (базис индукции) . Тогда .

2. (шаг индукции)

а).

б)

Пусть . Поскольку из следует , где имеем , откудa

(7)

в)

Тогда , где E – обозначение тождественного вычисляющего оператора. Рассмотрим последовательность идеалов:

Поскольку кольцо A[X] нетерово, эта последовательность стабилизируется на некотором номере . Покажем, что - наименьшее натуральное число такое, что

(8)

В самом деле, из (7) следует

поэтому из равенства следуют равенства для любого натурального k, откуда

(9)

Поскольку проблема принадлежности алгоритмически разрешима, формулы (6) - (8) описывают рекурсивный алгоритм построения . Утверждение а) доказано.

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

Пусть . Система равенств определяет систему линейных уравнений над A с неизвестными , фундамен­таль­ная система решений которой задаёт искомый базис .




Поделиться с друзьями:


Дата добавления: 2014-01-20; Просмотров: 339; Нарушение авторских прав?; Мы поможем в написании вашей работы!


Нам важно ваше мнение! Был ли полезен опубликованный материал? Да | Нет



studopedia.su - Студопедия (2013 - 2024) год. Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав! Последнее добавление




Генерация страницы за: 0.023 сек.