Алгоритмы инверсии программ для программ высшего порядка

10

Термин « инверсия программы» имеет несколько оттенков смысла, но, вероятно, он начался с работы Дж. Маккарти 1956 года «Обращение функций, определенных машинами Тьюринга в контексте ИИ». К настоящему времени обнаружено множество связей между инверсией программы и другими областями, например, обратимое программирование (физическое и логическое), частичная оценка, верификация, двунаправленное программирование, логическое программирование и машинное обучение.

Что такое инверсия программы? В первом приближении это что - то вроде этого: Учитывая программы принимает аргументы типа и возвращать результаты типа , производят программы , который «как - то» обратный . Я намеренно здесь размываю, поскольку концепцию можно (и можно) уточнить разными способами: например, должен ли быть инъективным? Должен вернуть все или только некоторые такие , что ?п:AВAВп-1ппп-1(б)aп(a)знак равноб

Существуют общие способы инвертирования программы, например, использование диагонализации, как уже указывалось Маккарти, или частичная оценка, но они, как правило, неэффективны. Также большинство работ по инверсии программ, с которыми я знаком, похоже, не имеют дело с полными языками программирования высшего порядка (т.е. -calculi).λ

Справочный запрос. Каково современное состояние явных алгоритмов для программной инверсии -calculi (без ограничения на более высокий порядок)?λ

Мартин Бергер
источник

Ответы:

5

В этом пространстве не было огромного количества работы, но то, что там есть, довольно интересно.

  1. Торбен Могенсен работал над этой проблемой. Вот две его работы.

    Первая статья дает алгоритм для функциональных программ первого порядка, а вторая расширяет его до более высокого порядка. Точная характеристика того, когда этот алгоритм будет успешным, оставлена ​​для дальнейшей работы.

  2. Тецуо Йокояма, Хольгер Бок Аксельсен и Роберт Глюк.

    Здесь описывается язык программирования RFun, который инвертирует функциональные программы первого порядка, но обеспечивает ограничения на приемистость и обратный детерминизм, которые гарантируют, что обратная оценка будет быстрой и прямой. (Они написали ряд других статей на эту тему, которые мне было трудно достать.)

  3. Стефан Бон и Балтасар Транкон Вайдманн.

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

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

  4. Франческо Тиецца, Нобуко Йошида

    Я не читал этот, но только обнаружил это, когда Гуглил для других газет. Учитывая авторов и предмет, я подозреваю, что это прямо в вашем переулке!

Нил Кришнасвами
источник
Спасибо. (2, 3, 4) не делают инверсию программы, но проектируют языки программирования, где программы являются обратимыми / обратимыми по определению. Это тесно связанная, но другая проблема. На самом деле я не совсем понимаю, как эти проблемы связаны. Я не видел полуобращения раньше, может быть, это уже решает проблему, так как инверсия кажется крайним случаем полуобращения? Кстати, вторая работа Могенсена идет только до 2-го порядка.
Мартин Бергер
@MartinBerger: Я думаю, что отношения зависят от того, для чего вы хотите использовать инверсию программы! Я заинтересовался этой проблемой, потому что я смотрел на вывод типа (если у вас есть функции уровня типа, полезно иметь возможность инвертировать эти функции для выяснения реализаций квантификатора), и поэтому ограничение языка не было демонстрацией для меня. Что ты пытаешься сделать?
Нил Кришнасвами
Сейчас меня интересует общая абстрактная проблема. Мой интерес к инверсии программы связан с проверкой программы. И я не мог найти нигде, который просто берет лямбда-термин (скажем, от PCF или STLC) и инвертирует его. Это потому, что я не смотрю в нужном месте?
Мартин Бергер