Algorithmes d'inversion de programme pour les programmes d'ordre supérieur

Le terme inversion de programme a plusieurs nuances de sens, mais a probablement commencé avec le travail de J. McCarthy de 1956, The Inversion of Functions Defined by Turing Machines dans le contexte de l'IA. À présent, de nombreuses connexions entre l'inversion de programme et d'autres domaines ont été découvertes, par exemple la programmation réversible (physique et logique), l'évaluation partielle, la vérification, la programmation bidirectionnelle, la programmation logique et l'apprentissage automatique.

Qu'est-ce que l'inversion de programme? En première approximation , il est quelque chose comme ceci: Étant donné un programme prenant des arguments de type A et le retour des résultats de type B , produire un programme P - 1 qui est « en quelque sorte » l'inverse de P . Je suis délibérément vague ici, car le concept peut être (et est) clarifié de diverses manières: par exemple, P doit-il être injectif? Faut - P - 1 ( b ) retourner tout ou seulement une partie d' une telle que P ( a ) = $P : A \rightarrow B$$A$$B$$P^{-1}$$P$$P$$P^{-1}(b)$$a$$P(a) = b$?

Il existe des moyens génériques d'inverser un programme, par exemple en utilisant la diagonalisation comme déjà souligné par McCarthy, ou en utilisant une évaluation partielle, mais ils ont tendance à ne pas être efficaces. De plus, la plupart des travaux sur l'inversion de programmes que je connais ne semblent pas concerner les langages de programmation d'ordre supérieur (c'est-à-dire -calculi).$\lambda$

Demande de réference. Quel est l'état de l'art dans les algorithmes explicites pour l'inversion de programme des -calculi (sans restriction sur l'ordre supérieur)?$\lambda$

Il n'y a pas eu énormément de travail dans cet espace, mais quel travail il y a, est assez intéressant.

1. Torben Mogensen a travaillé sur ce problème. Voici deux de ses papiers.

   Le premier article donne un algorithme pour les programmes fonctionnels de premier ordre, et le second l'étend à un ordre supérieur. La caractérisation précise du moment où cet algorithme réussira est laissée aux travaux futurs.

   • Semi-inversion des équations gardées
   • Semi-inversion des paramètres fonctionnels

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

   Cela décrit le langage de programmation RFun, qui inverse les programmes fonctionnels de premier ordre, mais impose des contraintes d'injectivité et de déterminisme en amont qui garantissent que l'évaluation en amont est aussi rapide que vers l'avant. (Ils ont écrit un certain nombre d'autres articles sur ce sujet, que j'ai eu du mal à obtenir.)

   • Vers un langage fonctionnel réversible.

3. Stefan Bohne et Baltasar Trancón Widemann.

   Ceci est un papier vraiment soigné! Il observe que (a) vous pouvez construire une catégorie où les morphismes sont des fonctions appariées avec leur inverse (quelle que soit la notion particulière d'inverse que vous utilisez), et (b) cette catégorie a une structure compacte de poignard. Cela signifie que vous pouvez écrire un programme avec une discipline de type linéaire légèrement funky, puis lire les interprétations avant et arrière de la sémantique.

   Ils donnent un langage fonctionnel avec une syntaxe assez sauvage: des expressions presque arbitraires peuvent être utilisées comme modèles, et la réversibilité le rend sensible.

   • Une approche pour la programmation fonctionnelle réversible généralisée

4. Francesco Tiezzia, Nobuko Yoshida

   Je n'ai pas lu celui-ci, mais je viens juste de le découvrir lors d'une recherche sur Google pour les autres articles. Compte tenu des auteurs et du sujet, je soupçonne que c'est votre affaire!

   • Pi-calcul réversible basé sur la session