A Strong Distillery

TL;DR

This paper introduces a new abstract machine for strong evaluation of lambda-terms, specifically for leftmost-outermost evaluation to normal form, with proven correctness, completeness, and linear overhead, enhancing understanding of implementation strategies in proof assistants.

Contribution

It presents the Strong Milner Abstract Machine, a novel variant of the KAM for strong evaluation, with a detailed analysis of its properties and overhead, and introduces a decoding method into the Linear Substitution Calculus.

Findings

The machine is correct and complete for leftmost-outermost evaluation.

Overhead is linear in steps and initial term size.

Features backtracking phases and their interactions with abstractions.

Abstract

Abstract machines for the strong evaluation of lambda-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard micro-step strategy for explicit substitutions, namely linear leftmost-outermost reduction, i.e., the extension to normal form of linear head reduction. Additionally, the overhead of the machine is shown to be linear both in the number of steps and in the size of the initial term, validating its design. The study highlights two distinguished features of strong machines, namely backtracking phases and their interactions with abstractions and environments.