В курсе теорема перехода 5.2 непосредственно формулируется для формул и позволяет переносить полную систему эквивалентных преобразований между конечными полными базисами. Если τ — конечная полная система тождеств для формул над базисом Б, а Π′ и Π задают взаимное моделирование операций Б в Б′ и Б′ в Б, то после перевода тождеств в Б′ получается конечная полная система для формул над
В обозначениях курса теорема 5.2 утверждает, что система \(\{\Pi'(\tau), \Pi'(\Pi)\}\) является КПСТ в базисе Б′. Таким образом, достаточно уметь реализовать операции одного полного базиса через другой и иметь полную систему в исходном базисе. Для СФЭ этот перенос сочетается с теоремой 5.1 о переходе от формульной КПСТ к
Что важно запомнить
- Б и Б′ предполагаются конечными полными базисами.
- Π′ моделирует операции Б формулами над Б′. Π задаёт обратный
- Каждое тождество τ переводится структурной заменой операций, образуя Π′(τ).
- Теорема 5.2: {Π′(τ),Π′(Π)} — КПСТ для формул над Б′. Для СФЭ далее применяется теорема
- Один односторонний перевод операций недостаточен для доказательства полноты преобразований нового базиса.
Структурное моделирование между базисами
Пусть \(\text{Б}={\varphi_i}\) и \(\text{Б}'={\varphi'_j}\) — два конечных полных базиса. Для каждой операции \(\varphi_i\) выбирают формулу \(\Phi'_i\) над Б′, реализующую ту же функцию. Тождества \(\varphi_i=\Phi'_i\) образуют систему перехода Π′ от Б к Б′. Аналогично строится система Π обратного перехода от Б′ к
Если в формуле F над Б каждую вершину/операцию \(\varphi_i\) заменить соответствующей формулой \(\Phi'_i\), получится формула Π′(F) над Б′. Она реализует ту же функцию. Точно так же переводится тождество t:F₁=F₂: его образом является Π′(t):Π′(F₁)=Π′(F₂). Это и есть структурное моделирование преобразований одного базиса средствами другого.
Формулировка теоремы перехода
Теорема 5.2 курса: если τ — конечная полная система тождеств для формул над Б, а Π′ и Π — системы тождеств перехода между Б и Б′ в обоих направлениях, то \(\{\Pi'(\tau), \Pi'(\Pi)\}\) является конечной полной системой тождеств для формул над
Почему нужен обратный переход
Чтобы преобразовать две произвольные эквивалентные формулы F′₁ и F′₂ над Б′, их сначала с помощью Π моделируют формулами над Б. В исходном базисе полнота τ гарантирует цепочку между полученными моделями. Затем вся цепочка переводится в Б′ системой Π′. Тождества Π′(Π) нужны, чтобы связать исходные формулы Б′ с результатами двойного моделирования. Именно поэтому в итоговой системе присутствуют и переведённые тождества τ, и переведённые тождества обратного
В сочетании с теоремой 5.1 тот же принцип позволяет получать конечные полные системы для СФЭ в других конечных полных базисах: сначала переносится формульная полнота, затем к ней добавляются схемные тождества ветвления и снятия.
Пример простыми словами
Если в новом базисе Б′ операция ∧ реализуется некоторой формулой \(G_{\land}(x,y)\), то при переводе формулы (x₁∧x₂)∨x₃ каждая вершина ∧ заменяется копией G∧. Аналогично заменяются остальные операции. Эквивалентная формула нового базиса имеет другую локальную структуру, но то же функционирование.
Частые ошибки
- Называть теоремой перехода простую замену обозначений операций. Здесь требуется функциональное моделирование операций формулами другого базиса.
- Забывать обратную систему Π. Она нужна, чтобы охватить произвольные формулы нового базиса при доказательстве полноты.
- Смешивать переход между базисами с переходом от формул к СФЭ. Это два разных вида структурного моделирования.
