Abstract machines for strong evaluation of the $\lambda$-calculus enter into arguments and have a set of transitions for backtracking out of an evaluated argument. We study a new abstract machine which avoids backtracking by splitting the run of the machine in smaller jobs, one for argument, and that jumps directly to the next job once one is finished. Usually, machines are also deterministic and implement deterministic strategies. Here we weaken this aspect and consider a light form of non-determinism, namely the diamond property, for both the machine and the strategy. For the machine, this introduces a modular management of jobs, parametric in a scheduling policy. We then show how to obtain various strategies, among which leftmost-outermost evaluation.

翻译：针对$\lambda$-演算的强求值评估的抽象机会进入论域，并包含一组用于在求值完成后回溯的转换规则。本研究提出一种新型抽象机，通过将机器运行拆分为更小的任务单元（每个论域对应一个任务）来避免回溯，并在任务完成后直接跳转至下一任务。传统机器通常具有确定性并实施确定性策略，本文则弱化这一特性，在机器与策略层面均引入一种轻量级非确定性形式——即钻石性质。对机器而言，这实现了基于调度策略参数化的任务模块化管理，并展示了如何衍生出包括最左最外求值在内的多种策略。