Аппроксимация абстрактных семантик формальными моделями программ

Решение задач анализа и оптимизации вычислительных программ в алгоритмических системах сильно осложняется нерекурсивностью функциональных свойств программ. Согласно теореме Райса в универсальном языке программирования любое свойство программ, зависящее только от вычисляемых ими функций, алгоритмически неразрешимо. Поэтому используется следующий прием. Исходная сложная семантика программ $\sigma$ заменяется более простой семантикой $\omega$ или классом семантик $\Omega$. Если выполнимость некоторого свойства программ в семантике $\omega$, или в каждой из семантик класса $\Omega$, влечет его выполнимость в семантике $\sigma$, то говорят, что семантика $\omega$, или класс $\Omega$, аппроксимирует $\sigma$ относительного заданного программного свойства. Выбрав для заданной семантики $\sigma$ подходящую аппроксимацию, в которой алгоритмически разрешимо исследуемое свойство программ, можно построить эффективную процедуру, частично разрешающую проблему анализа функциональных свойств программ в семантике $\sigma$. Одной из центральных проблем теоретического программирования является проблема функциональной эквивалентности программ, и настоящая статья посвящена изучению вопросов аппроксимации программных семантик относительно этого свойства программ.