| Summary: | This paper introduces a variant of the resource calculus, the rigid resource calculus, in which a permutation of elements in a bag is distinct from but isomorphic to the original bag. It is designed so that the Taylor expansion within it coincides with the interpretation by generalised species of Fiore et al., which generalises both Joyal’s combinatorial species and Girard’s normal functors, and which can be seen as a proofrelevant extension of the relational model. As an application, we prove the commutation between computing B¨ohm trees and (standard) Taylor expansions for a particular nondeterministic calculus.
|
|---|