通过代数效应构建动态线程的等式公理化：有限关系上的紧致态射、标记偏序和参数化代数理论
An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
AI总结：
本文通过代数效应为动态线程提供等式公理化，结合参数化代数理论构建并发编程语言的语义模型。
摘要：
我们利用代数效应的理论，为动态线程提供一个完整的等式公理化。我们的方法基于参数化代数理论，为函子范畴上的强monad提供具体的语法，并为名称和绑定提供便利的框架。我们的程序由关键的原始操作符'fork'和'wait'构建。'Fork'创建一个子线程并将其名称（线程ID）传递给父线程。'Wait'允许我们等待给定的子线程完成。我们提供了一个由fork和wait构建的参数化代数理论，以及基本的原子操作和定律，如'fork'的结合律。我们的等式公理化在两个意义上是完整的。首先，对于闭合表达式，它完全捕捉了标记偏序（pomsets）的相等性，这是并发的已知模型：模型完整。其次，任何两个开放表达式在所有闭合替换下相等时，它们在语法上是完整的。代数效应的好处是语义分析可以专注于fork和wait的代数操作。然后，我们通过提供操作语义和指称语义将分析扩展到一个简单的并发编程语言。指称语义是通过参数化代数理论的方法构建的，并且我们证明它在标记-偏序观察上是准确的、充分的和完全的。
英文摘要：
We use the theory of algebraic effects to give a complete equational axiomatization for dynamic threads. Our method is based on parameterized algebraic theories, which give a concrete syntax for strong monads on functor categories, and are a convenient framework for names and binding. Our programs are built from the key primitives `fork' and `wait'. `Fork' creates a child thread and passes its name (thread ID) to the parent thread. `Wait' allows us to wait for given child threads to finish. We provide a parameterized algebraic theory built from fork and wait, together with basic atomic actions and laws such as associativity of `fork'. Our equational axiomatization is complete in two senses. First, for closed expressions, it completely captures equality of labelled posets (pomsets), an established model of concurrency: model complete. Second, any two open expressions are provably equal if they are equal under all closing substitutions: syntactically complete. The benefit of algebraic effects is that the semantic analysis can focus on the algebraic operations of fork and wait. We then extend the analysis to a simple concurrent programming language by giving operational and denotational semantics. The denotational semantics is built using the methods of parameterized algebraic theories and we show that it is sound, adequate, and fully abstract at first order for labelled-poset observations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
