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

 

Полагают, что интерпретация 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 в базисе В свободна тогда и только тогда, когда она свободна на множестве всех свободных интерпретаций базиса В, т. е. когда каждая цепочка схемы подтверждается хотя бы одной свободной интерпретацией.

 

---

Дата добавления: 2015-12-20; просмотров: 19; Мы поможем в написании вашей работы!

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

---

---

Мы поможем в написании ваших работ!