Эквивалентные преобразования СФЭ обобщают преобразования формул. Подстановка, выделение подсхемы и эквивалентная замена сохраняют систему функций на выходах. Формула рассматривается как частный случай СФЭ, поэтому каждому формульному тождеству t сопоставляется его схемный аналог
Чтобы схемная модель могла точно воспроизводить преобразования формул, к t̄ добавляются специальные тождества ветвления τᴮ и снятия τᶜ. Они позволяют создавать/устранять совместное использование промежуточного результата и удалять структурные части, не влияющие на функционирование. Поэтому любой шаг преобразования формулы по τ можно смоделировать последовательностью преобразований СФЭ по
Что важно запомнить
- Эквивалентность СФЭ означает равенство реализуемых систем ФАЛ.
- Подстановка и замена эквивалентной подсхемы сохраняют функционирование.
- Формульному тождеству t соответствует схемное тождество
- τᴮ задаёт преобразования ветвления результата, а τᶜ снимает висячие функциональные элементы и входы. Совместно τᴮ и τᶜ позволяют устранять внутренние ветвления при переходе к системе формул.
- Формульное преобразование моделируется в СФЭ системой
От формулы к общей схеме
Для произвольного класса схем определения тождества, подстановки, подсхемы и эквивалентной замены переносятся с формул на графовые структуры. Подстановка для СФЭ может переименовывать и отождествлять входные переменные, а также переименовывать, дублировать или снимать выходы. При применении одной и той же подстановки к двум эквивалентным схемам эквивалентность
Схемный аналог формульного тождества
Формулу можно представить как СФЭ-квазидерево. Поэтому тождеству формул t:\(F'=F''\) сопоставляется пара эквивалентных СФЭ, обозначаемая t̄. Однако обычная СФЭ содержит внутренние ветвления, которых в дереве формулы нет, и при моделировании подстановки могут появляться новые общие ветви. Одних формульных тождеств поэтому недостаточно для удобного управления схемной
Тождества ветвления и снятия
Курс вводит для функциональных элементов системы тождеств τᴮ и τᶜ. Первые позволяют структурно организовывать ветвление одного результата к нескольким потребителям. Тождества τᶜ снимают висячие функциональные элементы и висячие входы. Совместное применение τᴮ и τᶜ позволяет устранить внутренние ветвления и висячие вершины, преобразовав СФЭ к системе формул, а затем при необходимости снова перейти к совместному использованию
Моделирование преобразования формулы
Пусть формула F преобразуется в F̂ одним тождеством t после некоторой подстановки. В СФЭ сначала при помощи τᴮ формируют нужные копии/ветвления входов подсхемы, затем применяют схемный аналог t̄, после чего τᶜ удаляет появившиеся лишние ветви. Поэтому любой формульный шаг F⇒F̂ можно реализовать как эквивалентное преобразование СФЭ по системе {t̄,τᴮ,τᶜ}. Для цепочки формульных шагов процедура
Пример простыми словами
Если одна подформула A используется в схеме сразу в двух местах, формульное представление требует двух позиционных вхождений A. Перед применением формульного тождества к одной из копий схемное преобразование может с помощью тождества ветвления организовать нужную локальную структуру, выполнить замену, а затем убрать лишнюю ветвь тождеством снятия.
Частые ошибки
- Считать, что любое формульное тождество можно буквально вставить в произвольный граф без подготовки. В СФЭ нужно учитывать ветвления и подсхемную структуру.
- Путать тождества ветвления с изменением функции. Они меняют способ использования результата, но не выходное функционирование.
- Считать удаление любой внутренней вершины допустимым τᶜ-преобразованием. Удаляемая структура не должна влиять на выходы.
