A Diamond Machine For Strong Evaluation

TL;DR

This paper introduces a new abstract machine for lambda calculus evaluation that avoids backtracking by splitting execution into smaller jobs and incorporates a controlled form of non-determinism called the diamond property.

Contribution

It presents a novel abstract machine design that manages evaluation jobs modularly and supports multiple strategies, including leftmost-outermost evaluation.

Findings

Avoids backtracking in lambda calculus evaluation

Supports multiple evaluation strategies through modular design

Introduces a controlled non-determinism via the diamond property

Abstract

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.