No conozco ninguna implementación del algoritmo de Lamping directamente en los combinadores de interacción. Sé que la presencia de etiquetas enteras es una característica necesaria del algoritmo de Lamping, incluso para los términos que se pueden escribir EAL, porque las etiquetas reflejan el anidamiento de los llamados cuadros exponenciales en redes de prueba, y el algoritmo de Lamping es esencialmente la ejecución de redes de prueba usando la geometría de interacción, como lo observaron primero Gonthier, Abadi y Lévy . Entonces, la cuestión de implementar el algoritmo en los combinadores de interacción se reduce a representar cuadros exponenciales en redes de prueba usando los combinadores. Esto es esencialmente lo que hicieron Mackie y Pinto en su artículo.
Por supuesto, la codificación de Mackie y Pinto aborda todos los términos , que usan cuadros lógicos lineales completos, mientras que los términos tipificables de EAL usan cuadros lógicos lineales elementales, que son más simples (son los llamados cuadros funcialesλ) Sin embargo, no creo que esta simplificación tenga un impacto notable en las implementaciones del combinador de interacción. Esto se debe a que los cuadros son una característica global (identifican subredes arbitrariamente grandes para duplicar / borrar), mientras que los combinadores de interacción (como cualquier sistema de red de interacción) son completamente locales (la reducción solo modifica subredes limitadas), por lo que el desafío es representar tales características globales a nivel local. Ahora, la duplicación / borrado global en EAL es idéntica a la lógica lineal completa, es por eso que no espero que una implementación del combinador de interacción de EAL difiera radicalmente de la propuesta por Mackie y Pinto.