Extended Addressing Machines for PCF, with Explicit Substitutions

TL;DR

This paper extends addressing machines with arithmetic and reflection capabilities, demonstrating they can model weak call-by-name PCF with explicit substitutions and represent natural number computations.

Contribution

It introduces extended addressing machines with new instructions and reflection, providing a formal model for PCF with explicit substitutions and natural number computation.

Findings

Modeling of weak call-by-name PCF with explicit substitutions

Representation of natural number computations in extended addressing machines

Formal proof of the extended machines' capabilities

Abstract

Addressing machines have been introduced as a formalism to construct models of the pure, untyped lambda-calculus. 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 prove 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.