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.

翻译：针对λ演算强求值的抽象机会进入参数并进行回溯，通过一组转换规则从已求值的参数中退出。本文研究一种新型抽象机，通过将机器运行拆分为更小的工作单元（每个参数对应一个工作单元）来避免回溯，并在一个工作完成后直接跳转至下一个任务。通常，抽象机具有确定性并实现确定性策略。本文弱化这一特征，在机器与策略中引入轻量级非确定性——即钻石性质。对于机器而言，这实现了工作的模块化管理且可参数化调度策略。随后我们展示了如何获得多种策略，其中最左最外求值策略是其中之一。