Addressing Machines as models of lambda-calculus

TL;DR

This paper introduces addressing machines, a new class of abstract machines manipulating memory addresses, to better model lambda-calculus computation, bridging the gap between traditional machine models and functional programming semantics.

Contribution

It proposes addressing machines as a novel formalism for modeling lambda-calculus, with an operational semantics and a connection to combinatory algebra, extending the theoretical understanding of computation models.

Findings

Addressing machines can be endowed with an operational semantics based on leftmost reduction.

The set of addresses forms a combinatory algebra.

A new rule similar to the ω-rule is introduced to model full untyped lambda-calculus.

Abstract

Turing machines and register machines have been used for decades in theoretical computer science as abstract models of computation. Also the $\lambda$-calculus has played a central role in this domain as it allows to focus on the notion of functional computation, based on the substitution mechanism, while abstracting away from implementation details. The present article starts from the observation that the equivalence between these formalisms is based on the Church-Turing Thesis rather than an actual encoding of $\lambda$-terms into Turing (or register) machines. The reason is that these machines are not well-suited for modelling $\lambda$-calculus programs. We study a class of abstract machines that we call "addressing machine" since they are only able to manipulate memory addresses of other machines. The operations performed by these machines are very elementary: load an address in a register, apply a machine to another one via their addresses, and call the address of another machine. We endow addressing machines with an operational semantics based on leftmost reduction and study their behaviour. The set of addresses of these machines can be easily turned into a combinatory algebra. In order to obtain a model of the full untyped $\lambda$-calculus, we need to introduce a rule that bares similarities with the $\omega$-rule and the rule $\zeta_\beta$ from combinatory logic.