Арифметика Пресбургера

Рассмотрим сигнатуру s_Z = (0, 1, +, -, =, <, D ₂, D ₃, …), D_m - одноместный предикатный символ, который при заданном значении m = 2, 3,… интерпретируется следующим образом D_m (x) º «число x делится на m без остатка». Теорию полученной таким образом структуры называют арифметикой Пресбургера.

Шаг 1. Борьба с неравенствами.

Шаг 2. Борьба с пердикатами делимости

Лемма 1. D_m (k x - i) º Ú _{j = 0…( m -1)} [ D_m (kj - i) & D_m (x - j)]

Лемма 2. D_m (x - i) º D_{q 1}(x - i) & D_{q 2}(x - i) & … & D_qn (x - i), где q ₁, q ₂, …, q_n сомножители в разложении числа m в произведение степеней простых попарно различных чисел p ₁, p ₂,…, p_n.

Лемма 3. Предположим, что после таких замен в конституанте встретятся две подформулы вида D_q (x - i) и D_q' (x - i_'), где q = p^a, q_' = p^b - степени одного и того же простого числа p, пусть для определенности a £ b. В таком случае в рассматриваемой конституанте заменяем D_q (x - i) на D_q (i _' - i).

Лемма 4. Китайская теорема об остатках. По остаткам от деления числа на систему попарно взаимно простые числа однозначно восстанавливается остаток от деления на произведение этих чисел.

Шаг 3. Элиминация квантора в конституэнтах

В первом случае имеем $ х [ D_m (x - i) & (s < j x) & (k x < t)]º$ х [ D_jkm (jk x - jki) & (k s < jk x) & (jk x < j t)]

º$ х [ D_jkm (x - jki) & (k s < x) & (x < j t)] º$ х [ D_{m ¢}(x - i¢) & (s¢ < x) & (x < t¢)]

º(s¢ +1 < t¢) & D_m (s¢ +1- i¢) Ú (s¢ +2< t¢) & D_m (s¢ +2- i¢) Ú … Ú (s¢ + m < t¢) & D_m (s¢ + m ¢ - i ¢),

где m¢ = jkm, i¢ = jki, s¢ = k s, t¢ = j t, тем самым переменная x исключена.

Во втором случае

$ х [(s < j x) & (k x < t)]º$ х [(k s < kj x) & (kj x < j t)]º D_jk (x -0) & (ks < x) & (x < jt)] (такой случай уже был)

Машина тьюринга.

Модель памяти – бесконечная в обе стороны лента, разбитая на ячейки. Имеется алфавит А и в любой момент времени в ячейке написан символ из А или пустое слово #. На ленте всегда конечное число букв.

Модель процессора – головка. Указывает на некоторую ячейку.

· напечатать/прочитать один из символов алфавита в обозреваемой ячейке;

· сдвинуть обозревающую головку на одну ячейку влево/вправо;

Модель программы – орграф, вершины которого помечены символом из множества , а дуги символами из множества так, что разным дугам, выходящим из одной вершины, приписаны разные символы. Есть единственная входная и как минимум одна выходная дуга.

В начальный момент головка вычислителя обозревает одну из ячеек ленты. Символ r или l то головка вычислителя сдвигается по ленте на одну ячейку. Если же ей приписан символ из алфавита , то этот символ печатается в обозреваемой ячейке. После того, как выполнено действие, отыскивается выходящая из q дуга, помеченная той буквой, которая находиться в данный момент в обозреваемой ячейке. Продолжаем, пока не выходная дуга. Если такой момент не наступит, то программа работает бесконечно.

Согласно данному описанию, программу можно задать, как набор: П = (Q, A, q ₀, Φ, ψ),

в котором

Q – множество вершин графа,

A – алфавит символов, печатающихся на ленте,

q ₀ – входная вершина (q ₀ Q),

Φ – отображение Q в ,

ψ – частичное отображение A ´ Q в Q,

V_П - множество выходных вершин.

(1) “Если входные данные удовлетворяют входному условию и алгоритм через конечное число шагов завершает работу, то выходные данные удовлетворяют требуемому выходному условию.”

(2) “Если входные данные удовлетворяют входному условию, то алгоритм через конечное число шагов завершает работу.”

Алгоритм, для которого доказано утверждение (1) называется частично правильным или частично корректным. Если же доказаны утверждения (1) и (2) то алгоритм называется правильным или корректным.

Дата добавления: 2015-08-31