Algoritmos de inversão de programa para programas de ordem superior

10

O termo inversão de programa tem várias tonalidades de significado, mas provavelmente começou com o trabalho de J. McCarthy, de 1956, The Inversion of Functions Defined by Turing Machines no contexto da IA. Até agora, muitas conexões entre inversão de programa e outros campos foram descobertas, por exemplo, programação reversível (física e lógica), avaliação parcial, verificação, programação bidirecional, programação lógica e aprendizado de máquina.

O que é inversão de programa? Em primeira aproximação é algo assim: Dado um programa tomando argumentos do tipo A e retornando resultados do tipo B , produzir um programa P - 1 que é "de alguma forma" o inverso de P . Estou deliberadamente sendo vago aqui, já que o conceito pode ser (e é) esclarecido de várias maneiras: por exemplo, é necessário que P seja injetor? Should P - 1 ( b ) devolver todos ou apenas alguns de uma forma que P ( a ) = bP:ABABP1PPP1(b)aP(a)=b?

Existem maneiras genéricas de inverter um programa, por exemplo, usando a diagonalização, como já indicado por McCarthy, ou usando a avaliação parcial, mas elas tendem a não ser eficientes. Além disso, a maioria dos trabalhos sobre inversão de programas com os quais estou familiarizado não parece lidar com linguagens de programação completas de ordem superior (ou seja, -calculi).λ

Solicitação de referência. Qual é o estado da arte em algoritmos explícitos para inversão de programa de calculi (sem restrição de ordem superior)?λ

Martin Berger
fonte

Respostas:

5

Não houve uma quantidade enorme de trabalho neste espaço, mas o que existe é bastante interessante.

  1. Torben Mogensen trabalhou neste problema. Aqui estão dois documentos dele.

    O primeiro artigo fornece um algoritmo para programas funcionais de primeira ordem e o segundo o estende para uma ordem superior. A caracterização precisa de quando esse algoritmo será bem-sucedido é deixada para trabalhos futuros.

  2. Tetsuo Yokoyama, Holger Bock Axelsen e Robert Glück.

    Isso descreve a linguagem de programação RFun, que inverte programas funcionais de primeira ordem, mas impõe restrições de injetividade e determinismo reverso que garantem que a avaliação reversa seja tão rápida quanto a avançada. (Eles escreveram vários outros artigos sobre esse assunto, sobre os quais tive problemas.)

  3. Stefan Bohne e Baltasar Trancón Widemann.

    Este é um papel realmente limpo! Ele observa que (a) você pode construir uma categoria em que os morfismos são funções emparelhadas com suas inversas (para qualquer noção particular de inversa que você esteja usando) e (b) essa categoria possui uma estrutura compacta de punhal. Isso significa que você pode escrever um programa com uma disciplina do tipo linear levemente descolada e depois ler as interpretações para frente e para trás da semântica.

    Eles fornecem uma linguagem funcional com uma sintaxe bastante selvagem: expressões quase arbitrárias podem ser usadas como padrões, e a reversibilidade a torna sensata.

  4. Nobuko Yoshida, Francesco Tiezzia

    Eu não li este, mas só o descobri quando pesquisava no Google para os outros jornais. Dado os autores e o assunto, suspeito que esse seja o seu caminho!

Neel Krishnaswami
fonte
Obrigado. (2, 3, 4) não fazem inversão de programa, mas projetam linguagens de programação em que os programas são reversíveis / invertíveis por definição. Esse é um problema intimamente relacionado, mas diferente. Na verdade, não sou totalmente claro sobre como esses problemas se relacionam. Eu não tinha visto semi-inversão antes, talvez já resolva o problema, pois a inversão parece ser um caso extremo de semi-inversão? O segundo artigo da BTW Mogensen sobe apenas para a 2ª ordem.
Martin Berger
@ MartinBerger: Eu acho que o relacionamento depende do que você deseja usar para a inversão do programa! Interessei-me pelo problema porque estava analisando a inferência de tipo (se você tiver funções no nível de tipo, é útil poder inverter essas funções para descobrir instanciações quantificadoras) e, portanto, restringir o idioma não foi um empecilho para o show. mim. O que você está tentando fazer?
Neel Krishnaswami
No momento, estou interessado no problema geral e abstrato. Meu interesse na inversão de programas vem da verificação de programas. E não consegui encontrar nenhum lugar que simplesmente pegue um termo lambda (do PCF ou STLC) e o inverta. É porque eu não estou procurando no lugar certo?
Martin Berger