Unique decomposition categories, Geometry of Interaction and combinatory logic
Esfandiar Haghverdi · Mathematical Structures in Computer Science · 2000
In another paper (Abramsky et al. 1999), we have developed Abramsky's analysis of Girard's Geometry of Interaction programme in detail. In this paper, our goal is to study the data ow based computational aspects of that analysis. We introduce unique decomposition categories that provide a suitable categorical framework for such computational analysis. The current study also serves to establish connections with the work on proof nets and paths by Girard and Danos and Regnier in this categorical setting. The latter goal is partially achieved here by the presentation of categorical models for dynamic algebras.