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λ). 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.
