Полная система тождеств для СФЭ должна позволять преобразовать любую СФЭ в любую эквивалентную ей СФЭ того же класса. Теорема 5.1 связывает эту задачу с формулами: если τ — конечная полная система тождеств для формул над базисом Б, то система \(\{\bar t:t\in\tau\}\cup\tau^B\cup\tau^C\) является конечной полной системой тождеств для СФЭ над
Для стандартного базиса Б₀ из полноты \(\tau_{\text{осн}}\) получается конечная полная система для СФЭ: схемные аналоги основных формульных тождеств вместе с тождествами ветвления и
Что важно запомнить
- КПСТ для СФЭ должна связывать преобразованиями любые две эквивалентные СФЭ.
- Формульная КПСТ переносится в СФЭ через схемные аналоги
- Дополнительно обязательны тождества ветвления τᴮ и снятия τᶜ.
- Теорема 5.1: конечная полнота для формул ⇒ конечная полнота для СФЭ того же базиса.
- Для Б₀ используется система {t̄:
Почему формульной системы недостаточно буквально
СФЭ отличается от дерева формулы возможностью внутренних ветвлений: один вычисленный результат может использоваться несколько раз. Поэтому эквивалентные схемы могут отличаться не только локальными функциональными фрагментами, но и тем, где промежуточный результат раздваивается или где остаются неиспользуемые части. Эти различия должны уметь устранять тождества
Теорема 5.1
Пусть τ — конечная полная система тождеств для эквивалентных преобразований формул над базисом Б. Каждому t∈τ сопоставим схемный аналог t̄, а к ним добавим системы тождеств ветвления \(\tau^B\) и снятия \(\tau^C\). Тогда
\(\{\bar t:t\in\tau\}\cup\tau^B\cup\tau^C\)
является конечной полной системой тождеств для эквивалентных преобразований СФЭ над
Идея доказательства
Сначала при помощи τᴮ и τᶜ произвольную СФЭ можно свести к эквивалентной системе формул: внутренние разветвления раскрываются, висячие или лишние структурные фрагменты снимаются. Затем полнота τ позволяет преобразовать полученную систему формул в формульное представление второй эквивалентной СФЭ. Каждый формульный шаг моделируется схемными тождествами t̄ вместе с τᴮ и τᶜ. Наконец, структурные тождества восстанавливают требуемую графовую организацию второй
Для Б₀={∧,∨,¬} теорема вместе с полнотой \(\tau_{\text{осн}}\) сразу даёт конкретную КПСТ для СФЭ. Важный смысл результата: проблема полноты тождеств для более общего графового класса сводится к уже решённой формульной проблеме плюс конечный набор правил, описывающих разделение и снятие ветвей.
Пример простыми словами
Пусть промежуточный результат \(A\) используется в СФЭ дважды. Тождества ветвления и снятия позволяют временно развернуть такое совместное использование в две позиционные копии, то есть перейти к системе формул. Там применяется нужное формульное тождество из \(\tau\), после чего схемные тождества снова собирают общее вычисление \(A\). Так полнота для формул переносится на графовую структуру СФЭ.
Частые ошибки
- Считать, что \(\tau_{\text{осн}}\) формул сама по себе полна для СФЭ. Графовая модель требует ещё тождеств ветвления и снятия.
- Путать «конечная система тождеств» и «конечное число схем». Теорема говорит о конечном наборе правил преобразования.
- Считать доказательство полноты перебором схем. Оно использует сведение СФЭ к формулам и моделирование формульных преобразований.
