Non-Deterministic Abstract Machines

We present a generic design of abstract machines for non-deterministic programming languages such as process calculi or the lambda calculus with full non-deterministic \(β\) -reduction. Such a machine traverses a term in the search for a redex, making non-deterministic choices when several paths are possible and backtracking when it reaches a dead end, i.e., an irreducible subterm. The search is guaranteed to terminate thanks to term annotations the machine introduces along the way. We show how to automatically derive a non-deterministic abstract machine from a zipper semantics—a form of structural operational semantics in which the decomposition process of a term into a context and a redex is made explicit. The derivation method ensures the soundness and completeness of the machines w.r.t. the zipper semantics. Zipper semantics themselves can be generated from a reduction semantics, a format commonly used to describe the semantics of sequential languages, in particular effectful ones.