Исправление metar, (текущая версия) :
как статически доказать эквивалентость двух произвольных алгоритмов
Язык программирования, на котором сформулированы эти два алгоритма, имеет какую-то семантику. Ты можешь сформулировать свойство в терминах этой семантики и попробовать доказать. Естественно, после того как ты его сформулируешь, окажется, что его проверка неразрешима в общем случае, «в лоб» жутко неэффективна чуть менее чем во всех конкретных — вот ты и будешь готов к погружению в мир абстрактной интерпретации, симуляций и логик поверх семантики.
как доказать что соотношения множеств входных и выходных данных для этих функций одинаковы (не учитывая переполнение стека для второй) ?
man Hoare logic. Ну или его бородатые статьи про program refinement для последовательных программ, если и так все понятно.
Исходная версия metar, :
как статически доказать эквивалентость двух произвольных алгоритмов
Язык программирования, на котором сформулированы эти два алгоритма, имеет какую-то семантику (вангую потребность читать lecture notes). Ты можешь сформулировать свойство в терминах этой семантики и попробовать доказать. Естественно, после того как ты его сформулируешь, окажется, что его проверка неразрешима в общем случае, «в лоб» жутко неэффективна чуть менее чем во всех конкретных — вот ты и будешь готов к погружению в мир абстрактной интерпретации, симуляций и логик поверх семантики.
как доказать что соотношения множеств входных и выходных данных для этих функций одинаковы (не учитывая переполнение стека для второй) ?
man Hoare logic. Ну или его бородатые статьи про program refinement для последовательных программ, если и так все понятно.