Geometry of Resource Interaction - A Minimalist Approach

TL;DR

This paper explores the geometry of resource interaction in a linear, non-deterministic lambda calculus variant, introducing a Geometry of Interaction that captures path persistence and counts addends.

Contribution

It defines a Geometry of Interaction for a typed Resource λ-calculus, characterizing path persistence and invariance under reduction, with a novel counting of addends in normal forms.

Findings

Characterizes path persistence in the typed Resource λ-calculus

Introduces a Geometry of Interaction invariant under reduction

Provides a method to count addends in normal forms

Abstract

The Resource $\lambda$-calculus is a variation of the $\lambda$-calculus where arguments can be superposed and must be linearly used. Hence it is a model for linear and non-deterministic programming languages, and the target language of Ehrhard-Taylor expansion of $\lambda$-terms. In a strictly typed restriction of the Resource $\lambda$-calculus, we study the notion of path persistence, and we define a Geometry of Interaction that characterises it, is invariant under reduction, and counts addends in normal forms.