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 persistency and we define a Geometry of Interaction that is invariant under reduction, characterises persistency, and counts the addends in normal forms.