Стандартный перевод

С целью обобщения теоремы Салквиста на темпоральную логику применяются преобразования:

1. атомы р переводятся в унарные предикаты р*(х);

2. 1* = 1, 0* = 0;

3. (А)* = (А*);

4. (А & В)* = А* & В*, (А  В)* = А*  В*;

5. ([F]A)* = y(x < y  A*(y)), где y – новая переменная;

6. ([P]A)* = y(x < y  A*(y)), где y – новая переменная;

7. (<F>A)* = y(x < y & A*(y));

8. (<P>A)* = y(y < x & A*(y)).

Рассмотрим темпоральные операции, применяемые при описании программ и в параллельном программировании.

Завтра и вчера

Добавляются одноместные операции T(завтра) и Y(вчера), и новое правило для построения формул:

Если А – формула, то TA и YA – формулы. Семантика в модели M = (Z, <, h):

M, t |= TA, если и только если M, t+1 |= A;

M, t |= YA, если и только если M, t-1 |= A.

Вместо TA применяются также записи Next A, 0A, XA.

Since, Until

Для любых формул А и В добавляются формулы ASB и AUB. Семантика в модели M = (W, <, h):

M, t |= AUB, если и только если для некоторого u > t верно M, u |= B и при всех v, удовлетворяющих соотношениям t < v < u, верно M, v |= A (иными словами, А верно до тех пор, пока не В);

M, t |= ASB, если и только если для некоторого u > t верно M, u |= B, а для всех v, удовлетворяющих соотношениям u < v < t, верно M, v |= A (с тех пор, как случилось В, верно А).

Выбор операторов

Можно сформулировать темпоральную логику для применений одного типа, выбирая отдельные логические связки и темпоральные операторы. Булевы связки &,  и символ 1 включаются всегда.

Примеры

Темпоральная логика FT состоит из формул, построенных из символа 1 и атомов с помощью &, , <F> и Т. Она включает оператор [F], ибо [F] = <F>.

Логика FPTY состоит из формул, построенных из символа 1 и атомов &, , <F>, <P>, T и Y.

Логика US состоит из формул, построенных из символа 1 и атомов с помощью &, , U, S.

В общем случае <F> и <P> невозможно выразить операторы T и Y. Тем не менее, операторы T и Y бывают нужны. Логика US включает формулы из FPTY:

<F>A = 1UA, <P>A = 1SA, TA = 0UA, YA = 0SA.

Стандартный перевод формул логики US основывается на определении:

(B U A)*(x) = y(y > x & A*(y)) & z(x < z < y  B*(x)).

Перевод S определяется симметрично.

Пусть С – класс потоков времени. Темпоральная логика (такая, как FP или US) называется экспрессивно полной относительно С, если для любой формулы первого порядка (х, Р₁, …, Р_n) существует формула А(Р₁, …, Р_n) темпоральной логики, для которой А*(х, Р₁*, …, Р_n*) эквивалентна (х, Р₁*, …, Р_n*) над С. То есть, для любой модели М с потоком времени из С верно:

M |= x (A*(x)  (x)).

Теорема 3 (Кемп). Темпоральная логика US экспрессивно полна над любым классом полных по Дедекинду линейных потоков времени.

Под полным по Дедекинду линейным потоком времени (T, <) понимается линейно упорядоченное множество, в котором нет таких непустых подмножеств X,YT, таких, что

1. X  Y = T;

2. x < y для всех x  X и y  Y;

3. X не имеет наибольшего, а Y – наименьшего элементов.

7. Алгоритмы и рекурсивные функции

Каждый алгоритм имеет входные и выходные данные и состоит из конечного числа инструкций. Например, алгоритм Евклида имеет на входе два положительных числа a и b, на выходе – их наибольший общий делитель. В качестве инструкций можно рассмотреть следующие команды:

1) сравнить a и b;

2) если a равно b, то установить наибольший общий делитель, равным a, и закончить работу;

3) если a > b, то установить a  =  a  –  b и перейти к 1;

если b  >  a, то установить b  =  b  –  a и перейти к 1.

Развитие математики требовало уточнения понятия алгоритма в связи с вопросами алгоритмической разрешимости проблем. Следующие свойства алгоритма были признаны характеризующими его среди методов построения математических объектов:

а) алгоритм состоит из шагов, на каждом из которых формируется система объектов, построенных в предшествующие моменты (дискретность алгоритма);

б) эта система объектов однозначно определяется системой в предшествующие моменты (детерминированность);

в) закон получения последующей системы объектов из предшествующих должен быть простым (элементарность шагов);

г) способ получения объектов на каждом шаге должен давать результаты (направленность);

д) начальная система объектов может выбираться из бесконечного множества (массовость).

Мы рассмотрим алгоритмы, используемые для вычисления значений числовых функций. Такие функции называются вычислимыми.

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