Я буквально недавно наткнулся на статью в википедии
Мёртвый код, там по ссылкам можно походить в связанные статьи, в них упоминаются ссылки на какие-то теоретические (или близкие к теоретическим) публикации. Попробуйте там посмотреть.
Кстати, читал, вещь хорошая.
Только там ссылаются только на книгу Ахо, Сети, Ульман Компиляторы — принципы, технологии, инструменты, 2003. и на книги на инглише, а на него у меня времени и сил мало. А книга Ахо посвящена компиляторам, из теории там только регулярные и КС-языки, остальное приводится как отдельные задачи и решения, это все не имеет ничего общего с тем, что написано в теории схем программ (хотя я только до синтаксического анализа дочитал, м.б. там дальше что-то есть)
https://ru.wikipedia.org/wiki/SSA - например вот это я ниасилил.
И вообще в Вике все выглядит как разрозненный набор задач и трюков, а не как общая теория. С другой стороны, задача удаления всех неиспользуемых переменных и неиспользуемых значений выглядит вполне разрешимой в общем случае.
Есть еще некая теория компиляции - есть она или нет? о чем она? насколько сильна? какая литература?
Еще есть на вид советская Теория вычислительных процессов (например вот:
http://savestud.su/metodichki/82/Teoriy ... sobie.html) - тут даже авторов нет, куча формализма и идея мне пока не видна. Это теория? Она устарела, нет? Что может? Как соотносится с другими теориями?
http://pco.iis.nsk.su/WikiGrapp/%D0%A1% ... 0%BC%D0%BChttps://www.hse.ru/data/2015/12/07/1080 ... %D0%BC.pdf - вот тут есть описание теории схем программ и история. Ничего вообще не понимаю совершенно!
В общем, ничего не вижу, барахтаюсь в пустоте.
О, можно? Было бы неплохо сравнить с внутренними ощущениями.
Только у меня тут немного не так: у меня есть оптимизирующие преобразования, а есть эквивиалентные. Композиция их может порождать оптимизирующее преобразование, которого нет в исходном списке. Я пишу только оптимизирующие преобразования. И они разной степени формализованности.
Язык =
PL/SQL1. Удалить неиспользуемые переменные.
2. Удалить команды, результат которых не используется, но определен.
3. Если в коде переменная инициализирована константой, то можно заменить все вхождения переменной на константу.
4. Если в коде есть одно и то же вычисление >1 раза - вычислить его в переменную и заменить вычисления на переменную.
5. Выражения вида
if A then P1 end if; if A then P2 and if;
if A then P1; P2; end if; при условии, что истинность

после исполнения

не изменилась.
6.
if true then P end if;
P;7.
if false then P end if;
null;8.
Код:
for i in a..b loop
if i <= C then
P
end if;
end loop;

Код:
for i in a..least(b,C) loop
P;
end loop;
(проблемы, когда

опущены)
9. Если для всех
P(i) Q(j) коммутативны, то
Код:
for j in 1..iCnt loop
P;
end loop;
for j in 1..iCnt loop
Q;
end loop;

Код:
for j in 1..iCnt loop
P;
Q;
end loop;
10. Если у множества истинных значений

имеется легкая для вычисления перечисляющая функция

, то дл некоторой функции

Код:
for j in 1..n loop
if P(j) then
C;
end if;
end loop;

Код:
for k in 1..m loop
j := f(k);
C;
end loop;
11. Если в массиве хранятся строки вида

, то достаточно хранить

, остальное вытащить в функцию.