Geometry of resource interaction – A minimalist approach

Carte non disponible

Date(s) - 23/10/2014
11 h 00 min - 12 h 00 min

Catégories Pas de Catégories

The Resource λ-calculus (RC) is a variation of the λ-calculus where arguments can be superposed and must be linearly used, and where reduction introduces formal sums on terms. Hence it is a model for non-deterministic and linear programming languages. But RC is also the target language of Taylor-Ehrhard expansion of λ-terms, a linearisation of the usage of arguments. In a strictly typed restriction of RC, we study the notion of paths on proof-nets and the property of persistency. We define a Geometry of Interaction (GoI) that is invariant under reduction, consequently characterises path persistency, and also accurately counts the number of addends being superposed in normal forms. This work intend to be the first step toward an higher destination: understanding and explicitly describing the relation between expansion and GoI.


Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange