Согласованные свободные интерпретации

Полагают, что интерпретация I и СИ I_h (того же базиса В) согласованы, если для любого логического выражения p справедливо I_h(p) = I(p).

Пусть, например, t = `g(h(h(x)), g(h(x), g(x,a)))`, а интерпретация I₃ совпадает с интерпретацией I₁ из п. 1.2.4 за исключением лишь того, что I(x) = 3. Так как I₃(a) = 1; I₃(g) - функция умножения; I₃(h) - функция вычитания 1; получаемI₃(t) = ((3-1)-1)*((3-1)*(3*1)) = 6.

В этом случае I_hпримера из п. 1.3.2. согласована с только что рассмотренной интерпретацией I₃, а так же с I₂ (рисок 1.3, в), но не согласована с I₁ (рисунок 1.3, б).

Справедливы прямое и обратное утверждения, что для каждой интерпретации I базиса В существует согласованная с ней СИ этого базиса.

Так, например, выше было сказано, что I_h рассмотренного примера не согласована с I₁. Что бы сделать I_h согласованной, необходимо условие Р(t) видоизменить: P(t) = 1, если число функциональных символов в t больше трех, P(t) = 0, в противном случае.

Можно поступить и по другому. Оставить I_h без изменения и согласовать с ней I₁. Для этого необходимо будет заменить I₁(x) = 4, на I₁(x) = 3.

Введем важное вспомогательное понятие подстановки термов, используемое в дальнейшем. Если x₁, …, x_n (n ≥ 0) – попарно различные переменные, t₁, ..., t_n – термы из Т, а p - функциональное или логическое выражение, то через p[t₁/x₁, ..., t_n /x_n] будем обозначать выражение, получающееся из выражения p одновременной заменой каждого из вхождений переменной x_i на терм t_I (i = 1, …, n). Например:

a[y/x] = a, f(x, y)[y/x, x/y] = f(y, x), g(x)[g(x)/x] = g(g(x)), p(x)[a/x] = p(a).

Приведем без доказательства несколько важных утверждений:

Если интерпретация I и свободная интерпретация I_h согласованы, то программы (S, I) и (S, I_h) либо зацикливаются, либо обе останавливаются и I(val(S,I_h)) = val(S,I), т.е. каждой конкретной программе можно поставить во взаимно-однозначное соответствие свободно интерпретированную (стандартную) согласованную программу.

Если интерпретация и свободная интерпретация согласованы, они порождают одну и ту же цепочку операторов схемы.

Теорема Лакхэма – Парка – Паттерсона. Стандартные схемы S₁ и S₂ в базисе В функционально эквивалентны тогда и только тогда, когда они функционально эквивалентны на множестве всех свободных интерпретаций базиса В, т.е. когда для любой свободной интерпретации I_h программы (S₁,I_h) и (S₂,I_h) либо обе зацикливаются, либо обе останавливаются и

val(S₁,I) = {I(val(S₁ I_h)) = I(val(S₂ I_h))} = val(S₂,I).

Стандартная схема S в базисе В пуста (тотальна, свободна) тогда и только тогда, когда она пуста (тотальна, свободна) на множестве всех свободных интерпретаций этого базиса, т.е. если для любой свободной интерпретации I_h программа (S, I_h) зацикливается (останавливается).

Стандартная схема S в базисе В свободна тогда и только тогда, когда она свободна на множестве всех свободных интерпретаций базиса В, т. е. когда каждая цепочка схемы подтверждается хотя бы одной свободной интерпретацией.