一句话：引入刚性资源演算，使 Taylor 展开与广义 species 解释一致，并证明 Böhm 树与 Taylor 展开交换。
本文引入资源演算的一种变体——刚性资源演算。在刚性资源项中，袋内元素的置换与原袋相区别但同构，从而精细区分资源使用的置换结构。该设计的关键在于，使刚性资源演算中的 Taylor 展开与 Fiore 等人提出的广义 species 解释相重合；广义 species 同时推广 Joyal 的组合 species 与 Girard 的 normal functors，并可视为关系语义的 proof-relevant 扩展。作为应用，作者针对一类特定的非确定性演算，证明了 Böhm 树的计算与标准 Taylor 展开可交换。这为资源演算、Taylor 展开与广义 species 语义之间建立了精确对应，并展示了该对应在非确定性计算中的语义应用。
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 proof-relevant extension of the relational model. As an application, we prove the commutation between computing Böhm trees and (standard) Taylor expansions for a particular nondeterministic calculus.