December 13, 2021
Giulio Manzonetto ( Laboratoire d'Informatique de Paris Nord (LIPN))Turing machines and register machines have been used for
decades in theoretical computer science as abstract models of
computation. However, they are not well-suited for modelling
higher-order computations, because accessing the address of a machine
is not a built-in operation, hence functional machines cannot be
easily passed through their reference. We study a class of abstract
machines that we call “addressing machines” 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. We show that they can be used, for instance, to construct
models of the pure, untyped lambda-calculus. Subsequently, we extend
the syntax of their programs by adding instructions for executing
arithmetic operations on natural numbers, and introduce a reflection
principle allowing certain machines to access their own address and
perform recursive calls. We show that the resulting extended
addressing machines naturally model a weak call-by-name PCF with
explicit substitutions. Finally, we show that they are also well
suited for representing regular PCF programs (closed terms) computing
natural numbers.