A Fully Abstract Model of PCF Based on Extended Addressing Machines
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.
Keywords
Cite
@article{arxiv.2306.13756,
title = {A Fully Abstract Model of PCF Based on Extended Addressing Machines},
author = {Benedetto Intrigila and Giulio Manzonetto and Nicolas Munnich},
journal= {arXiv preprint arXiv:2306.13756},
year = {2025}
}
Comments
arXiv admin note: text overlap with arXiv:2212.11147