Linear logic admits a wide range of semantic presentations reflecting its resource-sensitive notion of consequence. One well-known example is phase semantics: an algebraic semantics in which formulas are interpreted in phase spaces, consisting of a commutative monoid and a fixed subset, with respect to which an orthogonality relation is defined. A rather different and much more recent approach is given by base-extension semantics, which defines validity by inductively extending a provability relation on a base -- a set of inference rules over atomic propositions. We establish an equivalence between the two semantics by first defining bidirectional maps between bases and phase spaces, and then constructing an isomorphism between a phase space (resp. base) and its image under the composition of these maps. As a further contribution, we define the base-extension semantics clauses for the exponentials of linear logic.
翻译:线性逻辑因其对资源敏感的蕴涵概念而具有广泛的语义表示。一个著名例子是相位语义:一种代数语义,其中公式在相位空间中解释,该空间由交换幺半群和固定子集构成,并据此定义正交关系。另一种截然不同且更近期的方法是基扩张语义,它通过归纳扩张基础(即原子命题上的推理规则集)上的可证关系来定义有效性。我们首先定义基础与相位空间之间的双向映射,然后构建相位空间(或基础)与其在这些映射复合下的像之间的同构,从而建立两种语义之间的等价性。作为进一步贡献,我们还定义了线性逻辑指数运算的基扩张语义子句。