Je n'ai connaissance d'aucune implémentation de l'algorithme de Lamping directement dans les combinateurs d'interaction. Je sais que la présence d'étiquettes entières est une caractéristique nécessaire de l'algorithme de Lamping, même pour les termes typables EAL, car les étiquettes reflètent l'imbrication de boîtes dites exponentielles dans des réseaux de preuves, et l'algorithme de Lamping est essentiellement l'exécution de réseaux de preuves en utilisant la géométrie de l'interaction, comme l'ont d'abord observé Gonthier, Abadi et Lévy . Ainsi, la question de la mise en œuvre de l'algorithme dans les combinateurs d'interaction se résume à représenter des boîtes exponentielles dans des réseaux de preuve à l'aide des combinateurs. C'est essentiellement ce que Mackie et Pinto ont fait dans leur article.
Bien sûr, l'encodage de Mackie et Pinto s'adresse à tous les -terms, qui utilisent des boîtes logiques linéaires complètes, tandis que les termes typables EAL utilisent des boîtes logiques linéaires élémentaires, qui sont plus simples (ce sont des boîtes dites fonctorialesλ). Cependant, je ne pense pas que cette simplification aurait un impact notable sur les implémentations du combinateur d'interaction. En effet, les boîtes sont une caractéristique globale (elles identifient des sous-réseaux arbitrairement grands à dupliquer / effacer), tandis que les combinateurs d'interaction (comme tout système de réseau d'interaction) sont complètement locaux (la réduction ne modifie que les sous-réseaux bornés), le défi est donc de représenter de tels caractéristiques globales localement. Maintenant, la duplication / effacement global dans EAL est identique à celui de la logique linéaire complète, c'est pourquoi je ne m'attends pas à ce qu'une implémentation de combinateur d'interaction de EAL soit radicalement différente de celle proposée par Mackie et Pinto.
