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

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

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

Пусть A – алгебра с сигнатурой операций S = <s₁, …, s_k> и носителем A. Пусть, далее, X = < x₁, …, x_n > - вектор переменных, которые мы интерпретируем как переменные программы. Для краткости мы будем называть X памятью программы, а векторы a = < a₁, …, a_n>, a_i Î A - состояниями памяти. Множество U = Aⁿобразует пространство - универсум состояний памяти программы. Вычисляющий оператор – это отображение F : U à U, определенное покоординатно системой присвоений

x₁ := f₁(X), …, x_n := f_n(X) (2)

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

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

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

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

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

X := F(X), (4)

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

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

X := F(X), (5)

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

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

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

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

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

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

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

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

, . (6)

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

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

Тогда:

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

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

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

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

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

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

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

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