Asynchronous effects of Ahman and Pretnar complement the conventional synchronous treatment of algebraic computational 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, multi-party applications, and even a parallel variant of runners of algebraic effects. In this paper, we study the normalisation properties of this calculus. We prove that if one removes general recursion from the original calculus, then the remaining calculus is strongly normalising, including both its sequential and parallel parts. However, this only guarantees termination for very simple asynchronous examples. To improve on this result, we also prove that the sequential fragment of the calculus remains strongly normalising when a controlled amount of interrupt-driven recursive behaviour is reintroduced. Our strong normalisation proofs are structured compositionally as a natural 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.

翻译：Ahman与Pretnar提出的异步效应通过解耦代数运算调用的执行过程——将运算实现的需求发出信号与通过中断运行中的计算并返回运算结果（计算可通过安装匹配的中断处理器进行响应）相结合，从而为代数计算效应提供了基于异步性的补充，超越了传统的同步处理方式。除了为代数效应提供异步性外，所得核心演算还能自然地建模诸如抢占式多线程、（可取消的）远程函数调用、多方应用，甚至代数效应运行器的并行变体等实例。本文研究该演算的正规化性质。我们证明若从原始演算中移除一般递归，则剩余演算（包括其顺序部分与并行部分）具有强正规性。然而，这仅能保证非常简单的异步示例的终止性。为改进此结果，我们还证明了当重新引入受控的中断驱动递归行为时，该演算的顺序片段仍保持强正规性。我们的强正规性证明采用组合式结构，作为Lindley与Stark基于$\top\top$-提升方法证明效应语言强正规性的自然扩展。所有结果均在Agda中进行了形式化验证。