Соотношения в множествах семантических отображений и бинарных отношений

Построенная на преобразованиях предикатов семантика вкладывается в семантику двойственных преобразований в множествах функций. Принцип двойственности переносится на бинарные отношения, естественно возникающие при рассмотрении недетерминированных алгоритмов. Исследуется возможность привлечения небулевых, в частности арифметических, инвариантов цикла для анализа алгоритма; с этой же точки зрения рассматривается задача установления завершимости цикла.