On the equivalence of different presentations of Turner's bracket abstraction algorithm

TL;DR

This paper clarifies the relationships between different versions of Turner's bracket abstraction algorithm, demonstrating their equivalence in translating beta-normal form lambda-terms, thus resolving ambiguities and misconceptions in prior interpretations.

Contribution

It provides a formal comparison of various presentations of Turner's algorithm and establishes their equivalence in a specific context, clarifying ambiguities in the original and subsequent descriptions.

Findings

Some formulations of Turner's algorithm are equivalent for beta-normal form lambda-terms.

The paper resolves ambiguities and misconceptions about the algorithm's definitions.

Clarifies the relationship between different presentations of the algorithm.

Abstract

Turner's bracket abstraction algorithm is perhaps the most well-known improvement on simple bracket abstraction algorithms. It is also one of the most studied bracket abstraction algorithms. The definition of the algorithm in Turner's original paper is slightly ambiguous and it has been subject to different interpretations. It has been erroneously claimed in some papers that certain formulations of Turner's algorithm are equivalent. In this note we clarify the relationship between various presentations of Turner's algorithm and we show that some of them are in fact equivalent for translating lambda-terms in beta-normal form.