Доказательство свойств функциональных программ методом насыщения равенствами
Аннотация:
Цель работы — исследовать возможность применения комбинации методов насыщения равенствами и многорезультатной суперкомпиляции для выявления и доказательства свойств программ на нестрогом функциональном языке первого порядка. Настоящая работа показывает, что на основе метода насыщения равенствами и преобразований из суперкомпиляции можно построить систему преобразования функциональных программ, применимую для доказательства эквивалентности. Показано, что при этом удаётся избежать проблемы, связанной с комбинаторным взрывом количества функций, отличающихся только порядком аргументов. Также было показано, что можно сформулировать принцип индукции как специальное преобразование, работающее в рамках системы насыщения.
Ключевые слова:
функциональные программы, метод насыщения равенствами, суперкомпиляция, многорезультатная суперкомпиляция
