Термин « инверсия программы» имеет несколько оттенков смысла, но, вероятно, он начался с работы Дж. Маккарти 1956 года «Обращение функций, определенных машинами Тьюринга в контексте ИИ». К настоящему времени обнаружено множество связей между инверсией программы и другими областями, например, обратимое программирование (физическое и логическое), частичная оценка, верификация, двунаправленное программирование, логическое программирование и машинное обучение.
Что такое инверсия программы? В первом приближении это что - то вроде этого: Учитывая программы принимает аргументы типа и возвращать результаты типа , производят программы , который «как - то» обратный . Я намеренно здесь размываю, поскольку концепцию можно (и можно) уточнить разными способами: например, должен ли быть инъективным? Должен вернуть все или только некоторые такие , что ?
Существуют общие способы инвертирования программы, например, использование диагонализации, как уже указывалось Маккарти, или частичная оценка, но они, как правило, неэффективны. Также большинство работ по инверсии программ, с которыми я знаком, похоже, не имеют дело с полными языками программирования высшего порядка (т.е. -calculi).
Справочный запрос. Каково современное состояние явных алгоритмов для программной инверсии -calculi (без ограничения на более высокий порядок)?