A Fully Abstract Model of PCF Based on Extended Addressing Machines

TL;DR

This paper proves that extended addressing machines (EAMs) precisely model PCF's operational semantics, establishing full abstraction by showing their equivalence and definability correspondence.

Contribution

It demonstrates that EAMs can fully and accurately represent PCF computations, establishing a fully abstract model through equivalence and definability results.

Findings

EAMs simulate PCF with exact termination behavior

The model of PCF via EAMs is adequate and fully abstract

Every EAM can be transformed into an equivalent PCF program

Abstract

Extended addressing machines (EAMs) have been introduced to represent higher-order sequential computations. Previously, we have shown that they are capable of simulating -- via an easy encoding -- the operational semantics of PCF, extended with explicit substitutions. In this paper we prove that the simulation is actually an equivalence: a PCF program terminates in a numeral exactly when the corresponding EAM terminates in the same numeral. It follows that the model of PCF obtained by quotienting typable EAMs by a suitable logical relation is adequate. From a definability result stating that every EAM in the model can be transformed into a PCF program with the same observational behavior, we conclude that the model is fully abstract for PCF.