Если у вас есть две функции, реализующие другой алгоритм сортировки, то можно ли по исходному коду сделать вывод, что они имеют одинаковые внешние свойства? Это означает, что у них обоих будет возможная несортированная последовательность в качестве входных данных и отсортированная последовательность в качестве их выходных данных? Каким образом эти внешние свойства могут быть определены исходным кодом? И как бы вы описали эти внешние свойства? Какие обозначения будут использоваться?
Внешние свойства можно сделать известными, определив их явно, например, в системе типов, но мне интересно, можно ли это сделать неявно. Или как-то теоретически невозможно вывести такую семантику? Меня интересует, возможно ли это для произвольных функций, а не только для алгоритмов сортировки, предполагая, что такие вещи, как функции, всегда останавливаются и не имеют побочных эффектов.
Стоит ли смотреть на денотационную семантику или она не связана?
Я заинтересован в указателях для исследований в этой области и в различных терминах, используемых для описания предмета, которые могут помочь в моем поиске литературы.
Равенство расширений в полных языках программирования Тьюринга вообще неразрешимо, но это не должно помешать вам проверить или фальсифицировать, что любые две конкретные функции экстенсионально равны.
Проверка может происходить во многих формах, например, в теории множеств ZFC, используя операционную семантику. Однако это было бы больно. Если существует денотационная семантика, их также можно использовать, но хорошая денотационная семантика существует только для нескольких языков. Обычно используют программную логику, например логику Хоара , для демонстрации равенства расширений программ. Для этого логика Hoare для языков с функциями обычно требует аксиомы, гласящей, чтое= г⇔ ∀Иксα, е( х ) = г( х ) , при условии, что е а также г являются функциями типа α → β (детали аксиомы variy с деталями выбранного подхода к логике Хоара).
источник
Быстрый ответ (я признаю, что я не тратил много времени ...) Теорема Райса говорит, что для любого нетривиального вопроса неразрешимо сказать, будет ли функция, вычисляемая программой, иметь свойство или нет. Поэтому вопрос здесь неразрешим
источник