При преобразовании программ, манипулирующих строками, часто возникает проблема поиска решений уравнений в словах.
Пусть дана следующая функция F, рекурсивно реализующая некоторый предикат на множестве слов.
x,y -- строковые переменные, A - константа алфавита.
F(xAx) = F(x);
F( ) = True;
F(y) = False;
Пусть требуется исследовать свойства этого предиката на множестве слов вида zz, где z - параметр, пробегающий все слова в алфавите, и упростить данное определение. При попытке сопоставления параметризованного слова zz с аргументом первого правила определения функции F возникает уравнение xAx = zz, выполнимость которого при некотором z является необходимым и достаточным условием успешного сопоставления.
Если стоит задача автоматической верификации некоторого свойства программы либо её оптимизации, то уравнения могут быть введены алгоритмом преобразования, перед которым стоит эта задача. Например, если алгоритм преобразования объявляет параметризованные выражения A F(x) и F(y) частными случаями выражения w F(v), получаемыми подстановками w -> A | EMPTY, v -> x | y (где EMPTY - пустое слово), и затем работает уже с выражением w F(v) как обобщением двух рассмотренных выражений, полезным окажется уточнение, что в каждом из частных случаев этого выражения выполняется уравнение Aw =wA.
Суперкомпиляция - это метод преобразования программ, основанный на развёртке дерева параметризованных состояний программы и существенно использующий алгоритмы сопоставления параметризованных данных и их обобщения. В докладе будут рассмотрены некоторые возможности модельного суперкомпилятора MSCP, позволяющие ему оперировать уравнениями в словах и использовать их в данных алгоритмах.