Geometry of Resource Interaction — A Minimalist Approach
Abstract
The Resource λ-calculus (RC) is a variation of the λ-calculus, where arguments can be superposed and must be linearly used. Hence it is a model for non-deterministic and linear programming languages, and the target language of the Taylor expansion of λ-terms. In a strictly typed restriction of RC, we study the persistence and we define a Geometry of Interaction that is invariant under reduction, characterises persistence, and counts the addends in normal forms.