Jak kodujesz abstrakcyjny algorytm Lampinga za pomocą kombinacji interakcji?

Kombinatory interakcji były wcześniej proponowane jako cel kompilacji dla rachunku λ. Ten papier implementuje pełny rachunek λ. Wiadomo również, że możliwe jest zoptymalizowanie kodowania sieci interakcji rachunku λ dla podzbioru terminów λ, który jest typowy dla EAL. W tym artykule zaimplementowano ten podzbiór rachunku λ, tłumacząc wyrażenia λ typu EAL na sieci interakcji, które są prawdopodobnie bardziej złożone niż kombinatory interakcji, ponieważ używają nieskończonego alfabetu etykiet do grupowania powielaczy.

Zastanawiam się, czy można połączyć oba wnioski. To znaczy, czy jest jakieś kodowanie algorytmu abstrakcyjnego - to znaczy λ-terminów, które można wpisać w EAL - jako kombinatory interakcji?

Nie znam żadnej implementacji algorytmu Lampinga bezpośrednio w kombinatorach interakcji. Wiem, że obecność etykiet liczb całkowitych jest niezbędną cechą algorytmu Lampinga, nawet dla terminów typowych dla EAL, ponieważ etykiety odzwierciedlają zagnieżdżanie tak zwanych pól wykładniczych w siatkach próbnych, a algorytm Lampinga jest zasadniczo wykonywaniem siatek próbnych wykorzystując geometrię interakcji, co po raz pierwszy zaobserwowali Gonthier, Abadi i Lévy . Zatem kwestia implementacji algorytmu w kombinatorach interakcji sprowadza się do reprezentacji pól wykładniczych w sieciach próbnych za pomocą kombinacji. Tak właśnie zrobili Mackie i Pinto w swoim artykule.

Oczywiście kodowanie Mackie i Pinto odnosi się do wszystkich terminów, które używają pełnych liniowych pól logicznych, podczas gdy terminy typowe dla EAL używają elementarnych liniowych pól logicznych, które są prostsze (są to tak zwane pola funkcyjne$\lambda$). Nie uważam jednak, aby to uproszczenie wywarłoby znaczący wpływ na implementacje kombinatora interakcji. Wynika to z faktu, że skrzynki są funkcją globalną (identyfikują dowolnie duże podsieci, które mają być powielone / usunięte), podczas gdy kombinatory interakcji (jak każdy system sieci interakcji) są całkowicie lokalne (redukcja modyfikuje tylko ograniczone podsieci), więc wyzwaniem jest reprezentowanie takich funkcje globalne lokalnie. Teraz globalne powielanie / usuwanie w EAL jest identyczne jak w pełnej logice liniowej, dlatego nie oczekuję, że implementacja EAL w kombinatorze interakcji radykalnie różni się od tej zaproponowanej przez Mackie i Pinto.