A Fully Labelled Lambda Calculus: Towards Closed Reduction in the Geometry of Interaction Machine

We investigate the possibility of performing new reduction strategies with the Geometry of Interaction Machine (GOIm). To this purpose, we appeal to Lévy's labelled lambda calculus whose labels describe: a) the path that the GOIm will follow in the graph of a term and b) the operations that the GOIm requires to compute the multiplicative part from the Multiplicative and Exponential Linear Logic encoding that the machine uses. Our goal is to unveil the missing exponential information in the structure of the labels. This will provide us with a tool to talk about strategies for computing paths with the GOIm.