论文标题
协调选择的汇编
Compilation of Coordinated Choice
论文作者
论文摘要
最近，我们提出了协调的选择，这些选择是配备名称的非确定选择。协调选择的主要特征是它们在同名选择之间同步了非确定性决策。 同步机制的动机是解决理论问题。因此，作为一种实用的编程语言，我们仍然希望使用标准选择等协调选择。换句话说，我们希望避免同步。现在，有两个问题：（i）实际上，使用协调的选择编写程序有点复杂，在这种选择中，执行同步从未发生； （ii）从理论上讲，尚不清楚是否只能使用协调的程序来编写任何使用标准选择的程序。 在本文中，我们定义了两个简单地键入的lambda calculi，称为$λ^\并行$，配备了标准选择，配备了配备协调选择的$λ^{\parallowΩ} $，并将前者的汇编规则从前者中提供给后者。挑战是显示汇编的正确性，因为编译前后的表达式之间的行为对应不能直接通过编译规则来定义。对于挑战，我们给出了$λ^{\ParallelΩ} $的效果系统，该效果是表达执行同步永远不会发生的表达式的。然后，我们证明所有汇编的表达式都可以由效果系统键入。结果，我们可以轻松地显示正确性，因为正确性的主要关注点是同步是否发生。
Recently, we have proposed coordinated choices, which are nondeterministic choices equipped with names. The main characteristic of coordinated choices is that they synchronize nondeterministic decision among choices of the same name. The motivation of the synchronization mechanism is to solve a theoretical problem. So, as a practical programming language, we still want to use coordinated choices like standard ones. In other words, we want to avoid synchronization. Now, there are two problems: (i) practically, it is a bit complicated work to write a program using coordinated choices in which execution synchronization never happens; and (ii) theoretically, it is unknown whether any programs using standard choices can be written by using only coordinated ones. In this paper, we define two simply typed lambda calculi called $λ^\parallel$ equipped with standard choices and $λ^{\parallelω}$ equipped with coordinated choices, and give compilation rules from the former into the latter. The challenge is to show the correctness of the compilation because behavioral correspondence between expressions before and after compiling cannot be defined directly by the compilation rules. For the challenge, we give an effect system for $λ^{\parallelω}$ that characterizes expressions in which execution synchronization never happens. Then, we show that all compiled expressions can be typed by the effect system. As a result, we can easily show the correctness because the main concern of the correctness is whether synchronization happens or not.
