超越单子与双积：直觉主义逻辑中并行性的统一解释

传统方法通常依赖单子（如 Moggi 框架）或丰富的范畴结构（如线性逻辑模型中使用的双积）来建模 lambda 演算中的并行性和代数结构。本文提出一种最小化替代方案，在直觉主义命题逻辑框架内捕获并行性和加权并行性（线性组合），而无需使用单子或假设双积的存在。我们引入两个 lambda 演算：一个平行 lambda 演算和一个代数 lambda 演算，均扩展了完整的命题直觉主义逻辑。其语义给出于两个范畴：${\mathbf{Mag}_{\mathbf{Set}}}$，其对象为 magma，态为 $\mathbf{Set}$ 中的函数；以及 ${\mathbf{AMag}^{\mathcal{S}}_{\mathbf{Set}}}$，其对象为作用 magma。所要解决的关键技术挑战是，在平行和代数运算符的存在下解释析取。由于在我们最小化的设置中通常的余并置结构不可用，我们提出一种基于集合论的新解释，基于剩余并置与笛卡尔积的联合。这允许为两个演算构建sound且充分的模型。我们的结果为建模直觉主义逻辑中的并行性和代数效应提供了统一且结构轻量的框架，为超越传统单子或线性逻辑方法的替代方案打开了可能。