A Fully Abstract Model of PCF Based on Extended Addressing Machines
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2023
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916893191831552 |
|---|---|
| author | Intrigila, Benedetto Manzonetto, Giulio Munnich, Nicolas |
| author_facet | Intrigila, Benedetto Manzonetto, Giulio Munnich, Nicolas |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_13756 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | A Fully Abstract Model of PCF Based on Extended Addressing Machines Intrigila, Benedetto Manzonetto, Giulio Munnich, Nicolas Logic in Computer Science 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. |
| title | A Fully Abstract Model of PCF Based on Extended Addressing Machines |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2306.13756 |