异步效果的强归约
Strong Normalisation for Asynchronous Effects
AI总结：
本文研究了异步效果核心算法规则的强归约性质，证明去除一般递归后仍强归约，且在引入受控中断递归行为时仍保持强归约。
摘要：
Ahman和Pretnar的异步效果补足了传统同步处理代数效果的方式，基于解耦代数操作调用的执行，将其分为信号操作实现需执行和中断正在进行的计算并用操作结果中断，计算可安装匹配中断处理程序。除了为代数效果提供异步性，所得到的核心算术还自然建模如预emptive多线程、(可取消)远程函数调用和多方应用。本文研究该算术的归约性质。我们证明如果移除一般递归，则剩余的算术是强归约的，包括其顺序和并行部分。为覆盖更多有趣的程序，我们还证明当重新引入受控量的中断驱动递归行为时，算术的顺序部分仍保持强归约。我们的归约证明是结构化地作为Lindley和Stark的$\top\top$-lifting方法的扩展来证明效果语言的强归约。所有结果均在Agda中形式化。
英文摘要：
Asynchronous effects of Ahman and Pretnar complement the conventional synchronous treatment of algebraic effects with asynchrony based on decoupling the execution of algebraic operation calls into signalling that an operation's implementation needs to be executed, and into interrupting a running computation with the operation's result, to which the computation can react by installing matching interrupt handlers. Beyond providing asynchrony for algebraic effects, the resulting core calculus also naturally models examples such as pre-emptive multi-threading, (cancellable) remote function calls, and multi-party applications. In this paper, we study the normalisation properties of this calculus. We prove that if one removes general recursion from it, then the remaining calculus is strongly normalising, including both its sequential and parallel parts. To cover more interesting programs, we also prove that the sequential part of the calculus remains strongly normalising when a controlled amount of interrupt-driven recursive behaviour is reintroduced. Our normalisation proofs are structured compositionally as an extension of Lindley and Stark's $\top\top$-lifting-based approach for proving strong normalisation of effectful languages. All our results are also formalised in Agda.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
