Блог

Насколько я понимаю, следующая строка кода эффективно добавляет тот факт, что r12 = r0 к «среде», в которой Z3 попытается выполнить ограничения во время проверки типов:

prval () = is_fun(pf12, pf0)

Неверно ли думать, что это фактически уменьшает количество ограничений, потому что применение r12 = r0 может позволить решателю доказать, что два ранее уникальных ограничения теперь эквивалентны? И, как только мы достаточно уменьшим количество ограничений, индуктивная гипотеза вместе с нашим базовым вариантом (примерами) обеспечит оставшуюся часть решения?

Я пытаюсь получить общее представление о том, что происходит за кулисами, чтобы помочь понять, как создавать доказательства в функциональном программировании.

Я бы сказал, что это добавляет дополнительную информацию, которую решатель ограничений может использовать для решения ограничений (генерируется в соответствующей области, где доступна эта новая информация).