Algorytmy inwersji programów dla programów wyższego rzędu

Termin inwersja programu ma wiele odcieni znaczenia, ale prawdopodobnie zaczął się od pracy J. McCarthy'ego z 1956 r. Inwersja funkcji zdefiniowanych przez maszyny Turinga w kontekście sztucznej inteligencji. Do tej pory odkryto wiele połączeń między inwersją programu a innymi polami, np. Programowanie odwracalne (fizyczne i logiczne), częściowa ocena, weryfikacja, programowanie dwukierunkowe, programowanie logiki i uczenie maszynowe.

Co to jest inwersja programu? W pierwszym przybliżeniu jest to coś takiego: Biorąc pod uwagę program biorąc argumenty typu i zwracania wyników typu , produkować program , który jest „jakoś” odwrotność . Celowo jestem tutaj niejasny, ponieważ pojęcie to można (i jest) wyjaśnić na różne sposoby: np. Czy musi być iniekcyjne? Czy należy zwrócić wszystkie, czy tylko niektóre takie, że ?$P : A \rightarrow B$$A$$B$$P^{-1}$$P$$P$$P^{-1}(b)$$a$$P(a) = b$

Istnieją ogólne sposoby odwracania programu, np. Użycie diagonalizacji, jak już wskazał McCarthy, lub częściowa ocena, ale zwykle nie są one skuteczne. Również większość prac nad inwersją programów, które znam, nie dotyczy pełnych języków programowania wyższego rzędu (tj. -calculi).$\lambda$

Wniosek o referencję. Jaki jest stan techniki w jawnych algorytmach do odwracania programu -calculi (bez ograniczeń wyższych rzędów)?$\lambda$

W tej przestrzeni nie było dużo pracy, ale to, co tam jest, jest dość interesujące.

1. Torben Mogensen pracował nad tym problemem. Oto dwa jego artykuły.

   Pierwszy artykuł zawiera algorytm dla programów funkcjonalnych pierwszego rzędu, a drugi rozszerza go na wyższy poziom. Dokładna charakterystyka, kiedy ten algorytm odniesie sukces, pozostawia się do przyszłej pracy.

   • Częściowa inwersja strzeżonych równań
   • Częściowa inwersja parametrów funkcjonalnych

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

   Opisuje to język programowania RFun, który odwraca programy funkcjonalne pierwszego rzędu, ale wymusza ograniczenia iniekcyjne i deterministyczne wstecz, które zapewniają, że ocena wstecz jest tak szybka, jak naprzód. (Napisali wiele innych artykułów na ten temat, z którymi miałem problemy.)

   • W kierunku odwracalnego języka funkcjonalnego.

3. Stefan Bohne i Baltasar Trancón Widemann.

   To naprawdę fajny papier! Zauważa, że ​​(a) możesz skonstruować kategorię, w której morfizmy są funkcjami sparowanymi z ich odwrotnością (dla dowolnego określonego pojęcia odwrotności, której używasz), oraz (b) ta kategoria ma zwartą strukturę sztyletu. Oznacza to, że możesz napisać program z nieco funky dyscypliną typu liniowego, a następnie odczytać interpretacje do przodu i do tyłu z semantyki.

   Dają funkcjonalny język z dość dziką składnią: prawie dowolne wyrażenia mogą być używane jako wzorce, a odwracalność czyni to sensownym.

   • Podejście do uogólnionego odwracalnego programowania funkcjonalnego

4. Francesco Tiezzia, Nobuko Yoshida

   Nie przeczytałem tego, ale odkryłem go dopiero, gdy Googling napisał o innych artykułach. Biorąc pod uwagę autorów i temat, podejrzewam, że to właśnie na twojej drodze!

   • Odwracalny rachunek pi oparty na sesji