# Extended Addressing Machines for PCF,
with Explicit Substitutions

Benedetto Intrigila  Dipartimento di Ingegneria dell’Impresa,
University of Rome “Tor Vergata”, Italy  Giulio Manzonetto  Nicolas Münnich
Univ. USPN, Sorbonne Paris Cité,
LIPN, UMR 7030, CNRS, F-93430 Villetaneuse, France.

###### 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.

###### keywords:

Addressing machines, PCF, explicit substitutions, computational model.

††volume: NN††journal: Electronic Notes in Theoretical Informatics and
Computer Science††thanks: Email<EMAIL_ADDRESS>Partly supported by ANR Project PPS, ANR-19-CE48-0014.††thanks: Partly
supported by ANR JCJC Project CoGITARe, ANR-18-CE25-0001.††thanks: Email:
<EMAIL_ADDRESS>Email<EMAIL_ADDRESS>paris13.fr

## Introduction

Turing machines (TM) and $\lambda$-calculus constitute two fundamental
formalisms in theoretical computer science. Because of the difficulty in
emulating higher-order calculations on a TM, their equivalence on partial
numeric functions is not obtained directly, but rather composing different
encodings. As a consequence, no model of $\lambda$-calculus (_$\lambda$
-model_) based on TM’s has arisen in the literature so far. Recently, Della
Penna et al. have successfully built a $\lambda$-model based on so-called
_addressing machines_ (AM) [11]. The intent is to propose a model of
computation, alternative to von Neumann architecture, where computation is
based on communication between machines rather than performing local
operations. In fact, these machines are solely capable of manipulating the
addresses of other machines—this opens the way for modelling higher-order
computations since functions can be passed via their addresses. An AM can read
an address from its input-tape, store in a register the result of applying an
address to another and, finally, pass the execution to another machine by
calling its address (possibly extending its input-tape). The set of
instructions is deliberately small, to identify the minimal setting needed to
represent $\lambda$-terms. The downside is that performing calculations on
natural numbers is as awkward as using Church numerals in $\lambda$-calculus.

Contents. In this paper we extend the formalism of AM’s with a set of
instructions representing basic arithmetic operations and conditional tests on
natural numbers. As we are entering a world of machines and addresses, we need
specific machines to represent numerals and assign them recognizable
addresses. Finally, in order to model recursion, we rely on the existence of
machines representing fixed point combinators. These machines can be
programmed in the original formalism but we can avoid any dependency on self-
application by manipulating the addressing mechanism so that they have access
to their own address. This can be seen as a very basic version of the
reflection principle which is present in some programming languages. We call
the resulting formalism _extended addressing machines_ (EAMs).

Considering these features, one might expect EAMs to be well-suited for
simulating Plotkin’s Programming Computable Functions (PCF) [23], a simply
typed $\lambda$-calculus with constants, arithmetical operations, conditional
testing and a fixed point combinator. A PCF term of the form $(\lambda x.M)N$
can indeed be translated into a machine $\mathsf{M}$ reading as input ($x$)
from its tape the address of $\mathsf{N}$. As $\mathsf{M}$ has control over
the computation, it naturally models a weak leftmost call-by-name evaluation.
However, while in the contractum $M[N/x]$ of the redex the substitution is
instantaneous, $\mathsf{M}$ needs to pass the address of $\mathsf{N}$ to the
machines representing the subterms of $M$, with the substitution only being
performed if $\mathsf{N}$ gains control of the computation. As a result,
rather than PCF, EAMs naturally emulate the behavior of EPCF—a weak call-by-
name PCF with explicit substitutions that are only performed “on demand”, as
in [19]. We endow EAMs with a typing mechanism based on simple types and
define a type-preserving translation from well-typed EPCF terms to EAMs.
Subsequently, we prove that also the operational behavior of EPCF is
faithfully represented by the translation. Finally, by showing the equivalence
between PCF and EPCF on terminating programs of type $\mathsf{int}$, we are
capable of drawing conclusions for the original language PCF.

In this paper we mainly focus on the properties of the translation, but our
long-term goal is to construct a sequential model of higher-order
computations. The problem of finding a fully abstract model of PCF was
originally proposed by Robin Milner in [21] and is a difficult one. A model is
called _fully abstract_ (FA) whenever two programs sharing the type $\alpha$
get the same denotation in the model if and only if they are observationally
indistinguishable when plugged in the same context $C[]$ of type
$\alpha\to\mathsf{int}$. Therefore, a FA model provides a semantic
characterization of the observational equivalence of PCF. Quoting from [3]:

> “the problem is to understand what should be meant by a semantic
> characterization […] Our view is that the essential content of the problem,
> what makes it important, is that it calls for a semantic characterization of
> sequential, functional computation at higher-types”.

A celebrated result is that FA models of PCF can be obtained by defining
suitable categories of games [4, 3, 13]. Preliminary investigations show that
EAMs open the way to construct a more ‘computational’ FA model. E.g., in [21],
the model construction starts with first-order definable functions and
requires—to cope with fixed point operator—the addition of extra ‘limit
points’ to ensure that the resulting partial order is direct complete. In the
game semantics approach the fixed point operator is treated similarly, namely
via its canonical interpretation in a cpo-enriched Cartesian closed category
[4]. On the contrary, in our approach no limit construction is required to
give the fixed point operator a meaning. The fact that EAMs possess a given
recursor having its own address stored inside is easily obtained from a
mathematical point of view and, as argued above, can be seen as an abstract
view of the usual implementation of recursion. We believe this new point of
view may increase our understanding of PCF observational equivalence.

Outline. The paper is organized as follows. In Section 1 we introduce the
language EPCF along with its syntax, simply typed assignment system and
associated (call-by-name) big-step operational semantics. In Section 2 we
define EAMs (no familiarity with [11] is assumed) and introduce their
operational semantics. In Section 3 we describe a type–checking algorithm for
determining whether an EAM is well-typed. In Section 4 we present our main
results, namely:

  1. (i)

the translation of a well-typed EPCF term is an EAM typable with the same type
(Theorem 4.8);

  2. (ii)

if an EPCF term reduces to a value, then their translations as machines are
interconvertible (Thm. 4.10);

  3. (iii)

the operational semantics of PCF and EPCF coincide on terminating programs of
type $\mathsf{int}$ (Thm. 4.20);

  4. (iv)

the translation of a PCF program computing a number is an EAM evaluating the
corresponding numeral (Theorem 4.22).

Related works. A preliminary version of AMs was introduced in Della Penna’s
MSc thesis [10] in order to model computation as communication between
distinguished processes by means of their addresses. They were subsequently
refined in [11] with the theoretical purpose of constructing a model of
$\lambda$-calculus. Similarly, our paper should be seen as a first step
towards the construction of a denotational model of PCF. Thus, the natural
comparison is111The reader interested in a comparison with other abstract
machines or formalisms is invited to consult [14].  with other models rather
than other machine-based formalisms that have been proposed in the literature
(e.g., call-by-name: SECD [16], KAM [15], call-by-need: TIM [12], Lazy KAM [6,
17]); call-by-value: ZINC [18]) from which they differ at an implementational
level.

Compared with models of PCF based on Scott-continuous functions [21, 5, 7],
EAMs provide a more operational interpretation of a program and naturally
avoid parallel features that would lead to the failure of FA as in the
continuous semantics. Compared with Curien’s sequential algorithms [8] and
categories of games [4, 13] they share the intensionality of programs’
denotations, while presenting an original way of modelling sequential
computation. The model based on AMs also bares _some_ similarities with the
categories of assembly used to model PCF [20], mostly on a philosophical
level, in the sense that these models are based on the ‘codes’ (rather than
addresses) of recursive functions realizing a formula ($\cong$ type).

Concerning explicit substitutions we refer to the pioneering articles [1, 2,
9, 19]. Explicit substitutions have been barely considered in the context of
PCF—with the notable exception of [24].

##  1 Preliminaries

$\begin{array}[]{c}\begin{array}[]{ccc}\sigma\triangleright\underline{n}\Downarrow_{d}\underline{n}\underline{n}\in{\rm
Nature}&\sigma\triangleright\lambda x.M\langle\rho\rangle\Downarrow_{d}\lambda
x.M\langle\sigma+\rho\rangle&\sigma\triangleright
x\Downarrow_{d}V\lx@proof@logical@and\sigma(x)=(\rho,N)\rho\triangleright
N\Downarrow_{d}V\\\\[4.30554pt]
\sigma\triangleright\mathbf{fix}\,M\Downarrow_{d}V\sigma\triangleright
M\cdot(\mathbf{fix}\,M)\Downarrow_{d}V&\sigma\triangleright\mathbf{ifz}(M,N_{1},N_{2})\Downarrow_{d}V_{1}\lx@proof@logical@and\sigma\triangleright
M\Downarrow_{d}\underline{0}\sigma\triangleright
N_{1}\Downarrow_{d}V_{1}&\sigma\triangleright\mathbf{ifz}(M,N_{1},N_{2})\Downarrow_{d}V_{2}\lx@proof@logical@and\sigma\triangleright
M\Downarrow_{d}\underline{n+1}\sigma\triangleright
N_{2}\Downarrow_{d}V_{2}\\\\[4.30554pt]
\sigma\triangleright\mathbf{pred}\,M\Downarrow_{d}\underline{n}\sigma\triangleright
M\Downarrow_{d}\underline{n+1}&\sigma\triangleright\mathbf{pred}\,M\Downarrow_{d}\underline{0}\sigma\triangleright
M\Downarrow_{d}\underline{0}&\sigma\triangleright\mathbf{succ}\,M\Downarrow_{d}\underline{n+1}\sigma\triangleright
M\Downarrow_{d}\underline{n}\end{array}\\\\[43.05542pt] \sigma\triangleright
M\cdot N\Downarrow_{d}V\lx@proof@logical@and\sigma\triangleright
M\Downarrow_{d}\lambda
x.M^{\prime}\langle\rho\rangle\rho+[x\leftarrow(\sigma,N)]\triangleright
M^{\prime}\Downarrow_{d}V\end{array}$

Figure 1: The big-step operational semantics of EPCF.

The paradigmatic programming language PCF [23] is a simply typed
$\lambda$-calculus enriched with constants representing natural numbers, the
fundamental arithmetical operations, an if-then-else conditional instruction,
and a fixed-point operator. We give PCF for granted and rather present EPCF,
an extension of PCF with explicit substitutions [19]. We draw conclusions for
the standard PCF by exploiting the fact that they are equivalent on programs
(closed terms) of type $\mathsf{int}$.

######  Definition 1.1.

Consider fixed a countably infinite set $\mathrm{Var}$ of variables. EPCF
_terms_ and _explicit substitutions_ are defined by (for $n\geq 0$ and $\pol
x\in\mathrm{Var}$):

$\begin{array}[]{lcl}L,M,N&::=&~{}\,x\mid M\cdot N\mid\lambda
x.M\langle\sigma\rangle\mid\mathbf{0}\mid\mathbf{pred}\,M\mid\mathbf{succ}\,M\mid\mathbf{ifz}(L,M,N)\mid\mathbf{fix}\,M\\\
\sigma,\rho&::=&\left[x_{1}\leftarrow(\sigma_{1},M_{1}),\dots,x_{n}\leftarrow(\sigma_{n},M_{n})\right]\end{array}$

As is customary, $M\cdot N$ stands for the _application_ of a term $M$ to its
argument $N$, $\mathbf{0}$ represents the natural number 0, $\mathbf{pred}$
and $\mathbf{succ}$ indicate the predecessor and successor respectively,
$\mathbf{ifz}$ is the conditional test on zero, and finally, $\mathbf{fix}$ is
a fixed-point operator. We assume that application – often denoted as
juxtaposition – associates to the left and has higher precedence than
abstraction. Concerning $\lambda x.M\langle\sigma\rangle$, it represents an
_abstraction_ where $\sigma$ is a list of assignments from variables to
_closures_ (terms with the associated substitutions), where each variable can
only have one closure assigned to it.

######  Definition 1.2.

  1. (1)

In an explicit substitution

$\sigma=[x_{1}\leftarrow(\sigma_{1},M_{1}),\dots,x_{n}\leftarrow(\sigma_{n},M_{n})]$

the $x_{i}$’s are assumed to be fresh and distinguished.

  2. (2)

By (i), we can define $\sigma(x_{i})=(\sigma_{i},M_{i})$.

  3. (3)

The _domain_ of $\sigma$ is given by
$\mathrm{dom}(\sigma)=\\{x_{1},\dots,x_{n}\\}$.

  4. (4)

We write $\sigma+\rho$ for the concatenation of $\sigma$ and $\rho$, and in
this case we assume $\mathrm{dom}(\sigma)\cap\mathrm{dom}(\rho)=\emptyset$.

The set $\mathrm{FV}(M)$ of _free variables_ of an EPCF term $M$ is defined as
usual, except for the abstraction case $\mathrm{FV}(\lambda
x.M\langle\sigma\rangle)=\mathrm{FV}(M)-(\\{x\\}\cup\mathrm{dom}(\sigma))$.
The term $M$ is _closed_ if $\mathrm{FV}(M)=\emptyset$, and in that case it is
called an _EPCF program_.

Hereafter terms are considered up to renaming of bound variables. Therefore
the symbol $=$ will denote syntactic equality up to _$\alpha$ -conversion_.

###### Notation 1

  1. (1)

For every $n\in{\rm Nature}$, we let
$\underline{n}=\mathbf{succ}\,^{n}(\mathbf{0})$. In particular,
$\underline{0}$ is an alternative notation for $\mathbf{0}$.

  2. (2)

As a syntactic sugar, we write $\lambda x.M$ for $\lambda x.M\langle\rangle$.
With this notation in place, _PCF terms_ are simply EPCF terms containing
empty explicit substitutions.

  3. (3)

For $n\in{\rm Nature}$, we often write $\lambda x_{1}\dots\lambda x_{n}.M$ as
$\lambda x_{1}\dots x_{n}.M$, or even $\lambda\pol x.M$ when $n$ is clear from
the context. Summing up, and recalling that $\cdot$ is left associative,
$\lambda x_{1}x_{2}x_{3}.L\cdot M\cdot N$ stands for $\lambda x_{1}.(\lambda
x_{2}.(\lambda x_{3}.((L\cdot M)\cdot
N)\langle\rangle)\langle\rangle)\langle\rangle$.

  4. (4)

$M[N/x]$ denotes the capture-free substitution of $N$ for all free occurrences
of $x$ in $M$.

######  Example 1.3.

We introduce some notations for the following (E)PCF programs, that will be
used as running examples.

  1. (1)

$\mathbf{I}=\lambda x.x$, representing the identity.

  2. (2)

$\boldsymbol{\Omega}=\mathbf{fix}\,(\mathbf{I})$ representing the paradigmatic
looping program.

  3. (3)

$\mathbf{succ1}=\lambda x.\mathbf{succ}\,(x)$, representing the successor
function.

  4. (4)

$\mathbf{succ2}=(\lambda sn.s\cdot(s\cdot n))\cdot\mathbf{succ1}$,
representing the function $f(x)=x+2$.

  5. (5)

$\mathbf{add\\_aux}=\lambda
fxy.\mathbf{ifz}(y,x,(f\cdot(\mathbf{succ}\,x))\cdot(\mathbf{pred}\,y))$, i.e.
the functional

$\Phi_{f}(x,y)=\begin{cases}x,&\textrm{if }y=0,\\\ f(x+1,y-1),&\textrm{if
}y>0.\\\ \end{cases}$

  6. (6)

$\mathbf{add}=\mathbf{fix}\,(\mathbf{add\\_aux})$, i.e., the recursive
definition of addition $f(x,y)=x+y$.

The operational semantics of EPCF is defined via a call-by-name big-step
(leftmost) weak reduction.

######  Definition 1.4.

  1. (1)

We let $\mathrm{Val}=\\{\underline{n}\mid n\in{\rm Nature}\\}\cup\\{\lambda
x.M\langle\sigma\rangle\mid M\textrm{ is an {\sf EPCF}{} term}\\}$ be the set
of EPCF _values_.

  2. (2)

The _big-step weak reduction_ is the least relation $\Downarrow_{d}$ from EPCF
terms to $\mathrm{Val}$, closed under the rules of Figure 1.

  3. (3)

We say that an EPCF program $M$ is _terminating_ whenever $M\Downarrow_{d}V$
holds, for some $V\in\mathrm{Val}$. Otherwise, we say that $M$ is a _non-
terminating_ , or _looping_ , term.

######  Example 1.5.

We show some of the terms from Example 1.3, at work.

  1. (1)

We have
$[\,]\triangleright\mathbf{succ1}\cdot\mathbf{0}\Downarrow_{d}\underline{1}$.
To get the reader familiar with the operational semantics, we give the
details:

$[\,]\triangleright(\lambda
x.\mathbf{succ}\,(x))\cdot\underline{0}\Downarrow_{d}\underline{1}\lx@proof@logical@and[\,]\triangleright\lambda
x.\mathbf{succ}\,(x)\Downarrow_{d}\lambda
x.\mathbf{succ}\,(x)[x\leftarrow([\,],\underline{0})]\triangleright\mathbf{succ}\,(x)\Downarrow_{d}\underline{1}[x\leftarrow([\,],\underline{0})]\triangleright
x\Downarrow_{d}\underline{0}[\,]\triangleright\underline{0}\Downarrow_{d}\underline{0}$

  2. (2)

Similarly,
$[\,]\triangleright\mathbf{I}\cdot\underline{4}\Downarrow_{d}\underline{4}$,
$\ [\,]\triangleright\mathbf{I\cdot I}\Downarrow_{d}\mathbf{I}$, $\
[\,]\triangleright\mathbf{succ2}\cdot\underline{1}\Downarrow_{d}\underline{3}$
and
$[\,]\triangleright\mathbf{add}\cdot\underline{5}\cdot\underline{1}\Downarrow_{d}\underline{6}$.

  3. (3)

Since $\boldsymbol{\Omega}$ is looping, there is no $V\in\mathrm{Val}$ such
that $[\,]\triangleright\boldsymbol{\Omega}\Downarrow_{d}V$ is derivable.

We now endow EPCF terms with a type system based on simple types.

######  Definition 1.6.

  1. (1)

The set $\mathbb{T}$ of _(simple) types_ over a _ground type_ $\mathsf{int}$
is inductively defined by the grammar:

$\alpha,\beta\ ::=\ \mathsf{int}\mid\alpha\to\beta$ ($\mathbb{T}$)

The arrow associates to the right, in other words we write
$\alpha_{1}\to\cdots\to\alpha_{n}\to\beta$ for
$\alpha_{1}\to(\cdots\to(\alpha_{n}\to\beta)\cdots)$ ($=\pol\alpha\to\beta$,
for short).

  2. (2)

A _typing context_ $\Gamma$ is given by a set of associations between
variables and types, written $x_{1}:\alpha_{1},\dots,x_{n}:\alpha_{n}$. In
this case, we let $\mathrm{dom}(\Gamma)=\\{x_{1},\dots,x_{n}\\}$. When writing
$\Gamma,x:\alpha$, we silently assume that $x\notin\mathrm{dom}(\Gamma)$.

  3. (3)

_Typing judgements_ are triples, denoted $\Gamma\vdash^{\mathsf{E}}M:\alpha$,
where $\Gamma$ is a typing context, $M$ is an EPCF term and
$\alpha\in\mathbb{T}$.

  4. (4)

_Typing derivations_ are finite trees built bottom-up in such a way that the
root has shape $\Gamma\vdash^{\mathsf{E}}M:\alpha$ and every node is an
instance of a rule from Figure 2. In the rule $(\to_{\mathrm{I}})$ we assume
wlog that $x\notin\Gamma$, by $\alpha$-conversion. We also use an auxiliary
predicate $\sigma\models\Gamma$ whose intuitive meaning is that $\Gamma$ is a
typing context constructed from an explicit substitution $\sigma$.

  5. (5)

When writing $\Gamma\vdash^{\mathsf{E}}M:\alpha$, we mean that this typing
judgement is derivable.

  6. (6)

We say that $M$ _is typable_ if $\Gamma\vdash^{\mathsf{E}}M:\alpha$ is
derivable for some $\Gamma,\alpha$.

$\begin{array}[]{c}\begin{array}[]{cccc}\Gamma,x:\alpha\vdash^{\mathsf{E}}x:\alpha&\Gamma\vdash^{\mathsf{E}}\mathbf{0}:\mathsf{int}&\Gamma\vdash^{\mathsf{E}}\mathbf{fix}\,M:\alpha\Gamma\vdash^{\mathsf{E}}M:\alpha\rightarrow\alpha\\\\[4.30554pt]
\Gamma\vdash^{\mathsf{E}}\mathbf{succ}\,M:\mathsf{int}\Gamma\vdash^{\mathsf{E}}M:\mathsf{int}&\Gamma\vdash^{\mathsf{E}}\mathbf{pred}\,M:\mathsf{int}\Gamma\vdash^{\mathsf{E}}M:\mathsf{int}&\Gamma\vdash^{\mathsf{E}}\lambda
x.M\langle\sigma\rangle:\alpha\rightarrow\beta\lx@proof@logical@and\sigma\models\Delta\Gamma,\Delta,x:\alpha\vdash^{\mathsf{E}}M:\beta\\\\[4.30554pt]
\begin{array}[]{ccc}\Gamma\vdash^{\mathsf{E}}M\cdot
N:\beta\lx@proof@logical@and\Gamma\vdash^{\mathsf{E}}M:\alpha\rightarrow\beta\Gamma\vdash^{\mathsf{E}}N:\alpha\end{array}&&\Gamma\vdash^{\mathsf{E}}\mathbf{ifz}(L,M,N):\alpha\lx@proof@logical@and\Gamma\vdash^{\mathsf{E}}L:\mathsf{int}\Gamma\vdash^{\mathsf{E}}M:\alpha\Gamma\vdash^{\mathsf{E}}N:\alpha\\\
[]\models\emptyset&&\sigma+[x\leftarrow(\rho,M)]\models\Gamma,x:\alpha\lx@proof@logical@and\sigma\models\Gamma\rho\models\Delta\Delta\vdash^{\mathsf{E}}M:\alpha\end{array}\end{array}$

Figure 2: EPCF type assignment system.

######  Example 1.7.

The following are examples of derivable typing judgments.

  1. (1)

$\displaystyle\vdash^{\mathsf{E}}\lambda
x.\mathbf{succ}\,(y)\langle[y\leftarrow([\,],\mathbf{0})]\rangle:\alpha\rightarrow\mathsf{int}[y\leftarrow([\,],\mathbf{0})]\models
y:\mathsf{int}\lx@proof@logical@and[\,]\models\emptyset[\,]\models\emptyset\vdash^{\mathsf{E}}\mathbf{0}:\mathsf{int}y:\mathsf{int},x:\alpha\vdash^{\mathsf{E}}\mathbf{succ}\,(y):\mathsf{int}y:\mathsf{int},x:\alpha\vdash^{\mathsf{E}}y:\mathsf{int}$

  2. (2)

$\vdash^{\mathsf{E}}(\lambda
x.\mathbf{succ}\,(x))\cdot\mathbf{0}:\mathsf{int}$.

  3. (3)

$\vdash^{\mathsf{E}}(\lambda sn.s\cdot(s\cdot n))\cdot(\lambda
x.\mathbf{succ}\,(x)):\mathsf{int}\rightarrow\mathsf{int}$.

  4. (4)

$\vdash^{\mathsf{E}}\mathbf{fix}\,(\lambda
fxy.\mathbf{ifz}(y,x,f\cdot(\mathbf{succ}\,x)\cdot(\mathbf{pred}\,y))):\mathsf{int}\rightarrow\mathsf{int}\rightarrow\mathsf{int}$.

  5. (5)

$\vdash^{\mathsf{E}}\boldsymbol{\Omega}:\alpha$, for all
$\alpha\in\mathbb{T}$.

The following lemma summarizes the main (rather standard) properties of the
language EPCF.

######  Lemma 1.8.

Let $M$ be an EPCF term, $V\in\mathrm{Val}$, $\alpha,\beta\in\mathbb{T}$ and
$\Gamma$ be a context.

  1. (1)

(Syntax directedness) Every derivable judgement
$\Gamma\vdash^{\mathsf{E}}M:\alpha$ admits a unique derivation.

  2. (2)

(Strengthening) If $\Gamma,x:\beta\vdash^{\mathsf{E}}M:\alpha$ and
$x\notin\mathrm{FV}(M)$ then $\Gamma\vdash^{\mathsf{E}}M:\alpha$.

  3. (3)

(Subject reduction) For $M$ closed, $\vdash^{\mathsf{E}}M:\alpha$ and
$[\,]\triangleright M\Downarrow_{d}V$ entail $\vdash^{\mathsf{E}}V:\alpha$.

It follows that, if an EPCF program $M$ is typable, then it is also typable in
the empty context.

##  2 Extended Addressing Machines

We extend the addressing machines from [11] with instructions for performing
arithmetic operations and conditional testing. Natural numbers are represented
by particular machines playing the role of numerals.

###  2.1 Main definitions

We consider fixed a countably infinite set $\mathbb{A}$ of _addresses_
together with a distinguished countable subset $\mathbb{X}\subset\mathbb{A}$,
such that $\mathbb{A}-\mathbb{X}$ remains infinite. Intuitively, $\mathbb{X}$
is the set of addresses that we reserve for the numerals, therefore hereafter
we work under the hypothesis that $\mathbb{X}={\rm Nature}$, an assumption
that we can make without loss of generality.

Let $\varnothing\notin\mathbb{A}$ be a “null” constant corresponding to an
uninitialised register. Set
$\mathbb{A}_{\varnothing}=\mathbb{A}\cup\\{\varnothing\\}$.

######  Definition 2.1.

  1. (1)

An _$\mathbb{A}$ -valued tape_ $T$ is a finite ordered list of addresses
$T=[a_{1},\dots,a_{n}]$ with $a_{i}\in\mathbb{A}$ for all $i\,(1\leq i\leq
n)$. When $\mathbb{A}$ is clear from the context, we simply call $T$ a tape.
We denote by $\mathcal{T}_{\mathbb{A}}$ the set of all $\mathbb{A}$-valued
tapes.

  2. (2)

Let $a\in\mathbb{A}$ and $T,T^{\prime}\in\mathcal{T}_{\mathbb{A}}$. We denote
by $a::T$ the tape having $a$ as first element and $T$ as tail. We write
$T\,@\,T^{\prime}\,$ for the concatenation of $T$ and $T^{\prime}$, which is
an $\mathbb{A}$-valued tape itself.

  3. (3)

Given an index $i\geq 0$, an $\mathbb{A}_{\varnothing}$-valued _register_
$R_{i}$ is a memory-cell capable of storing either $\varnothing$ or an address
$a\in\mathbb{A}$. We write $\oc R_{i}$ to represent the value stored in the
register $R_{i}$. (The notation $\oc R_{i}$ is borrowed from ML, where $\oc$
represents an explicit dereferencing operator.)

  4. (4)

Given $\mathbb{A}_{\varnothing}$-valued registers $R_{0},\dots,R_{n}$ for
$n\geq 0$, an address $a\in\mathbb{A}$ and an index $i\geq 0$, we write $\pol
R[R_{i}:=a]$ for the list of registers $\pol R$ where the value of $R_{i}$ has
been updated by setting $\oc R_{i}=a$. Notice that, whenever $i>n$, we assume
that the contents of $\pol R$ remains unchanged, i.e. $\pol R[R_{i}:=a]=\pol
R$.

Intuitively, the contents of the registers $R_{0},\dots,R_{n}$ constitutes the
_state_ of a machine, while the tape correspond to the list of its inputs. The
addressing machines from [11] are endowed with only three instructions
($i,j,k,l$ range over indices of registers):

  1. 1.

$\mathtt{Load}~{}i$ : reads an address $a$ from the input tape, assuming it is
non-empty, and stores $a$ in the register $R_{i}$. If the tape is empty then
the machine suspends its execution without raising an error.

  2. 2.

$k\shortleftarrow\mathtt{App}(i,\,j)$ : reads the addresses $a_{1},a_{2}$ from
$R_{i}$ and $R_{j}$ respectively, and stores in $R_{k}$ the address of the
machine obtained by extending the tape of the machine of address $a_{1}$ with
the address $a_{2}$. The resulting address is not calculated internally but
rather obtained calling an external _application map_.

  3. 3.

$\mathtt{Call}~{}i$ : transfers the computation to the machine having as
address the value stored in $R_{i}$, whose tape is extended with the remainder
of the current machine’s tape.

As a general principle, writing on a non-existing register does not cause
issues as the value is simply discarded—this is in fact the way one can erase
an argument. The attempt of reading an uninitialized register would raise an
error—we however show that these kind of errors can be avoided statically (see
Lemma 2.4).

We enrich the above set of instructions with arithmetic operations mimicking
the ones present in PCF:

  1. 4.

$l\shortleftarrow\mathtt{Test}(i,\,j,\,k)$: implements the “ _is zero?_ ” test
on $!R_{i}$. Assuming that the value of $R_{i}$ is an address $n\in{\rm
Nature}$, the instruction stores in $R_{l}$ the value of $R_{j}$ or $R_{k}$,
depending on whether $n=0$.

  2. 5.

$j\shortleftarrow\mathtt{Pred}(i)$: if $\oc R_{i}\in{\rm Nature}$, the value
of $R_{j}$ becomes $\oc R_{i}\ominus 1=\max(\oc R_{i}-1,0)$.

  3. 6.

$j\shortleftarrow\mathtt{Succ}(i)$: if $\oc R_{i}\in{\rm Nature}$, then the
value of $R_{j}$ becomes $\oc R_{i}+1$.

Notice that the instructions above need $R_{i}$ to contain a natural number to
perform the corresponding operation. However, they are also supposed to work
on addresses of machines that compute a numeral. For this reason, the machine
whose address is stored in $R_{i}$ must first be executed, and only if the
computation terminates with a numeral is the arithmetic operation performed.
Clearly, if the computation terminates in an address not representing a
numeral, then an error should be raised at execution time. We will see that
these kind of errors can be avoided using a type inference algorithm (see
Proposition 3.6, below).

######  Definition 2.2.

  1. (1)

A _program_ $P$ is a finite list of instructions generated by the following
grammar, where $\varepsilon$ represents the empty string and $i,j,k,l$ are
indices of registers:

$\begin{array}[]{lcl}\mathtt{P}&::=&\mathtt{Load}~{}i;\,\mathtt{P}\mid\mathtt{A}\\\
\mathtt{A}&::=&k\shortleftarrow\mathtt{App}(i,\,j);\,\mathtt{A}\mid
l\shortleftarrow\mathtt{Test}(i,\,j,\,k);\,\mathtt{A}\mid
j\shortleftarrow\mathtt{Pred}(i);\,\mathtt{A}\mid
j\shortleftarrow\mathtt{Succ}(i);\,\mathtt{A}\mid\mathtt{C}\\\
\mathtt{C}&::=&\mathtt{Call}~{}i\mid\varepsilon\end{array}$

Thus, a program starts with a list of $\mathtt{Load}$’s, continues with a list
of $\mathtt{App}$, $\mathtt{Test}$, $\mathtt{Pred}$, $\mathtt{Succ}$, and
possibly ends with a $\mathtt{Call}$. Each of these lists may be empty, in
particular the empty program $\varepsilon$ can be generated.

  2. (2)

In a program, we write $\mathtt{Load}~{}(i_{1},\dots,i_{n})$ as an
abbreviation for the instructions
$\mathtt{Load}~{}i_{1};\,\cdots;\,\mathtt{Load}~{}i_{n}$.

  3. (3)

Let $P$ be a program, $r\geq 0$, and $\mathcal{I}\subseteq\\{0,\dots,r-1\\}$
be a set of indices corresponding to the indices of initialized registers.
Define the relation $\mathcal{I}\models^{r}P$, whose intent is to specify that
$P$ does not read uninitialized registers, as the least relation closed under
the rules:

$\begin{array}[]{cccc}\mathcal{I}\models^{r}\varepsilon&\mathcal{I}\models^{r}\mathtt{Call}~{}ii\in\mathcal{I}&\mathcal{I}\models^{r}j\shortleftarrow\mathtt{Pred}(i);\,\mathtt{A}\lx@proof<EMAIL_ADDRESS>\mathcal{I}\models^{r}\mathtt{Load}~{}i;\,\mathtt{P}\lx@proof@logical@and\mathcal{I}\cup\\{i\\}\models^{r}\mathtt{P}i<r&\mathcal{I}\models^{r}\mathtt{Load}~{}i;\,\mathtt{P}\lx@proof@logical@and\mathcal{I}\models^{r}\mathtt{P}i\geq
r&\mathcal{I}\models^{r}j\shortleftarrow\mathtt{Succ}(i);\,\mathtt{A}\lx@proof<EMAIL_ADDRESS>\mathcal{I}\models^{r}k\shortleftarrow\mathtt{App}(i,\,j);\,\mathtt{A}\lx@proof@logical@and\mathcal{I}\cup\\{k\\}\models^{r}\mathtt{A}i,j\in\mathcal{I}k<r&\lx@intercol\hfil\mathcal{I}\models^{r}l\shortleftarrow\mathtt{Test}(i,\,j,\,k);\,\mathtt{A}\lx@proof@logical@and\mathcal{I}\cup\\{l\\}\models^{r}\mathtt{A}i,j,k\in\mathcal{I}l<r\hfil\lx@intercol\end{array}$

  4. (4)

A program $P$ is _valid with respect to $R_{0},\dots,R_{r-1}$_ if
$\mathcal{R}\models^{r}P$ holds for $\mathcal{R}=\\{i\mid
R_{i}\neq\varnothing\ \land\ 0\leq i<r\\}$.

######  Example 2.3.

For each of these programs, we specify its validity with respect to
$R_{0}=7,R_{1}=a,R_{2}=\varnothing$ (i.e., $r=3$).

$\begin{array}[]{lcr}P_{1}=2\shortleftarrow\mathtt{Pred}(0);\,\mathtt{Call}~{}2&&\textrm{(valid)}\\\
P_{2}=\mathtt{Load}~{}(2,8);\,0\shortleftarrow\mathtt{Test}(0,\,1,\,2);\,\mathtt{Call}~{}0&&\textrm{(valid)}\\\
P_{3}=\mathtt{Load}~{}(0,2,8);\,\mathtt{Call}~{}8&&\textrm{(calling the
uninitialized register $R_{8}$, thus not valid)}\end{array}$

######  Lemma 2.4.

Given $\mathbb{A}_{\varnothing}$-valued registers $\pol R$ and a program $P$
it is decidable whether $P$ is valid w.r.t. $\pol R$.

######  Proof 2.5.

Decidability follows from the syntax directedness of Definition 2.2(3), and
the preservation of the invariant $\mathcal{I}\subseteq\\{0,\dots,r-1\\}$,
since $\mathcal{I}$ is only extended with $k<r$.

######  Definition 2.6.

  1. (1)

An _extended addressing machine_ (_EAM_) $\mathsf{M}$ with $r$ registers over
$\mathbb{A}$ is given by a tuple:

$\mathsf{M}=\langle R_{0},\dots,R_{r-1},P,T\rangle$

where $\pol R$ are $\mathbb{A}_{\varnothing}$-valued registers, $P$ is a
program valid w.r.t. $\pol R$ and $T\in\mathcal{T}_{\mathbb{A}}$ is an (input)
tape.

  2. (2)

We write $\mathsf{M}.r$ for the number of registers of $\mathsf{M}$,
$\mathsf{M}.R_{i}$ for its $i$-th register, $\mathsf{M}.P$ for the associated
program and $\mathsf{M}.T$ for its input tape. When writing “$R_{i}=a$” in a
tuple we indicate that $R_{i}$ is present and $\oc R_{i}=a$.

  3. (3)

We say that an extended addressing machine $\mathsf{M}$ as above is _stuck_ ,
written $\mathsf{stuck}(\mathsf{M})$, whenever its program has shape
$\mathsf{M}.P=\mathtt{Load}~{}i;P$ but its input-tape is empty
$\mathsf{M}.T=[]$. Otherwise $\mathsf{M}$ is _ready_ , written
$\lnot\mathsf{stuck}(\mathsf{M})$.

  4. (4)

The set of all extended addressing machines over $\mathbb{A}$ will be denoted
by $\mathcal{M}_{\mathbb{A}}$.

  5. (5)

For $n\geq 0$, the _$n$ -th numeral machine_ is defined $\mathsf{n}=\langle
R_{0},\varepsilon,[]\rangle$ with $\oc R_{0}=n$.

  6. (6)

For $n\geq 0$ and $a\in\mathbb{A}$, define

$\mathsf{Y}_{n}^{a}=\langle(R_{0}=a,R_{1}=\varnothing,\dots,R_{n+1}=\varnothing,P,[]\rangle$

where$\begin{array}[t]{rl}P=&\mathtt{Load}~{}(1,\dots,{n+1});0\shortleftarrow\mathtt{App}(0,\,1);\cdots;0\shortleftarrow\mathtt{App}(0,\,n+1);1\shortleftarrow\mathtt{App}(1,\,2);\cdots;\\\
&1\shortleftarrow\mathtt{App}(1,\,n+1);1\shortleftarrow\mathtt{App}(1,\,0);\mathtt{Call}~{}1\end{array}$

We now enter into the details of the addressing mechanism which constitutes
the core of this formalism.

######  Definition 2.7.

Recall that ${\rm Nature}$ stands for an infinite subset of $\mathbb{A}$, here
identified with the set of natural numbers, and $\mathsf{Y}_{n}^{a}$ has been
introduced in Definition 2.6(6).

  1. (1)

Since $\mathcal{M}_{\mathbb{A}}$ is countable, we can fix a bijective function
$\\#:\mathcal{M}_{\mathbb{A}}\to\mathbb{A}$ satisfying the following
conditions:

    1. (a)

(Numerals) $\forall n\in\mathbb{N}\,.\,\\#{\mathsf{n}}=n$, where $\mathsf{n}$
is the $n$-th numeral machine;

    2. (b)

(Fixed point combinator) for all $n\geq 0$, there exists an address
$a\in\mathbb{A}-{\rm Nature}$ such that $\\#(\mathsf{Y}_{n}^{a})=a$.

We say that the bijection $\\#(\cdot)$ is an _address table map_ and call the
element $\\#\mathsf{M}$ the address of the EAM $\mathsf{M}$. We simply write
$\mathsf{Y}_{n}$ for the machine satisfying the equation above and
$a_{\mathsf{Y}_{n}}$ for its address, i.e.
$\\#(\mathsf{Y}_{n})=a_{\mathsf{Y}_{n}}$.

  2. (2)

For $a\in\mathbb{A}$, we write $\\#^{-1}(a)$ for the unique machine having
address $a$, i.e., $\\#^{-1}(a)=\mathsf{M}\iff\\#\mathsf{M}=a.$

  3. (3)

Given $\mathsf{M}\in\mathcal{M}_{\mathbb{A}}$ and
$T^{\prime}\in\mathcal{T}_{\mathbb{A}}$, we write
$\mathsf{M}\,@\,T^{\prime}\,$ for the machine $\langle\mathsf{M}.\pol
R,\mathsf{M}.P,\mathsf{M}.T\,@\,T^{\prime}\,\rangle$.

  4. (4)

Define the _application map_ $(\cdot):\mathbb{A}\times\mathbb{A}\to\mathbb{A}$
by setting $a\cdot b=\\#(\\#^{-1}(a)\,@\,{[}b{]}\,)$, i.e., the _application_
of $a$ to $b$ is the unique address $c$ of the EAM obtained by adding $b$ at
the end of the input tape of the EAM $\\#^{-1}(a)$.

######  Example 2.8.

The following are examples of EAMs (whose registers are assumed uninitialized,
i.e. $\pol R=\pol\varnothing$).

  1. (1)

$\mathsf{Succ1}:=\langle
R_{0},\mathtt{Load}~{}0;0\shortleftarrow\mathtt{Succ}(0);\mathtt{Call}~{}0,[]\rangle$.

  2. (2)

$\mathsf{Succ2}:=\langle
R_{0},R_{1},\mathtt{Load}~{}0;\mathtt{Load}~{}1;1\shortleftarrow\mathtt{App}(0,\,1);1\shortleftarrow\mathtt{App}(0,\,1);\mathtt{Call}~{}1,[a_{\mathsf{S}}]\rangle$,
where $a_{\mathsf{S}}=\\#{\mathsf{Succ1}}$.

  3. (3)

$\mathsf{Add\\_aux}:=\langle\pol R,P,[]\rangle$ with $\mathsf{Add\\_aux}.r=5$
and
$P=\mathtt{Load}~{}(0,1,2);3\shortleftarrow\mathtt{Pred}(1);4\shortleftarrow\mathtt{Succ}(2);0\shortleftarrow\mathtt{App}(0,\,3);$
$0\shortleftarrow\mathtt{App}(0,\,4);0\shortleftarrow\mathtt{Test}(1,\,2,\,0);\mathtt{Call}~{}0$.

######  Remark 2.9.

In general, there are uncountably many possible address table maps of
arbitrary computational complexity. A natural example of such maps is given by
_Gödelization_ , which can be performed effectively. The framework is however
more general and allows to consider non-r.e. sets of addresses like the
complement $K^{c}$ of the halting set

$K=\\{(i,x)\mid\textrm{the program $i$ terminates when run on input $x$}\\}$

and a non-computable function $\\#:\mathcal{M}_{K^{c}}\to K^{c}$ as a map.

In an implementation of EAMs the address table map should be computable—one
can choose a fresh address from $\mathbb{A}$ whenever a new machine is
constructed, save the correspondence in some table and retrieve it in constant
time.

######  Remark 2.10.

Depending on the chosen address table map, it might be possible to construct
infinite (static) chains of EAMs $(\mathsf{M})_{n\in{\rm Nature}}$, e.g.,
$\mathsf{M}_{n}=\langle R_{0}=\\#\mathsf{M}_{n+1},\varepsilon,[]\rangle$.

The results we present are independent from the choice of $\\#$.

###  2.2 Operational semantics

The operational semantics of extended addressing machines is given through a
small-step rewriting system. The reduction strategy is deterministic, since
the only applicable rule at every step is univocally determined by the first
instruction of the internal program, the contents of the registers and the
head of the tape.

######  Definition 2.11.

We introduce a fresh constant $\texttt{err}\notin\mathcal{M}_{\mathbb{A}}$ to
represent a machine raising an error.

  1. (1)

Define a reduction strategy $\to_{\mathsf{c}}$ on EAMs, representing one step
of computation, as the least relation $\to_{\mathsf{c}}\
\subseteq\mathcal{M}_{\mathbb{A}}\times(\mathcal{M}_{\mathbb{A}}\cup\\{\texttt{err}\\})$
closed under the rules in Figure 3.

  2. (2)

The _multistep reduction_ $\twoheadrightarrow_{\mathsf{c}}$ is defined as the
transitive-reflexive closure of $\to_{\mathsf{c}}$.

  3. (3)

Given
$\mathsf{M},\mathsf{N},\mathsf{M}\twoheadrightarrow_{\mathsf{c}}\mathsf{N}$,
we write $|\mathsf{M}\twoheadrightarrow_{\mathsf{c}}\mathsf{N}|\in{\rm
Nature}$ for the length of the (unique) reduction path from $\mathsf{M}$ to
$\mathsf{N}$.

  4. (4)

For $\mathsf{M},\mathsf{N}\in\mathcal{M}_{\mathbb{A}}$, we write
$\mathsf{M}\leftrightarrow_{\mathsf{c}}\mathsf{N}$ if they have a common
reduct $\mathsf{Z}\in\mathcal{M}_{\mathbb{A}}\cup\\{\texttt{err}\\}$, i.e.
$\mathsf{M}\twoheadrightarrow_{\mathsf{c}}\mathsf{Z}{~{}}_{\mathsf{c}}\\!\\!\twoheadleftarrow\mathsf{N}$.

  5. (5)

An extended address machine $\mathsf{M}$: _is in final state_ if it cannot
reduce, written $\mathsf{M}\not\to_{\mathsf{c}}$; _reaches a final state_ if
$\mathsf{M}\twoheadrightarrow_{\mathsf{c}}\mathsf{M}^{\prime}$ for some
$\mathsf{M}^{\prime}\in\mathcal{M}_{\mathbb{A}}$ in final state; _raises an
error_ if $\mathsf{M}\twoheadrightarrow_{\mathsf{c}}\texttt{err}$; _does not
terminate_ , otherwise.

Unconditional rewriting rules

$\begin{array}[]{rcl}\langle\pol
R,\mathtt{Call}~{}i;P,T\rangle&\to_{\mathsf{c}}&\\#^{-1}(\oc R_{i})\,@\,T\\\
\langle\pol R,\mathtt{Load}~{}i;P,a::T\rangle&\to_{\mathsf{c}}&\langle\pol
R[R_{i}:=a],P,T\rangle\\\ \langle\pol
R,k\shortleftarrow\mathtt{App}(i,\,j);P,T\rangle&\to_{\mathsf{c}}&\langle\pol
R[R_{k}:=\oc R_{i}\cdot\oc R_{j}],P,T\rangle\\\ \end{array}$

Under the assumption that $\\#^{-1}(\oc R_{i})\not\to_{\mathsf{c}}$ (i.e., it
is in final state).

$\begin{array}[]{rcl}\langle\pol
R,j\shortleftarrow\mathtt{Pred}(i);P,T\rangle&\to_{\mathsf{c}}&\begin{cases}\langle\pol
R[R_{j}:=\oc R_{i}\ominus 1,P,T\rangle,&\textrm{if }\oc R_{i}\in{\rm
Nature},\\\ \texttt{err},&\textrm{otherwise}.\end{cases}\\\\[12.91663pt]
\langle\pol
R,j\shortleftarrow\mathtt{Succ}(i);P,T\rangle&\to_{\mathsf{c}}&\begin{cases}\langle\pol
R[R_{j}:=\oc R_{i}\oplus 1,P,T\rangle,&\textrm{if }\oc R_{i}\in{\rm
Nature},\\\ \texttt{err},&\textrm{otherwise}.\end{cases}\\\\[12.91663pt]
\langle\pol
R,l\shortleftarrow\mathtt{Test}(i,\,j,\,k);P,T\rangle&\to_{\mathsf{c}}&\begin{cases}\langle\pol
R[R_{l}:=\oc R_{j}],P,T\rangle,&\textrm{if }\oc R_{i}=0,\\\\[3.0pt]
\langle\pol R[R_{l}:=\oc R_{k}],P,T\rangle,&\textrm{if }\oc R_{i}\in{\rm
Nature}^{+},\\\ \texttt{err},&\textrm{otherwise}.\end{cases}\\\\[12.91663pt]
\end{array}$

Under the assumption that $\\#^{-1}(\oc R_{i})\to_{\mathsf{c}}\mathsf{A}$
(i.e., it is not in final state).

$\begin{array}[]{rcl}\langle\pol
R,j\shortleftarrow\mathtt{Pred}(i);P,T\rangle&\to_{\mathsf{c}}&\langle\pol
R[R_{i}:=\\#{\mathsf{A}}],j\shortleftarrow\mathtt{Pred}(i);P,T\rangle\\\\[4.30554pt]
\langle\pol
R,j\shortleftarrow\mathtt{Succ}(i);P,T\rangle&\to_{\mathsf{c}}&\langle\pol
R[R_{i}:=\\#{\mathsf{A}}],j\shortleftarrow\mathtt{Succ}(i);P,T\rangle\\\\[4.30554pt]
\langle\pol
R,l\shortleftarrow\mathtt{Test}(i,\,j,\,k);P,T\rangle&\to_{\mathsf{c}}&\langle\pol
R[R_{i}:=\\#{\mathsf{A}}],l\shortleftarrow\mathtt{Test}(i,\,j,\,k);P,T\rangle\\\\[4.30554pt]
\end{array}$

Figure 3: Small-step operational semantics for extended addressing machines.

Notice that since the redexes in Figure 3 are not overlapping, the confluence
of $\twoheadrightarrow_{\mathsf{c}}$ follows easily (cf. [11, Lemma 2.11(2)]).

######  Lemma 2.12.

If $\mathsf{M}\twoheadrightarrow_{\mathsf{c}}\mathsf{M^{\prime}}$, then
$\mathsf{M}\,@\,\\#\mathsf{N}\,\twoheadrightarrow_{\mathsf{c}}\mathsf{M^{\prime}}\,@\,\\#\mathsf{N}\,$.

######  Proof 2.13.

By induction on the length of
$\mathsf{M}\twoheadrightarrow_{\mathsf{c}}\mathsf{M^{\prime}}$.

######  Example 2.14.

See Example 2.8 for the definition of $\mathsf{Succ1}$, $\mathsf{Succ2}$,
$\mathsf{Add\\_aux}$.

  1. (1)

We have $\mathsf{Succ1}\,@\,[0]\,\twoheadrightarrow_{\mathsf{c}}\mathsf{1}$
and $\mathsf{Succ2}\,@\,[1]\,\twoheadrightarrow_{\mathsf{c}}\mathsf{3}$.

  2. (2)

Define $\mathsf{Add}=\mathsf{Y}_{0}\,@\,[\\#\mathsf{Add\\_aux}]\,$, an EAM
performing the addition. We show:

$\begin{array}[]{l}\mathsf{Add}\,@\,[1,3]\,\to_{\mathsf{c}}\left\langle\begin{aligned}
(R_{0}=a_{\mathsf{Y}_{0}},R_{1}=\\#\mathsf{Add\\_aux}),0\shortleftarrow\mathtt{App}(0,\,1);1\shortleftarrow\mathtt{App}(1,\,0);\mathtt{Call}~{}1,[1,3]\end{aligned}\right\rangle\\\\[4.30554pt]
\twoheadrightarrow_{\mathsf{c}}\left\langle\begin{aligned} \pol
R,\mathtt{Load}~{}(0,1,2);3\shortleftarrow\mathtt{Pred}(1);4\shortleftarrow\mathtt{Succ}(2);0\shortleftarrow\mathtt{App}(0,\,3);0\shortleftarrow\mathtt{App}(0,\,4);\\\
0\shortleftarrow\mathtt{Test}(1,\,2,\,0);\mathtt{Call}~{}0,[\\#{\mathsf{Add}},1,3]\end{aligned}\right\rangle\\\\[8.61108pt]
\twoheadrightarrow_{\mathsf{c}}\left\langle\begin{aligned}
R_{0}=\\#{\mathsf{Add}},R_{1}=1,R_{2}=3,R_{3},R_{4},3\shortleftarrow\mathtt{Pred}(1);4\shortleftarrow\mathtt{Succ}(2);0\shortleftarrow\mathtt{App}(0,\,3);\\\
0\shortleftarrow\mathtt{App}(0,\,4);0\shortleftarrow\mathtt{Test}(1,\,2,\,0);\mathtt{Call}~{}0,[]\end{aligned}\right\rangle\\\\[4.30554pt]
\twoheadrightarrow_{\mathsf{c}}\left\langle\begin{aligned}
R_{0}=\\#(\mathsf{Add}\,@\,[0,4]\,),R_{1}=1,R_{2}=3,R_{3}=0,R_{4}=4,0\shortleftarrow\mathtt{Test}(1,\,2,\,0);\mathtt{Call}~{}0,[]\end{aligned}\right\rangle\\\\[4.30554pt]
\twoheadrightarrow_{\mathsf{c}}\left\langle\begin{aligned}
R_{0}=\\#(\mathsf{Add}\,@\,[0,5]\,),R_{1}=0,R_{2}=4,R_{3}=0,R_{4}=5,0\shortleftarrow\mathtt{Test}(1,\,2,\,0);\mathtt{Call}~{}0,[]\end{aligned}\right\rangle\twoheadrightarrow_{\mathsf{c}}\mathsf{4}\end{array}$

  3. (3)

For $\mathsf{I}=\langle
R_{0}=\varnothing,\mathtt{Load}~{}0;\mathtt{Call}~{}0,[]\rangle$,
$\mathsf{Y}_{0}\,@\,[\\#\mathsf{I}]\,\twoheadrightarrow_{\mathsf{c}}\mathsf{I}\,@\,[\\#(\mathsf{Y}_{0}\,@\,[\\#\mathsf{I}]\,)]\,$.

  4. (4)

$\mathsf{Y}_{n}\,@\,[\\#\mathsf{M},d_{1},\dots,d_{n}]\,\twoheadrightarrow_{\mathsf{c}}\mathsf{M}\,@\,[d_{1},\dots,d_{n},\\#(\mathsf{Y}_{n}\,@\,[\\#\mathsf{M},d_{1},\dots,d_{n}]\,)]\,,$
for all $n\geq 0$, $\mathsf{M}\in\mathcal{M}_{\mathbb{A}}$, $\pol
d\in\mathbb{A}$.

##  3 Typing Algorithm

$\begin{array}[]{c}\begin{array}[]{ccc}\vdash\mathsf{M}:\mathsf{int}\\#\mathsf{M}\in{\rm
Nature}&\qquad\qquad\vdash\mathsf{M}:(\pol\delta\to\alpha\to\alpha)\to\pol\delta\to\alpha\lx@proof@logical@and\\#{\mathsf{M}}=a_{\mathsf{Y}_{n}}\pol\delta=\delta_{1}\to\cdots\to\delta_{n}&\Delta\vdash\langle(),P,T\rangle:\alpha\Delta\Vdash(P,T):\alpha\end{array}\\\\[4.30554pt]
\begin{array}[]{cc}\Delta\vdash\langle(R_{0},\dots,R_{r}),P,T\rangle:\alpha\lx@proof@logical@and\Delta\vdash\langle
R_{0},\dots,R_{r-1},P,T\rangle:\alpha\oc
R_{r}=\varnothing&\Delta\vdash\langle(R_{0},\dots,R_{r}),P,T\rangle:\alpha\lx@proof@logical@and
R_{r}:\beta,\Delta\vdash\langle
R_{0},\dots,R_{r-1},P,T\rangle:\alpha\vdash\\#^{-1}(\oc
R_{r}):\beta\\\\[4.30554pt]
\Delta\Vdash(\mathtt{Load}~{}i;P,[]):\beta\to\alpha\Delta[R_{i}:\beta]\Vdash(P,[]):\alpha&\Delta\Vdash(\mathtt{Load}~{}i;P,a::T):\alpha\lx@proof@logical@and\Delta[R_{i}:\beta]\Vdash(P,T):\alpha\vdash\\#^{-1}(a):\beta\\\\[4.30554pt]
\Delta,R_{i}:\mathsf{int}\Vdash(j\shortleftarrow\mathtt{Pred}(i);P,T):\alpha(\Delta,R_{i}:\mathsf{int})[R_{j}:\mathsf{int}]\Vdash(P,T):\alpha&\Delta,R_{i}:\mathsf{int}\Vdash(j\shortleftarrow\mathtt{Succ}(i);P,T):\alpha(\Delta,R_{i}:\mathsf{int})[R_{j}:\mathsf{int}]\Vdash(P,T):\alpha\\\\[4.30554pt]
\end{array}\\\\[4.30554pt]
\Delta,R_{i}:\mathsf{int},R_{j}:\beta,R_{k}:\beta\Vdash(l\shortleftarrow\mathtt{Test}(i,\,j,\,k);P,T):\alpha(\Delta,R_{i}:\mathsf{int},R_{j}:\beta,R_{k}:\beta)[R_{l}:\beta]\Vdash(P,T):\alpha\\\\[4.30554pt]
\Delta,R_{i}:\alpha\to\beta,R_{j}:\alpha\Vdash(k\shortleftarrow\mathtt{App}(i,\,j);P,T):\delta(\Delta,R_{i}:\alpha\to\beta,R_{j}:\alpha)[R_{k}:\beta]\Vdash(P,T):\delta\\\\[4.30554pt]
\Delta,R_{i}:\alpha_{1}\to\dots\to\alpha_{n}\to\alpha\Vdash(\mathtt{Call}~{}i,[\\#{\mathsf{M}_{1}},\dots,\\#{\mathsf{M}_{n}}]):\alpha\lx@proof@logical@and\vdash\mathsf{M}_{1}:\alpha_{1}\cdots\vdash\mathsf{M}_{n}:\alpha_{n}\end{array}$

Figure 4: Typing rules for extended addressing machines.

Recall that the set $\mathbb{T}$ of (simple) types has been introduced in
Definition 1.6(1). We now show that certain EAMs can be typed, and that
typable machines do not raise error during their execution.

######  Definition 3.1.

  1. (1)

A _typing context_ $\Delta$ is a finite set of associations between registers
and types, represented as a list
$R_{i_{1}}:\alpha_{1},\dots,R_{i_{n}}:\alpha_{n}$. The indices
$i_{1},\dots,i_{n}$ are not necessarily consecutive.

  2. (2)

We denote by $\Delta[R_{i}:\alpha]$ the typing context $\Delta$ where the type
associated with $R_{i}$ becomes $\alpha$. If $R_{i}$ is not present in
$\Delta$, then $\Delta[R_{i}:\alpha]=\Delta,R_{i}:\alpha$.

  3. (3)

Let $\Delta$ be a typing context, $\mathsf{M}\in\mathcal{M}_{\mathbb{A}}$, $P$
be a program, $T\in\mathcal{T}_{\mathbb{A}}$ and $\alpha\in\mathbb{T}$. We
define the typing judgements

$\Delta\vdash\mathsf{M}:\alpha\qquad\qquad\qquad\Delta\Vdash(P,T):\alpha$

by mutual induction as the least relations closed under the rules of Figure 4.
The rules $(\mathrm{nat})$ and $(\mathrm{fix})$ are the base cases and take
precedence over $(R_{\varnothing})$ and $(R_{\mathbb{T}})$.

  4. (4)

For $R_{i_{1}},\dots,R_{i_{n}}\in\pol R$, write
$R_{i_{1}}:\beta_{i_{1}},\dots,R_{i_{n}}:\beta_{i_{n}}\models\pol R$ if
$\\#^{-1}(\oc R_{j}):\beta_{j}$, for all $j\in\\{i_{1},\dots,i_{n}\\}$.

The algorithm in Figure 4 deserves some discussion. As it is presented as a
set of inference rules, one should reason bottom-up. To give a machine
$\mathsf{M}$ a type $\alpha$, one needs to derive the judgement
$\vdash\mathsf{M}:\alpha$. The machines $\mathsf{n}$ and $\mathsf{Y}_{n}$ are
recognizable from their addresses and the rules $(\mathrm{nat})$ and
$(\mathrm{fix})$ can thus be given higher precedence. Otherwise, the rule
$(R_{\mathbb{T}})$ allows to check whether the value in a register is typable
and only retain its type, the rule $(R_{\varnothing})$ allows to get rid of
uninitialized registers. Once this initial step is performed, one needs to
derive a judgement of the form
$R_{i_{1}}:\beta_{i_{1}},\dots,R_{i_{n}}:\beta_{i_{n}}\Vdash(P,T):\alpha$,
where $P$ and $T$ are the program and the input tape of the original machine
respectively. This is done by verifying the coherence of the instructions in
the program with the types of the registers and of the values in the input
tape. As a final consideration, notice that the rules in Figure 4 can only be
considered as an algorithm when the address table map is effectively given.
Otherwise, the algorithm would depend on an oracle deciding $a=\\#\mathsf{M}$.

######  Remark 3.2.

  1. (1)

For all $\mathsf{M}\in\mathcal{M}_{\mathbb{A}}$ and $\alpha\in\mathbb{T}$, we
have $\vdash\mathsf{M}:\alpha$ if and only if there exists $a\in\mathbb{A}$
such that both $\\#^{-1}(a):\alpha$ and $\\#{\mathsf{M}}=a$ hold.

  2. (2)

If $\\#\mathsf{M}\notin{\rm Nature}\cup\\{a_{\mathsf{Y}_{n}}\mid n\geq 0\\}$,
then
$\vdash\mathsf{M}:\alpha\iff\exists\Delta\,.\,[\Delta\models\mathsf{M}.\pol R\
\land\ \Delta\Vdash(\mathsf{M}.P,\mathsf{M}.T):\alpha]$

  3. (3)

The higher priority assigned to the rules $(\mathrm{nat})$ and
$(\mathrm{fix})$ does not modify the set of typable machines, rather
guarantees the syntax-directedness of the system.

######  Example 3.3.

The following typing judgements are derivable.

  1. (1)

$\vdash\mathsf{Succ2}:\mathsf{int}\rightarrow\mathsf{int}$

  2. (2)

$\vdash\mathsf{Add}:\mathsf{int}\rightarrow\mathsf{int}\rightarrow\mathsf{int}$,
where $\mathsf{Add}=\mathsf{Y}_{0}\,@\,[\\#\mathsf{Add\\_aux}]\,$

  3. (3)

For a smaller example, like
$\vdash\mathsf{Succ1}:\mathsf{int}\to\mathsf{int}$, we can provide the whole
derivation tree:

$\vdash\langle(R_{0}=\varnothing),\mathtt{Load}~{}0;0\shortleftarrow\mathtt{Succ}(0);\mathtt{Call}~{}0,[]\rangle:\mathsf{int}\to\mathsf{int}\lx@proof@logical@and\vdash\langle(),\mathtt{Load}~{}0;0\shortleftarrow\mathtt{Succ}(0);\mathtt{Call}~{}0,[]\rangle:\mathsf{int}\to\mathsf{int}\Vdash\langle\mathtt{Load}~{}0;0\shortleftarrow\mathtt{Succ}(0);\mathtt{Call}~{}0,[]\rangle:\mathsf{int}\to\mathsf{int}R_{0}:\mathsf{int}\Vdash\langle
0\shortleftarrow\mathtt{Succ}(0);\mathtt{Call}~{}0,[]\rangle:\mathsf{int}R_{0}:\mathsf{int}\Vdash\langle\mathtt{Call}~{}0,[]\rangle:\mathsf{int}\oc
R_{0}=\varnothing$

######  Lemma 3.4.

Let $\mathsf{M}\in\mathcal{M}_{\mathbb{A}}$, $\alpha\in\mathbb{T}$. Assume
that $\\#:\mathsf{M}\to\mathbb{A}$ is effectively given.

  1. (1)

If $\mathsf{M}=\langle\pol R=\varnothing,P,[]\rangle$ then the typing
algorithm is capable of deciding whether $\vdash\mathsf{M}:\alpha$ holds.

  2. (2)

In general, the typing algorithm semi-decides whether
$\vdash\mathsf{M}:\alpha$ holds.

######  Proof 3.5.

(Sketch) (i) In this case, $\vdash\mathsf{M}:\alpha$ holds if and only if
$\Vdash(\mathsf{M}.P,[])$ does. By induction on the length of $\mathsf{M}.P$,
one verifies if it is possible to construct a derivation. Otherwise, conclude
that $\vdash\mathsf{M}:\alpha$ is not derivable.

(ii) In the rules $(R_{\mathbb{T}})$ and $(\mathrm{load}_{\mathbb{T}})$, one
needs to show that a type for the premises exists. As the set of types is
countable, and effectively given, one can easily design an algorithm
constructing a derivation tree (by dovetailing). However, the algorithm cannot
terminate when executed on $\mathsf{M}_{0}$ from Remark 2.10.

The machine $\mathsf{M}_{0}$ in Remark 2.10 cannot be typable because it would
require an infinite derivation tree.

######  Proposition 3.6.

Let $\mathsf{M},\mathsf{M^{\prime}},\mathsf{N},\in\mathcal{M}_{\mathbb{A}}$
and $\alpha,\beta\in\mathbb{T}$.

  1. (1)

If $\vdash\mathsf{M}:\beta\to\alpha$ and $\vdash\mathsf{N}:\beta$ then
$\vdash\mathsf{M}\,@\,[\\#{\mathsf{N}}]\,:\alpha$.

  2. (2)

If $\vdash\mathsf{M}:\alpha$ and $\mathsf{M}\to_{\mathsf{c}}\mathsf{N}$ then
$\vdash\mathsf{N}:\alpha$.

  3. (3)

If $\vdash\mathsf{M}:\mathsf{int}$ then either $\mathsf{M}$ does not terminate
or $\mathsf{M}\twoheadrightarrow_{\mathsf{c}}\mathsf{n}$, for some $n\geq 0$.

  4. (4)

If $\vdash\mathsf{M}:\alpha$ then $\mathsf{M}$ does not raise an error.

######  Proof 3.7.

(i) Simultaneously, one proves that $\Delta\Vdash(P,T):\beta\to\alpha$ and
$\vdash\mathsf{N}:\beta$ imply
$\Delta\Vdash(P,T\,@\,[\\#\mathsf{N}]\,):\alpha$. Proceed by induction on a
derivation of $\vdash\mathsf{M}:\beta\to\alpha$ (resp.
$\Delta\Vdash(P,T):\beta\to\alpha$).

Case ($\mathrm{nat}$) is vacuous.

Case ($\mathrm{fix_{n}}$). We show the case for $n=0$, the others being
similar. By definition of $\mathsf{Y}_{0}$, we have:

$\mathsf{Y}_{0}\,@\,[\\#\mathsf{N}]\,=\left\langle\begin{aligned}
(\varnothing,a_{\mathsf{Y}_{0}}),\mathtt{Load}~{}0;1\shortleftarrow\mathtt{App}(1,\,0);0\shortleftarrow\mathtt{App}(0,\,1);\mathtt{Call}~{}0,[\\#{\mathsf{N}}]\end{aligned}\right\rangle.$

Notice that, in this case, $\beta=\alpha\to\alpha$. Using
$\\#^{-1}(a_{\mathsf{Y}_{0}})=\mathsf{Y}_{0}$, we derive:

$\vdash\langle(R_{0}=\varnothing,R_{1}=a_{\mathsf{Y}_{0}}),\mathtt{Load}~{}0;1\shortleftarrow\mathtt{App}(1,\,0);0\shortleftarrow\mathtt{App}(0,\,1);\mathtt{Call}~{}0,[\\#{\mathsf{N}}]\rangle:\alpha\lx@proof@logical@and
R_{1}:(\alpha\to\alpha)\to\alpha\Vdash\langle
R_{0}=\varnothing,\mathtt{Load}~{}0;\cdots,[\\#{\mathsf{N}}]\rangle:\alpha
R_{1}:(\alpha\to\alpha)\to\alpha\Vdash(\mathtt{Load}~{}0;\cdots,[\\#{\mathsf{N}}]):\alpha\lx@proof@logical@and
R_{0}:\alpha\to\alpha,R_{1}:(\alpha\to\alpha)\to\alpha\Vdash(1\shortleftarrow\mathtt{App}(1,\,0);\cdots,[]):\alpha
R_{0}:\alpha,R_{1}:\alpha\Vdash(\mathtt{Call}~{}0,[]):\alpha\vdash\mathsf{N}:\alpha\to\alpha\vdash\mathsf{Y}_{0}:(\alpha\to\alpha)\to\alpha\mathrm{fix}_{0}$

Case $\mathrm{load}_{\varnothing}$. Then $P=\mathtt{Load}~{}i;P^{\prime}$,
$T=[]$ and $\Delta[R_{i}:\beta]\Vdash(P^{\prime},[]):\alpha$. By assumption
$\vdash\mathsf{N}:\beta$, so we conclude
$\Delta\Vdash(\mathtt{Load}~{}i;P^{\prime},[]):\alpha$ by applying
$\mathrm{load}_{\mathbb{T}}$. All other cases derive straightforwardly from
the IH.

(ii) The cases $\mathsf{M}=\mathsf{Y}_{n}$ or $\mathsf{M}=\mathsf{n}$ for some
$n\in{\rm Nature}$ are vacuous, as these machines are in final state.
Otherwise, by Remark 3.2(2), $\Delta\Vdash(\mathsf{M}.P,\mathsf{M}.T):\alpha$
for some $\Delta\models\mathsf{M}.\pol R$. By cases on the shape of
$\mathsf{M}.P$.

Case $P=\mathtt{Load}~{}i;P^{\prime}$. Then $\mathsf{M}.T=a::T^{\prime}$
otherwise $\mathsf{M}$ would be in final state, and $\mathsf{N}=\langle\pol
R[R_{i}:=a],P^{\prime},T^{\prime}\rangle$. From $(\mathrm{Load}_{\mathbb{T}})$
we get $\Delta[R_{i}:\beta]\Vdash(P^{\prime},T^{\prime}):\alpha$ for some
$\beta\in\mathbb{T}$ satisfying $\\#^{-1}(a):\beta$. As $\Delta\models\pol R$
we derive $\Delta[R_{i}:\beta]\models\pol R[R_{i}:=a]$, so as
$N=\left\langle\begin{aligned} \pol
R[R_{i}:=a],P^{\prime},T^{\prime}\end{aligned}\right\rangle$, by Remark
3.2(2), $\vdash N:\alpha$.

Case $P=\mathtt{Call}~{}i$. Then
$R_{i}:\alpha_{1}\to\cdots\to\alpha_{n}\to\alpha$,
$T=[\\#{\mathsf{M}_{1}},\dots,\\#{\mathsf{M}_{n}}]$ and
$\vdash\mathsf{M}_{j}:\alpha_{j}$, for all $j\leq n$. In this case,
$\mathsf{N}=\\#^{-1}(\oc(\mathsf{M}.R_{i}))\,@\,T\,$ with
$\vdash\\#^{-1}(\oc(\mathsf{M}.R_{i})):\alpha_{1}\to\cdots\to\alpha_{n}\to\alpha$,
so we conclude by (i).

All other cases follows easily from the IH.

(iii) Assume that $\vdash\mathsf{M}:\mathsf{int}$ and
$\mathsf{M}\twoheadrightarrow_{\mathsf{c}}\mathsf{N}$ for some $\mathsf{N}$ in
final state. By (ii), we obtain that $\vdash\mathsf{N}:\mathsf{int}$ holds,
therefore $\mathsf{N}=\mathsf{n}$ since numerals are the only machines in
final state typable with $\mathsf{int}$.

(iv) The three cases from Figure 3 where a machine can raise an error are
ruled out by the typing rules ($\mathrm{pred}$), ($\mathrm{succ}$) and
($\mathrm{test}$), respectively. Therefore, no error can be raised during the
execution.

##  4 Translation and Simulation

We define a type-preserving translation from EPCF terms to extended addressing
machines. More precisely, we show that if $\Gamma\vdash^{\mathsf{E}}M:\alpha$
is derivable then $M$ is transformed into a machine $\mathsf{M}$ which is
typable with the same $\alpha$. By Proposition 3.6, $\mathsf{M}$ never raises
a runtime error and well–typedness is preserved during its execution. We then
show that if a well-typed EPCF program $M$ computes a value $\underline{n}$,
then its translation $\mathsf{M}$ reduces to the corresponding EAM
$\mathsf{n}$. Finally, this result is transported to PCF using their
equivalence on programs of type $\mathsf{int}$.

We start by showing that EAMs implementing the main ${\sf PCF}{}$ instructions
are definable. We do not need any machinery for representing explicit
substitutions because they are naturally modelled by the evaluation strategy
of EAMs.

######  Lemma 4.1.

Let $n\geq 0$. There are EAMs satisfying (for all
$a,b,c,d_{1},\dots,d_{n}\in\mathbb{A}$):

  1. (1)

$\mathsf{Pr}_{i}^{n}\,@\,[d_{1},\dots,d_{n}]\,\hskip
25.0pt\twoheadrightarrow_{\mathsf{c}}d_{i}$, for $1\leq i\leq n$;

  2. (2)

$\mathsf{Apply}_{n}\,@\,[a,b,d_{1},\dots,d_{n}]\,\twoheadrightarrow_{\mathsf{c}}\\#^{-1}(a)\,@\,[d_{1},\dots,d_{n},b\cdot
d_{1}\cdots d_{n}]\,$;

  3. (3)

$\mathsf{Pred}_{n}\,@\,[a,d_{1},\dots,d_{n}]\,\twoheadrightarrow_{\mathsf{c}}\langle
R_{0}=a\cdot d_{1}\cdots d_{n},\pol
R,;0\shortleftarrow\mathtt{Pred}(0);\mathtt{Call}~{}0,[]\rangle$;

  4. (4)

$\mathsf{Succ}_{n}\,@\,[a,d_{1},\dots,d_{n}]\,\twoheadrightarrow_{\mathsf{c}}\langle
R_{0}=a\cdot d_{1}\cdots d_{n},\pol
R,;0\shortleftarrow\mathtt{Succ}(0);\mathtt{Call}~{}0,[]\rangle$;

  5. (5)

$\mathsf{Ifz}_{n}\,@\,[a,b,c,d_{1},\dots,d_{n}]\,\twoheadrightarrow_{\mathsf{c}}\langle
R_{0}=a\cdot\pol d,R_{1}=b\cdot\pol d,R_{2}=c\cdot\pol d,\pol
R,0\shortleftarrow\mathtt{Test}(0,\,1,\,2);\mathtt{Call}~{}0,[]\rangle$.

######  Proof 4.2.

Easy. As an example, we give a possible definition of the predecessor:

$\mathsf{Pred}_{n}=\left\langle\begin{aligned}
R_{0},\dots,R_{n},\mathtt{Load}~{}(0,\dots,n);0\shortleftarrow\mathtt{App}(0,\,1);\cdots;0\shortleftarrow\mathtt{App}(0,\,n);0\shortleftarrow\mathtt{Pred}(0);\mathtt{Call}~{}0,[]\end{aligned}\right\rangle$

The others are similar.

######  Lemma 4.3.

The EAMs in the previous lemma can be defined in order to ensure their
typability (for all $n\geq 0$, $\alpha,\beta,\gamma,\delta_{i}\in\mathbb{T}$):

  1. (1)

$\vdash\mathsf{Pr}_{i}^{n}:\pol\delta\to\delta_{i}$, with
$\pol\delta=\delta_{1}\to\cdots\to\delta_{n}$;

  2. (2)

$\vdash\mathsf{Apply}_{n}:(\pol\delta\to\beta\to\alpha)\to(\pol\delta\to\beta)\to\pol\delta\to\alpha$;

  3. (3)

$\vdash\mathsf{Pred}_{n}:(\pol\delta\to\mathsf{int})\to\pol\delta\to\mathsf{int}$;

  4. (4)

$\vdash\mathsf{Succ}_{n}:(\pol\delta\to\mathsf{int})\to\pol\delta\to\mathsf{int}$;

  5. (5)

$\vdash\mathsf{Ifz}_{n}:(\pol\delta\to\mathsf{int})\to(\pol\delta\to\alpha)\to(\pol\delta\to\alpha)\to\pol\delta\to\alpha$;

######  Proof 4.4.

The naive implementations are, in fact, typable.

We will show that, using the auxiliary EAMs given in Lemma 4.3, we can
translate any ${\sf EPCF}$ term into an EAM. In order to proceed by induction,
we first need to define the size of an EPCF term.

######  Definition 4.5.

Let $M$ be an EPCF term and $\sigma$ be an explicit substitution. The sizes
$|{-}|$ of $\sigma$, $M$ and $(\sigma,M)$ are defined by mutual induction,
e.g.

$\begin{array}[]{rclcrcl}|{[]}|&=&0,&&|{(\sigma,M)}|&=&|{\sigma}|+|{M}|,\\\
|{\rho+[x\leftarrow(\rho^{\prime},N)]}|&=&|{\rho}|+|{(\rho^{\prime},N)}|,&&|{\lambda
x.M\langle\sigma\rangle}|&=&|{(\sigma,M)}|+1,\\\ \end{array}$

and the other cases of $|{M}|$ are standard whence they are omitted.

Intuitively, an EPCF term $M$ having $x_{1},\dots,x_{n}$ as free variables is
translated as an EAM $\mathsf{M}$ loading $n$ arguments as input.

######  Definition 4.6.

(Translation) Let $M$ be an EPCF term and $\sigma$ be an explicit substitution
such that $\mathrm{FV}(M)\subseteq\mathrm{dom}(\sigma)\cup\\{\pol x\\}$, where
$\pol x=x_{1},\dots,x_{n}$. The _translation_ of the pair $(\sigma,M)$ (w.r.t
$\pol x$) is a machine denoted $\llparenthesis\sigma,M\rrparenthesis^{\pol
x}\in\mathcal{M}_{\mathbb{A}}$, or simply $\llbracket M\rrbracket^{\pol x}$
when $\sigma$ is empty.222In other words, we set $\llbracket M\rrbracket^{\pol
x}=\llparenthesis[],M\rrparenthesis^{\pol x}$. The machine
$\llparenthesis\sigma,M\rrparenthesis^{\pol x}$ is defined by induction on
$|{(\sigma,M)}|$ as follows:

$\begin{array}[]{lcll}\llparenthesis\sigma+[y\leftarrow(\tau,N)],M\rrparenthesis^{\pol
x}&=&\llparenthesis\sigma,M\rrparenthesis^{y,\pol
x}\,@\,[\\#\llparenthesis\tau,N\rrparenthesis]\,;\\\\[3.44444pt] \llbracket
x_{i}\rrbracket^{\pol x}&=&\mathsf{Pr}_{i}^{n},&\\\\[3.44444pt]
\llbracket\lambda y.M\langle\sigma\rangle\rrbracket^{\pol
x}&=&\llparenthesis\sigma,M\rrparenthesis^{\pol x,y},\textrm{ where wlog
}y\notin\pol x;\\\\[3.44444pt] \llbracket M\cdot N\rrbracket^{\pol
x}&=&\mathsf{Apply}_{n}\,@\,[\\#\llbracket M\rrbracket^{\pol x},\\#\llbracket
N\rrbracket^{\pol x}]\,;\\\\[3.44444pt]
\llbracket\underline{k}\rrbracket^{\pol
x}&=&\mathsf{Pr}_{1}^{n+1}\,@\,[k]\,,\textrm{ where }k\in{\rm
Nature};\\\\[3.44444pt] \llbracket\mathbf{pred}\,M\rrbracket^{\pol
x}&=&\mathsf{Pred}_{n}\,@\,[\\#{\llbracket M\rrbracket^{\pol
x}}]\,;\\\\[3.44444pt] \llbracket\mathbf{succ}\,M\rrbracket^{\pol
x}&=&\mathsf{Succ}_{n}\,@\,[\\#{\llbracket M\rrbracket^{\pol
x}}]\,;\\\\[3.44444pt] \llbracket\mathbf{ifz}(L,M,N)\rrbracket^{\pol
x}&=&\mathsf{Ifz}_{n}\,@\,[\\#{\llbracket L\rrbracket^{\pol x}},\\#{\llbracket
M\rrbracket^{\pol x}},\\#{\llbracket N\rrbracket^{\pol x}}]\,;\\\\[3.44444pt]
\llbracket\mathbf{fix}\,M\rrbracket^{\pol
x}&=&\mathsf{Y}_{n}\,@\,[\\#{\llbracket M\rrbracket^{\pol x}}]\,.\\\
\end{array}$

We show the extended abstract machines associated by this translation to some
of our running examples.

######  Example 4.7.

1\. $\llbracket(\lambda
x.\mathbf{succ}\,(x)\langle\rangle)\cdot\underline{0}\rrbracket=\mathsf{Succ}_{1}\,@\,[\\#\mathsf{Pr}_{1}^{1},0]\,$.

2\. $\llbracket(\lambda sn.s(sn))(\lambda
x.\mathbf{succ}\,(x))\rrbracket=\mathsf{Apply}_{2}\,@\,[\\#\mathsf{Pr}_{1}^{2},\\#(\mathsf{Apply}_{2}\,@\,[\\#\mathsf{Pr}_{1}^{2},\\#\mathsf{Pr}_{2}^{2}]\,),\\#(\mathsf{Succ}_{1}\,@\,[\\#\mathsf{Pr}_{1}^{1}]\,)]\,$.

3\.
$\begin{array}[t]{l}\llbracket\mathbf{add}\rrbracket=\mathsf{Y}_{0}\,@\,\\#\llbracket\lambda
fxy.\mathbf{ifz}(y,x,(f\cdot(\mathbf{succ}\,x)\cdot(\mathbf{pred}\,y)))\rrbracket\\\
=\mathsf{Y}_{0}\,@\,\\#\llbracket\mathbf{ifz}(y,x,(f\cdot(\mathbf{succ}\,x)\cdot(\mathbf{pred}\,y)))\rrbracket^{f,x,y}\,,\\\
=\mathsf{Y}_{0}\,@\,\\#(\mathsf{Ifz}_{3}\,@\,[\\#\mathsf{Pr}_{3}^{3},\\#\mathsf{Pr}_{2}^{3},\\#\llbracket
f\cdot(\mathbf{succ}\,x)\cdot(\mathbf{pred}\,y)\rrbracket^{f,x,y}\,]\,),\\\\[4.30554pt]
\end{array}$
where $\llbracket
f\cdot(\mathbf{succ}\,x)\cdot(\mathbf{pred}\,y)\rrbracket^{f,x,y}=\mathsf{Apply}_{3}\,@\,[\\#{(\mathsf{Apply}_{3}\,@\,[\\#\mathsf{Pr}_{1}^{3},\\#{(\mathsf{Succ}_{3}\,@\,[\\#\mathsf{Pr}_{2}^{3}]\,)}]\,)},\\#{(\mathsf{Pred}_{3}\,@\,[\\#\mathsf{Pr}_{3}^{3}]\,)}]\,$.

######  Theorem 4.8.

Let $M$ be an EPCF term, $\alpha\in\mathbb{T}$,
$\Gamma=x_{1}:\beta_{1},\dots,x_{n}:\beta_{n}$. Then

$\Gamma\vdash^{\mathsf{E}}M:\alpha\quad\Rightarrow\quad\vdash\llbracket
M\rrbracket^{x_{1},\dots,x_{n}}:\beta_{1}\to\cdots\to\beta_{n}\to\alpha.$

######  Proof 4.9.

By induction on a derivation of $\Gamma\vdash^{\mathsf{E}}M:\alpha$. As an
induction loading, one needs to prove simultaneously that for all explicit
substitutions $\sigma$ with $\mathrm{dom}(\sigma)=\\{x_{1},\dots,x_{n}\\}$, if
$\sigma\models x_{1}:\beta_{1},\dots,x_{n}:\beta_{n}$ then
$\vdash\llparenthesis\sigma(x_{i})\rrparenthesis:\beta_{i}$, for all $i\leq
n$.

######  Theorem 4.10.

Let $M$ be an EPCF term and $V\in\mathrm{Val}$. Then

$\sigma\triangleright
M\Downarrow_{d}V\Rightarrow\llparenthesis\sigma,M\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket
V\rrbracket$

######  Proof 4.11.

By induction on a derivation of $\sigma\triangleright M\Downarrow_{d}V$.

######  Corollary 4.12.

For an EPCF program $M$ of type $\vdash^{\mathsf{E}}M:\mathsf{int}$ we have

$[\,]\triangleright\,M\Downarrow_{d}\underline{n}\Rightarrow\llbracket
M\rrbracket\twoheadrightarrow_{\mathsf{c}}\mathsf{n}$

######  Proof 4.13.

Assume that $[\,]\triangleright M\Downarrow_{d}\underline{n}$. By Theorem
4.10, we have
$\llparenthesis[\,],M\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket\underline{n}\rrbracket$.
Since
$\llbracket\underline{n}\rrbracket\twoheadrightarrow_{\mathsf{c}}\mathsf{n}$
and the numeral machine $\mathsf{n}$ is in final state we conclude $\llbracket
M\rrbracket\twoheadrightarrow_{\mathsf{c}}\mathsf{n}$.

###  4.1 Applying the translation to regular PCF

Let us show how to apply our machinery to the usual (call-by-name) PCF. Our
presentation follows [22].

######  Definition 4.14.

  1. (1)

PCF _terms_ are defined by the grammar (for $n\geq 0$, $x\in\mathrm{Var}$):

$P,Q,Q^{\prime}\ ::=~{}\,x\mid P\cdot Q\mid\lambda
x.P\mid\mathbf{0}\mid\mathbf{pred}\,P\mid\mathbf{succ}\,P\mid\mathbf{ifz}(P,Q,Q^{\prime})\mid\mathbf{fix}\,P$

  2. (2)

A closed PCF term $P$ is called a PCF _program_.

  3. (3)

A PCF value $U$ is a term of the form $\lambda x.P$ or $\underline{n}$, for
some $n\geq 0$.

  4. (4)

Given a PCF term $P$ and a value $U$, we write $P\Downarrow U$ if this
judgement can be obtained by applying the rules from Figure 5.

  5. (5)

The set $\mathbb{T}$ of _simple types_ and _typing contexts_ have already been
defined in items (1) and (2) of Definition 1.6, respectively.

  6. (6)

Given a PCF term $P$, a typing context $\Gamma$ and $\alpha\in\mathbb{T}$, we
write $\Gamma\vdash^{\sf PCF}P:\alpha$ if this typing judgement is derivable
from the rules of Figure 6.

$\begin{array}[]{ccc}U\Downarrow
UU\in\mathrm{Val}&\mathbf{pred}\,P\Downarrow\mathbf{0}P\Downarrow\mathbf{0}&\mathbf{pred}\,P\Downarrow\underline{n}P\Downarrow\underline{n+1}\\\\[4.30554pt]
\mathbf{ifz}(P,Q,Q^{\prime})\Downarrow U_{1}\lx@proof@logical@and
P\Downarrow\underline{0}Q\Downarrow
U_{1}&\qquad\mathbf{ifz}(P,Q,Q^{\prime})\Downarrow U_{2}\lx@proof@logical@and
P\Downarrow\underline{n+1}Q^{\prime}\Downarrow
U_{2}&\mathbf{succ}\,P\Downarrow\underline{n+1}P\Downarrow\underline{n}\\\\[4.30554pt]
\mathbf{fix}\,P\Downarrow UP\cdot(\mathbf{fix}\,P)\Downarrow U&P\cdot
Q\Downarrow U\lx@proof@logical@and P\Downarrow\lambda
x.P^{\prime}P^{\prime}[Q/x]\Downarrow U\end{array}$ Figure 5: The big-step
operational semantics of PCF. $\begin{array}[]{ccccccc}\Gamma,x:\alpha\vdash
x:\alpha&&\Gamma\vdash\lambda x.P:\alpha\to\beta\Gamma,x:\alpha\vdash
P:\beta&&\Gamma\vdash\underline{0}:\mathsf{int}&&\Gamma\vdash
PQ:\beta\lx@proof@logical@and\Gamma\vdash P:\alpha\to\beta\Gamma\vdash
Q:\alpha\\\\[4.30554pt]
\Gamma\vdash\mathbf{pred}\,~{}P:\mathsf{int}\Gamma\vdash
P:\mathsf{int}.&&\Gamma\vdash\mathbf{fix}\,P:\alpha\Gamma\vdash
P:\alpha\to\alpha&&\Gamma\vdash\mathbf{succ}\,~{}P:\mathsf{int}\Gamma\vdash
P:\mathsf{int}.&&\Gamma\vdash\mathbf{ifz}(P,Q,Q^{\prime}):\alpha\lx@proof@logical@and\Gamma\vdash
P:\mathsf{int}\Gamma\vdash Q:\alpha\Gamma\vdash Q^{\prime}:\alpha\\\
\end{array}$ Figure 6: The type inference rules of PCF.

Recall that any PCF program $P$ can be seen as an ${\sf EPCF}$ term, thanks to
the notation $\lambda x.N:=\lambda x.N\langle\rangle$. However, the hypotheses
$\vdash^{\sf PCF}P:\mathsf{int}$ and $P\Downarrow\underline{n}$ are _a priori_
not sufficient for applying Corollary 4.12, since one needs to show that also
the corresponding EPCF judgments $\vdash^{\mathsf{E}}P:\mathsf{int}$ and
$P\Downarrow_{d}\underline{n}$ hold. The former is established by the
following lemma.

######  Lemma 4.15.

Let $M$ be a PCF term, $\alpha\in\mathbb{T}$ and $\Gamma$ be a context. Then

$\Gamma\vdash^{{\sf
PCF}}M:\alpha\qquad\Rightarrow\qquad\Gamma\vdash^{\mathsf{E}}M:\alpha$

######  Proof 4.16.

By a straightforward induction on a derivation of $\Gamma\vdash^{{\sf PCF}}M$.

An EPCF term is easily translated into PCF by performing all its explicit
substitutions. The converse is trickier as the representation is not unique:
for every PCF term $P$ there are several decompositions
$P=P^{\prime}[Q_{1}/x_{1},\dots,Q_{n}/x_{n}]$. Recall that the size
$|{(\sigma,M)}|$ has been defined in Definition 4.5.

######  Definition 4.17.

Let $M$ be an EPCF term and $\sigma$ be an explicit substitution. Define a PCF
term $(\sigma,M)^{*}$ by induction on $|{(\sigma,M)}|$ as follows:

$\begin{array}[]{rcl}(\sigma,x)^{*}&=&\begin{cases}\sigma(x)^{*},&\textrm{if
}x\in\mathrm{dom}(\sigma),\\\ x,&\textrm{otherwise},\end{cases}\\\
(\sigma,\lambda x.M\langle\rho\rangle)^{*}&=&\lambda x.(\sigma+\rho,M)^{*},\\\
(\sigma,M\cdot N)^{*}&=&(\sigma,M)^{*}\cdot(\sigma,N)^{*},\\\
(\sigma,\mathbf{fix}\,M)^{*}&=&\mathbf{fix}\,((\sigma,M)^{*}),\\\
(\sigma,\underline{0})^{*}&=&\underline{0},\\\
(\sigma,\mathbf{pred}\,M)^{*}&=&\mathbf{pred}\,(\sigma,M)^{*},\\\
(\sigma,\mathbf{succ}\,M)^{*}&=&\mathbf{succ}\,(\sigma,M)^{*},\\\
(\sigma,\mathbf{ifz}(L,M,N))^{*}&=&\mathbf{ifz}((\sigma,L)^{*},(\sigma,M)^{*},(\sigma,N)^{*}).\\\
\end{array}$

For a PCF term $P$, define $P^{\dagger}=\\{(\sigma,M)\mid(\sigma,M)^{*}=P\\}$.

To show the equivalence between PCF and EPCF, we need yet another auxiliary
lemma.

######  Lemma 4.18 (Substitution Lemma).

  1. (1)

Let $M,N$ be EPCF terms, $\sigma,\rho$ be explicit substitutions and $x$ be a
variable.

$(\sigma+[x\leftarrow(\rho,N)],M)^{*}=(\sigma,M)^{*}[(\rho,N)^{*}/x]$

  2. (2)

Let $P,Q$ be PCF terms with $\mathrm{FV}(P)\subseteq\\{x\\}$ and $Q$ closed.
For all EPCF terms $M,N$ and explicit substitutions $\sigma,\rho$, we have:

$(\sigma,M)\in P^{\dagger}\land(\rho,N)\in
Q^{\dagger}\Rightarrow(\sigma+[x\leftarrow(\rho,N)],M)\in(P[Q/x])^{\dagger}$

We rely on the freshness hypothesis on the variables in
$\mathrm{dom}(\sigma)$.

######  Proof 4.19.

(i) By structural induction on $M$.

Case $M=y$, with $y\neq x$:

There are two subcases.

  * •

If $y\in\mathrm{dom}(\sigma)$, then
$(\sigma+[x\leftarrow(\rho,N)],y)^{*}=\sigma(y)=\sigma(y)[(\rho,N)^{*}/x]=(\sigma,y)^{*}[(\rho,N)^{*}/x]$,
since $x\notin\mathrm{FV}(\sigma(y))$;

  * •

if $y\notin\mathrm{dom}(\sigma)$, then
$(\sigma+[x\leftarrow(\rho,N)],y)^{*}=y=y[(\rho,N)^{*}/x]=(\sigma,y)^{*}[(\rho,N)^{*}/x]$.

Case $M=x$:

Then
$(\sigma+[x\leftarrow(\rho,N)],x)^{*}=(\rho,N)^{*}=x[(\rho,N)^{*}/x]=(\sigma,x)^{*}[(\rho,N)^{*}/x].$

Case $M=\lambda y.M^{\prime}$:

Wlog, we may assume $y\neq x$. We have $(\sigma+[x\leftarrow(\rho,N)],\lambda
y.M^{\prime})^{*}=\lambda
y.(\sigma+[x\leftarrow(\rho,N)],M^{\prime})^{*}=\lambda
y.((\sigma,M^{\prime})^{*}[(\rho,N)^{*}/x])=(\lambda
y.(\sigma,M^{\prime})^{*})[(\rho,N)^{*}/x]=((\sigma,\lambda
y.M^{\prime})^{*})[(\rho,N)^{*}/x].$

All other cases derive straightforwardly from the IH.

(ii) By an easy induction on $P$, using (1).

######  Theorem 4.20.

The big-step weak reduction of EPCF is equivalent to the usual big-step
operational semantics of PCF. Formally:

  1. (1)

Given an EPCF program $M$, a value $V$ and an explicit substitution $\sigma$,
we have:

$\sigma\triangleright
M\Downarrow_{d}V\quad\Rightarrow\quad(\sigma,M)^{*}\Downarrow([\,],V)^{*}$

  2. (2)

Given a PCF program $P$ and PCF value $U$. If $P\Downarrow U$ then

$\forall(\sigma,M)\in P^{\dagger},\,\exists V\in\mathrm{Val}\,.\,(\
\sigma\triangleright M\Downarrow_{d}V\textrm{ and }([\,],V)\in U^{\dagger}\ )$

######  Proof 4.21.

(Proof sketch) For the full proof, we refer to the technical Appendix A.

(i) Proceed by induction on a derivation of $\sigma\triangleright
M\Downarrow_{d}V$, using Lemma 4.18(1) in the $(\beta_{v})$-case.

(ii) By induction on the lexicographically ordered pairs, whose first
component is the length of a derivation of $P\Downarrow U$ and second
component is $|{(\sigma,M)}|$, using Lemma 4.18(2) in the $(\beta_{v})$-case.

As promised, we now draw conclusions for the regular PCF. As customary in PCF,
we are interested on the properties of closed terms having ground type.

######  Theorem 4.22.

For a PCF program $P$ of type $\mathsf{int}$, $P\Downarrow\underline{n}$
entails $\llbracket P\rrbracket\twoheadrightarrow_{\mathsf{c}}\mathsf{n}$.

######  Proof 4.23.

Note that $P$ is also an ${\sf EPCF}$ term such that $([],P)\in P^{\dagger}$,
and that $\vdash^{\mathsf{E}}P:\mathsf{int}$ by Lemma 4.15. Thus
$[\,]\triangleright\,P\Downarrow_{d}\underline{n}$ by Theorem 4.20(2).
Conclude by Corollary 4.12.

## References

  * [1] Abadi, M., L. Cardelli, P.-L. Curien and J.-J. Lévy, _Explicit substitutions_ , in: F. E. Allen, editor, _Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990_ (1990), pp. 31–46.
URL https://doi.org/10.1145/96709.96712

  * [2] Abadi, M., L. Cardelli, P.-L. Curien and J.-J. Lévy, _Explicit substitutions_ , J. Funct. Program. 1 (1991), pp. 375–416.
URL https://doi.org/10.1017/S0956796800000186

  * [3] Abramsky, S., R. Jagadeesan and P. Malacaria, _Full abstraction for PCF_ , Inf. Comput. 163 (2000), pp. 409–470.
URL https://doi.org/10.1006/inco.2000.2930

  * [4] Abramsky, S., P. Malacaria and R. Jagadeesan, _Full abstraction for PCF_ , in: M. Hagiya and J. C. Mitchell, editors, _Theoretical Aspects of Computer Software, International Conference TACS ’94, Sendai, Japan, April 19-22, 1994, Proceedings_ , Lecture Notes in Computer Science 789 (1994), pp. 1–15.
URL https://doi.org/10.1007/3-540-57887-0_87

  * [5] Berry, G., P.-L. Curien and J.-J. Lévy, _Full abstraction for sequential languages: state of the art_ , in: M. Nivat and J. Reynolds, editors, _Algebraic methods in semantics_ , Cambridge University Press, 1985 pp. 89–132.
  * [6] Cregut, P., “Machines a environnement pour la reduction symbolique et l’evaluation partielle,” Ph.D. thesis, Université Paris-Diderot (Paris VII) (1991), in French.
URL http://www.theses.fr/1991PA077152

  * [7] Curien, P., _Definability and full abstraction_ , Electron. Notes Theor. Comput. Sci. 172 (2007), pp. 301–310.
URL https://doi.org/10.1016/j.entcs.2007.02.011

  * [8] Curien, P.-L., _Observable algorithms on concrete data structures_ , in: _Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS ’92), Santa Cruz, California, USA, June 22-25, 1992_ (1992), pp. 432–443.
URL https://doi.org/10.1109/LICS.1992.185554

  * [9] Curien, P.-L., T. Hardin and J.-J. Lévy, _Confluence properties of weak and strong calculi of explicit substitutions_ , J. ACM 43 (1996), pp. 362–397.
URL https://doi.org/10.1145/226643.226675

  * [10] Della Penna, G., “Una semantica operazionale per il network computing: le macchine di Turing virtuali,” Master’s thesis, Università degli Studi di L’Aquila (1996-97), in Italian.
  * [11] Della Penna, G., B. Intrigila and G. Manzonetto, _Addressing machines as models of lambda-calculus_ , Log. Methods Comput. Sci. 18 (2022).
  * [12] Fairbairn, J. and S. Wray, _Tim: A simple, lazy abstract machine to execute supercombinators_ , in: G. Kahn, editor, _Functional Programming Languages and Computer Architecture_ (1987), pp. 34–45.
  * [13] Hyland, J. M. E. and C. L. Ong, _On full abstraction for PCF: I, II, and III_ , Inf. Comput. 163 (2000), pp. 285–408.
URL https://doi.org/10.1006/inco.2000.2917

  * [14] Intrigila, B., G. Manzonetto and N. Münnich, _Extended addressing machines a comparative view_ (2022).
URL https://lipn.univ-paris13.fr/~gmanzonetto/papers/NotesIMM22

  * [15] Krivine, J.-L., _A call-by-name lambda-calculus machine_ , Higher Order Symbol. Comput. 20 (2007), p. 199–207.
URL https://doi.org/10.1007/s10990-007-9018-9

  * [16] Landin, P. J., _The Mechanical Evaluation of Expressions_ , The Computer Journal 6 (1964), pp. 308–320.
URL https://doi.org/10.1093/comjnl/6.4.308

  * [17] Lang, F., _Explaining the lazy Krivine machine using explicit substitution and addresses_ , Higher-Order and Symbolic Computation (2007).
URL https://hal.inria.fr/inria-00198756

  * [18] Leroy, X., _The ZINC experiment: an economical implementation of the ML language_ , Technical report 117, INRIA (1990).
  * [19] Lévy, J.-J. and L. Maranget, _Explicit substitutions and programming languages_ , in: C. P. Rangan, V. Raman and R. Ramanujam, editors, _Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings_ , Lecture Notes in Computer Science 1738 (1999), pp. 181–200.
URL https://doi.org/10.1007/3-540-46691-6_14

  * [20] Longley, J., “Realizability toposes and language semantics,” Ph.D. thesis, University of Edinburgh (1995).
  * [21] Milner, R., _Fully abstract models of typed $\lambda$-calculi_, Theor. Comput. Sci. 4 (1977), pp. 1–22.
URL https://doi.org/10.1016/0304-3975(77)90053-6

  * [22] Ong, C.-H. L., _Correspondence between operational and denotational semantics of PCF_ , in: S. Abramsky, D. Gabbay and T. S. E. Maibaum, editors, _Semantic Modelling_ , Handbook of Logic in Computer Science 4, Oxford University Press, 1995 pp. 269–356.
  * [23] Plotkin, G. D., _LCF considered as a programming language_ , Theor. Comput. Sci. 5 (1977), pp. 223–255.
URL https://doi.org/10.1016/0304-3975(77)90044-5

  * [24] Seaman, J. and S. P. Iyer, _An operational semantics of sharing in lazy evaluation_ , Sci. Comput. Program. 27 (1996), pp. 289–322.
URL https://doi.org/10.1016/0167-6423(96)00012-3

##  Appendix A Technical Appendix

This technical appendix is devoted to provide the proofs that have been
partially given, or completely omitted, in the body of the paper. As an
abbreviation, we write IH for “induction hypothesis”.

###  A.1 Proofs of Section 1

######  Proof A.1 (Proof of Lemma 1.8).

Items (1) and (2) are straightforward. We prove (3).

Given an EPCF term $M$, an EPCF value $V$, an explicit substitution $\sigma$,
a type $\alpha$, and a context $\Gamma$ such that $\sigma\triangleright
M\Downarrow_{d}V,\sigma\models\Gamma,\Gamma\vdash M:\alpha$, we prove by
induction on a derivation of $\sigma\triangleright M\Downarrow_{d}V$ that
$\vdash V:\alpha$.

Case $(\mathrm{nat})$:

In this case $M=V=\underline{n}$, for $\underline{n}\in{\rm Nature}$, and
$\alpha=\mathsf{int}$. By the typing rules of EPCF,
$\vdash\underline{n}:\mathsf{int}$.

Case $(\mathrm{fun})$:

In this case $M=\lambda x.M^{\prime}\langle\rho\rangle,V=\lambda
x.M^{\prime}\langle\sigma+\rho\rangle,\alpha=\beta\rightarrow\gamma$. As
$\Gamma\vdash\lambda x.M^{\prime}\langle\rho\rangle:\beta\rightarrow\gamma$,
$\exists!\Delta$ such that $\rho\models\Delta,\Gamma,\Delta,x:\beta\vdash
M^{\prime}:\gamma$. As $\sigma\models\Gamma$ and $\rho\models\Delta$,
$\sigma+\rho\models\Gamma,\Delta$. Thus by the typing rules of EPCF,
$\vdash\lambda x.M^{\prime}\langle\sigma+\rho\rangle:\beta\rightarrow\gamma$.

Case $(\mathrm{var})$:

In this case $M=x,\sigma(x)=(\rho,N),\Gamma=\Gamma^{\prime},x:\alpha$. By the
operational semantics of EPCF, $\rho\triangleright N\Downarrow_{d}V$, and by
the type system of EPCF as $\sigma\models\Gamma^{\prime},x:\alpha$,
$[x\leftarrow(\rho,N)]\models x:\alpha$ and thus
$\rho\models\Delta,\Delta\vdash N:\alpha$. By IH, $\vdash V:\alpha$.

Case $(\beta_{v})$:

In this case $M=N\cdot L$. By the operational semantics of EPCF,
$\sigma\triangleright N\Downarrow_{d}\lambda x.N^{\prime}\langle\rho\rangle$
and $\rho+[x\leftarrow(\sigma,L)]\triangleright N^{\prime}\Downarrow_{d}V$. By
the type system of EPCF, $\Gamma\vdash N:\beta\rightarrow\alpha$,
$\Gamma\vdash L:\beta$. By IH, $\vdash\lambda
x.N^{\prime}\langle\rho\rangle:\beta\rightarrow\alpha$, and then by the type
system of EPCF $\rho\models\Delta,\Delta,x:\beta\vdash N^{\prime}:\alpha$. By
the type system we also have $[x\leftarrow(\sigma,L)]\models x:\beta$, so
$\rho+[x\leftarrow(\sigma,L)]\models\Delta,x:\beta$, and thus by IH we
conclude $\vdash V:\alpha$.

All other cases derive straightforwardly from applying the rules of the type
system and the IH.

###  A.2 Proofs of Section 4

######  Proof A.2 (Proof of Theorem 4.8).

We prove the following statements by mutual induction and call the respective
inductive hypotheses IH1 and IH2.

  1. (i)

Let $M$ be an EPCF term, $\Gamma=x_{1}:\beta_{1},\dots,x_{n}:\beta_{n}$ and
$\alpha\in\mathbb{T}$. Then $\Gamma\vdash
M:\alpha\quad\Rightarrow\quad\vdash\llbracket
M\rrbracket^{x_{1},\dots,x_{n}}:\beta_{1}\to\cdots\to\beta_{n}\to\alpha.$

  2. (ii)

For all $\Gamma=x_{1}:\beta_{1},\dots,x_{n}:\beta_{n}$ and $\sigma$, with
$\mathrm{dom}(\sigma)=\\{x_{1},\dots,x_{n}\\}$, we have
$\sigma\models\Gamma\quad\Rightarrow\quad\vdash\llparenthesis\sigma(x_{1})\rrparenthesis:\beta_{1},\dots,\vdash\llparenthesis\sigma(x_{n})\rrparenthesis:\beta_{n}.$

We start with the cases concerning i.

Case $(\mathrm{ax})$:

Then, $x_{1}:\beta_{1},\dots,x_{n}:\beta_{n}\vdash x_{i}:\beta_{i}$, and
$\llbracket x_{i}\rrbracket^{x_{1},\dots,x_{n}}=\mathsf{Pr}_{i}^{n}.$ By Lemma
4.3(1) we conclude
$\vdash\mathsf{Pr}_{i}^{n}:\beta_{1}\to\dots\to\beta_{n}\to\beta_{i}$.

Case $(0)$:

In this case, we have $\Gamma\vdash\mathbf{0}:\mathsf{int}$ and
$\llbracket\mathbf{0}\rrbracket^{x_{1},\dots,x_{n}}=\mathsf{Pr}_{1}^{n+1}\,@\,[0]\,.$
By Lemma 4.3(1)
$\vdash\mathsf{Pr}_{1}^{n+1}\,@\,:\,\mathsf{int}\to\beta_{1}\to\dots\to\beta_{n}\to\mathsf{int}$
and, by Figure 4 $\vdash\\#^{-1}(0):\mathsf{int}$. By Proposition 3.6(1),
$\vdash\mathsf{Pr}_{1}^{n+1}\,@\,[{0}]\,:\beta_{1}\to\dots\to\beta_{n}\to\mathsf{int}$.

Case $(\mathrm{Y})$:

In this case $\Gamma\vdash\mathbf{fix}\,M^{\prime}:\alpha$ and
$\llbracket\mathbf{fix}\,M^{\prime}\rrbracket^{\pol
x}=\mathsf{Y}_{n}\,@\,[\\#{\llbracket M^{\prime}\rrbracket^{\pol x}}]\,$. By
$(\mathrm{fix}_{n})$ in Figure 4, we have
$\vdash\mathsf{Y}_{n}:(\pol\beta\to\alpha\to\alpha)\to\pol\beta\to\alpha$.
From the hypothesis IH1, we obtain $\vdash\llbracket
M^{\prime}\rrbracket^{x_{1},\dots,x_{n}}:\pol\beta\to\alpha\to\alpha$. By
Proposition 3.6(1), we conclude that $\vdash\mathsf{Y}_{n}\,@\,[\\#{\llbracket
M^{\prime}\rrbracket^{x_{1},\dots,x_{n}}}]\,:\beta_{1}\to\dots\to\beta_{n}\to\alpha$.

Case $(+)$:

In this case $\Gamma\vdash\mathbf{succ}\,{M^{\prime}}:\mathsf{int}$ since
$\Gamma\vdash{M^{\prime}}:\mathsf{int}$. By definition,
$\llbracket\mathbf{succ}\,M^{\prime}\rrbracket^{x_{1},\dots,x_{n}}=\mathsf{Succ}_{n}\,@\,[\\#\llbracket
M^{\prime}\rrbracket^{x_{1},\dots,x_{n}}]\,$. By Lemma 4.3(4),
$\vdash\mathsf{Succ}_{n}:(\pol\beta\to\mathsf{int})\to\pol\beta\to\mathsf{int}$.
From IH1, we get $\vdash\llbracket
M^{\prime}\rrbracket^{x_{1},\dots,x_{n}}:\pol\beta\to\mathsf{int}$, and thus
by Proposition 3.6(1), we conclude
$\vdash\mathsf{Succ}_{n}\,@\,[\\#{\llbracket
M^{\prime}\rrbracket^{x_{1},\dots,x_{n}}}]\,:\pol\beta\to\mathsf{int}.$

Case $(-)$:

Analogous, applying Lemma 4.3(4).

Case $(\mathrm{ifz})$:

Assume $\Gamma\vdash\mathbf{ifz}(L,N_{1},N_{2}):\alpha$ since $\Gamma\vdash
L:\mathsf{int}$ and $\Gamma\vdash N_{i}:\alpha$, for $i\in\\{1,2\\}$. By
definition of the translation, we have
$\llbracket\mathbf{ifz}(L,N_{2},N_{2})\rrbracket^{\pol
x}=\mathsf{Ifz}_{n}\,@\,[\\#\llbracket L\rrbracket^{\pol x},\\#\llbracket
N_{1}\rrbracket^{\pol x},\\#\llbracket N_{2}\rrbracket^{\pol x}]\,.$ By
applying Lemma 4.3(5), we obtain
$\vdash\mathsf{Ifz}_{n}:(\pol\beta\to\mathsf{int})\to(\pol\beta\to\alpha)\to(\pol\beta\to\alpha)\to\pol\beta\to\alpha$.
By the hypothesis IH1, we get $\vdash\llbracket L\rrbracket^{\pol
x}:\pol\beta\to\mathsf{int}$ and $\vdash\llbracket N_{i}\rrbracket^{\pol
x}:\pol\beta\to\alpha$ for $i\in\\{1,2\\}$, and thus by Proposition 3.6(1), we
conclude $\vdash\mathsf{Ifz}_{n}\,@\,[\\#\llbracket L\rrbracket^{\pol
x},\\#\llbracket N_{1}\rrbracket^{\pol x},\\#\llbracket N_{2}\rrbracket^{\pol
x}]\,:\pol\beta\to\alpha$.

Case $(\to_{\mathrm{I}})$:

Assume that $\Gamma\vdash\lambda
z.M^{\prime}\langle\sigma\rangle:\alpha_{1}\to\alpha_{2}$, for
$\alpha=\alpha_{1}\to\alpha_{2}$, because there is
$\Delta=y_{1}:\delta_{1},\dots,y_{m}:\delta_{m}$ such that
$\sigma\models\Delta$ and $\Gamma,\Delta,z:\alpha_{1}\vdash
M^{\prime}:\alpha_{2}$. Then $\sigma\models\Delta$ entails
$\sigma=[y_{1}\leftarrow(\rho_{1},N_{1}),\dots,y_{m}\leftarrow(\rho_{m},N_{m})]$
for appropriate $\pol\rho,\pol N$. By definition, we have $\llbracket\lambda
z.M^{\prime}\langle\sigma\rangle\rrbracket^{x_{1},\dots,x_{n}}=\llparenthesis\sigma,M^{\prime}\rrparenthesis^{\pol
x,z}=\llbracket M^{\prime}\rrbracket^{y_{1},\dots,y_{m},\pol
x,z}\,@\,[\\#\llparenthesis\rho_{1},N_{1}\rrparenthesis,\dots,\\#\llparenthesis\rho_{m},N_{m}\rrparenthesis]\,.$
By applying IH1, we obtain $\vdash\llbracket M^{\prime}\rrbracket^{\pol y,\pol
x,z}:\pol\delta\to\pol\beta\to\alpha_{1}\to\alpha_{2}$. From IH2, we get
$\vdash\llparenthesis\sigma_{1},N_{1}\rrparenthesis:\delta_{1}\dots\vdash\llparenthesis\sigma_{m},N_{m}\rrparenthesis:\delta_{m}$.
Finally, by Proposition 3.6(1), we derive $\vdash\llbracket
M^{\prime}\rrbracket^{\pol y,\pol
x,z}\,@\,[\\#\llparenthesis\sigma_{1},N_{1}\rrparenthesis,\dots,\\#\llparenthesis\sigma_{m},N_{m}\rrparenthesis]\,:\pol\beta\to\alpha_{1}\to\alpha_{2}$.

Case $(\to_{\mathrm{E}})$:

In this case $\Gamma\vdash M_{1}\cdot M_{2}:\alpha$ since, for some
$\delta\in\mathbb{T}$, $\Gamma\vdash M_{1}:\delta\to\alpha$ and $\Gamma\vdash
M_{2}:\delta$. By definition, $\llbracket M_{1}\cdot M_{2}\rrbracket^{\pol
x}=\mathsf{Apply}_{n}\,@\,[\\#\llbracket M_{1}\rrbracket^{\pol
x},\\#\llbracket M_{2}\rrbracket^{\pol x}]\,.$ By Lemma 4.3(2), we get
$\vdash\mathsf{Apply}_{n}:(\pol\beta\to\delta\to\alpha)\to(\pol\beta\to\delta)\to\pol\beta\to\alpha$.
By IH1, we obtain $\vdash\llbracket M_{1}\rrbracket^{\pol
x}:\pol\beta\to\delta\to\alpha$ and $\vdash\llbracket M_{2}\rrbracket^{\pol
x}:\pol\beta\to\delta$. Conclude, by Proposition 3.6(1), that
$\vdash\mathsf{Apply}_{n}\,@\,[\\#\llbracket M_{1}\rrbracket^{\pol
x},\\#\llbracket M_{2}\rrbracket^{\pol x}]\,:\pol\beta\to\alpha$.

We now consider the cases concerning ii.

Case $(\sigma_{0})$

: In this case $[\,]\models\emptyset$, so we have nothing to prove.

Case $(\sigma)$:

In this case $\Gamma=\Gamma^{\prime},x_{n}:\beta_{n}$ and
$\sigma=\sigma^{\prime}+[x_{n}\leftarrow(\rho,N)]\models\Gamma^{\prime},x_{n}:\beta_{n}$,
because $\sigma^{\prime}\models\Gamma^{\prime}$, $\rho\models\Delta$ and
$\Delta\vdash N:\beta_{n}$, for some
$\Delta=y_{1}:\delta_{1},\dots,y_{m}:\delta_{m}$. By IH2 on
$\sigma^{\prime}\models\Gamma^{\prime}$, we get
$\llparenthesis\sigma(x_{i})\rrparenthesis=\llparenthesis\sigma^{\prime}(x_{i})\rrparenthesis:\beta_{i}$,
for all $i\in\\{1,\dots,n-1\\}$. We show
$\llparenthesis(\rho,N)\rrparenthesis:\beta_{n}$. By IH1, we get
$\vdash\llbracket
N\rrbracket^{y_{1},\dots,y_{m}}:\delta_{1}\to\cdots\to\delta_{m}\to\beta_{n}$.
By applying IH2 on $\rho\models\Delta$, we get
$\llparenthesis\rho(y_{j})\rrparenthesis:\delta_{j}$, for all
$j\in\\{1,\dots,m\\}$. Since $\llparenthesis\rho,N\rrparenthesis=\llbracket
N\rrbracket^{\pol
y}\,@\,[\\#\llparenthesis\rho(y_{1})\rrparenthesis,\dots,\\#\llparenthesis\rho(y_{m})\rrparenthesis]\,$,
we conclude $\vdash\llparenthesis\rho,N\rrparenthesis:\beta_{n}$, by
Proposition 3.6(1).

######  Proof A.3 (Proof of Theorem 4.10).

We prove $\sigma\triangleright
M\Downarrow_{d}V\Rightarrow\llparenthesis\sigma,M\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket
V\rrbracket$ by induction on a derivation of $\sigma\triangleright
M\Downarrow_{d}V$. We let $\mathrm{dom}(\sigma)=\\{x_{1},\dots,x_{n}\\}$ and
sometimes use the convenient notation $\\#\llparenthesis\sigma(\pol
x)\rrparenthesis=\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis.$

Case $(\mathrm{nat})$:

Then $M=V=\underline{k}$, for some $k\geq 0$. Recall that we assume
$k=\\#\mathsf{k}$. Then using Lemma 4.1(1),
$\llparenthesis\sigma,\underline{k}\rrparenthesis=\llbracket\underline{k}\rrbracket^{x_{1},\dots,x_{n}}\,@\,[\\#\llparenthesis\sigma(\pol
x)\rrparenthesis]\,=\mathsf{Pr}_{1}^{n+1}\,@\,[k,\\#\llparenthesis\sigma(\pol
x)\rrparenthesis]\,\twoheadrightarrow_{\mathsf{c}}\\#^{-1}(k){}_{\mathsf{c}}\\!\\!\twoheadleftarrow\mathsf{Pr}_{1}^{1}\,@\,[k]\,=\llbracket\underline{k}\rrbracket$

Case 2: $(\mathrm{fun})$

We have $M=\lambda z.M^{\prime}\langle\rho\rangle$ and $V=\lambda
x.M^{\prime}\langle\sigma+\rho\rangle$, with
$\mathrm{dom}(\sigma)\cap\mathrm{dom}(\rho)=\emptyset$. Say,
$\mathrm{dom}(\rho)=\\{y_{1},\dots,y_{m}\\}$. Then

$\displaystyle\llparenthesis\sigma,\lambda
z.M^{\prime}\langle\rho\rangle\rrparenthesis$ $\displaystyle=\llbracket\lambda
z.M^{\prime}\langle\rho\rangle\rrbracket^{x_{1},\dots,x_{n}}\,@\,[\\#\llparenthesis\sigma(\pol
x)\rrparenthesis]\,=\llparenthesis\rho,M^{\prime}\rrparenthesis^{\pol
x,z}\,@\,[\\#\llparenthesis\sigma(\pol x)\rrparenthesis]\,$
$\displaystyle=\llbracket M^{\prime}\rrbracket^{\pol y,\pol
x,z}\,@\,[\\#\llparenthesis\rho(\pol
y)\rrparenthesis,\\#\llparenthesis\sigma(\pol
x)\rrparenthesis]\,=\llparenthesis\sigma+\rho,M^{\prime}\rrparenthesis^{z}=\llbracket\lambda
z.M^{\prime}\langle\sigma+\rho\rangle\rrbracket$

The case follows by reflexivity of $\leftrightarrow_{\mathsf{c}}$.

Case $(\mathrm{var})$:

We have $M=x_{i}$, $\sigma(x_{i})=(\rho,N)$ and $\rho\triangleright
N\Downarrow_{d}V$. Then, using Lemma 4.1(1), we have
$\llparenthesis\sigma,x_{i}\rrparenthesis=\llbracket
x_{i}\rrbracket^{x_{1},\dots,x_{n}}\,@\,[\\#\llparenthesis\sigma(\pol
x)\rrparenthesis]\,=\mathsf{Pr}_{i}^{n}\,@\,[\\#\llparenthesis\sigma(\pol
x)\rrparenthesis]\,\twoheadrightarrow_{\mathsf{c}}\llparenthesis\sigma(x_{i})\rrparenthesis=\llparenthesis\rho,N\rrparenthesis$
We conclude since, by IH, we have
$\llparenthesis\rho,N\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket
V\rrbracket$.

Case $(\beta_{v})$:

$M=M_{1}\cdot M_{2}$, $\sigma\triangleright M_{1}\Downarrow_{d}\lambda
z.M_{1}^{\prime}\langle\rho\rangle$ and
$\rho+[z\leftarrow(\sigma,M_{2})]\triangleright
M_{1}^{\prime}\Downarrow_{d}V$. Easy calculations give:

$\displaystyle\llparenthesis\sigma,M_{1}\cdot M_{2}\rrparenthesis$
$\displaystyle=$ $\displaystyle\llbracket M_{1}\cdot
M_{2}\rrbracket^{x_{1},\dots,x_{n}}\,@\,[\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\,$
$\displaystyle=$ $\displaystyle\mathsf{Apply}_{n}\,@\,[\llbracket
M_{1}\rrbracket^{\pol x},\\#\llbracket M_{2}\rrbracket^{\pol
x},\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\,$
$\displaystyle\twoheadrightarrow_{\mathsf{c}}$ $\displaystyle\llbracket
M_{1}\rrbracket^{\pol x}\,@\,[\\#\llparenthesis\sigma(\pol
x)\rrparenthesis,\\#{(\llbracket M_{2}\rrbracket^{\pol
x}\,@\,[\\#\llparenthesis\sigma(\pol x)\rrparenthesis]\,)}]\,,$
$\displaystyle\textrm{by
Lemma~{}\ref{lem:existenceofeams}\eqref{lem:existenceofeams2}},$
$\displaystyle=$
$\displaystyle\llparenthesis\sigma,M_{1}\rrparenthesis\,@\,[\\#{\llparenthesis\sigma,M_{2}\rrparenthesis}]\,$

By IH on $\sigma\triangleright M_{1}\Downarrow_{d}\lambda
z.M_{1}^{\prime}\langle\rho\rangle$, we have
$\llparenthesis\sigma,M_{1}\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket\lambda
z.M_{1}^{\prime}\langle\rho\rangle\rrbracket=\llparenthesis\rho,M_{1}^{\prime}\rrparenthesis^{z}$.
Calling $\mathrm{dom}(\rho)=\\{y_{1},\dots,y_{m}\\}$, we get

$\displaystyle\llparenthesis\sigma,M_{1}\rrparenthesis\,@\,[\\#{\llparenthesis\sigma,M_{2}\rrparenthesis}]\,$
$\displaystyle\leftrightarrow_{\mathsf{c}}\llparenthesis\rho,M_{1}^{\prime}\rrparenthesis^{z}\,@\,[\\#{\llparenthesis\sigma,M_{2}\rrparenthesis}]\,,$
$\displaystyle\textrm{by def.\ of $\leftrightarrow_{\mathsf{c}}$ and
Lemma~{}\ref{lem:reduction}},$ $\displaystyle=\llbracket
M_{1}^{\prime}\rrbracket^{y_{1},\dots,y_{m},z}\,@\,[\\#\llparenthesis\rho(\pol
y)\rrparenthesis,\\#{\llparenthesis\sigma,M_{2}\rrparenthesis}]\,$
$\displaystyle=\llparenthesis\rho+[z\leftarrow(\sigma,M_{2})],M_{1}^{\prime}\rrparenthesis$

By IH conclude
$\llparenthesis\rho+[z\leftarrow(\sigma,M_{2})],M_{1}^{\prime}\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket
V\rrbracket$.

Case $(\mathrm{pr})$:

$M=\mathbf{pred}\,M^{\prime}$, $V=\underline{n}$ and $\sigma\triangleright
M^{\prime}\Downarrow_{d}\underline{n+1}$, for some $n\geq 0$. By IH we get
$\llparenthesis\sigma,M^{\prime}\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket\underline{n+1}\rrbracket=\\#^{-1}(n+1)$
and, since the $(n+1)$-th numeral machine is in final state, we derive
$\llparenthesis\sigma,M^{\prime}\rrparenthesis\twoheadrightarrow_{\mathsf{c}}\\#^{-1}(n+1)$.
Conclude as follows:

$\begin{array}[]{rll}\llparenthesis\sigma,\mathbf{pred}\,M^{\prime}\rrparenthesis=&\llbracket\mathbf{pred}\,M^{\prime}\rrbracket^{x_{1},\dots,x_{n}}\,@\,[\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
=&\mathsf{Pred}_{n}\,@\,[\\#\llbracket
M^{\prime}\rrbracket^{x_{1},\dots,x_{n}},\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
\twoheadrightarrow_{\mathsf{c}}&\langle R_{0}=\\#(\llbracket
M^{\prime}\rrbracket^{\pol x}\,@\,[\\#\llparenthesis\sigma(\pol
x)\rrparenthesis]\,),\pol
R,0\shortleftarrow\mathtt{Pred}(0);\mathtt{Call}~{}0,[]\rangle,&\textrm{by
Lemma~{}\ref{lem:existenceofeams}\eqref{lem:existenceofeams3},}\\\ =&\langle
R_{0}=\\#\llparenthesis\sigma,M^{\prime}\rrparenthesis,\pol
R,;0\shortleftarrow\mathtt{Pred}(0);\mathtt{Call}~{}0,[]\rangle\\\
\twoheadrightarrow_{\mathsf{c}}&\langle R_{0}=n+1,\pol
R,0\shortleftarrow\mathtt{Pred}(0);\mathtt{Call}~{}0,[]\rangle\twoheadrightarrow_{\mathsf{c}}\\#^{-1}(n)\end{array}$

Case $(\mathrm{pr_{0}})$:

Analogous to the previous case, using the fact that $\mathtt{Pred}(0)$ is 0.

Case 7: $(\mathrm{sc})$

$M=\mathbf{succ}\,M^{\prime}$, $V=\underline{n+1}$ and $\sigma\triangleright
M^{\prime}\Downarrow_{d}\underline{n}$, for some $n\geq 0$. By IH we get
$\llparenthesis\sigma,M^{\prime}\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket\underline{n}\rrbracket=\\#^{-1}(n)$
and, since the $n$-th numeral machine is in final state, we derive
$\llparenthesis\sigma,M^{\prime}\rrparenthesis\twoheadrightarrow_{\mathsf{c}}\\#^{-1}(n)$.
Conclude as follows:

$\begin{array}[]{rlll}\llparenthesis\sigma,\mathbf{succ}\,M^{\prime}\rrparenthesis&=&\llbracket\mathbf{succ}\,M^{\prime}\rrbracket^{x_{1},\dots,x_{n}}\,@\,[\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
&=&\mathsf{Succ}_{n}\,@\,[\\#\llbracket
M^{\prime}\rrbracket^{x_{1},\dots,x_{n}},\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
&\twoheadrightarrow_{\mathsf{c}}&\langle R_{0}=\\#(\llbracket
M^{\prime}\rrbracket^{\pol x}\,@\,[\\#\llparenthesis\sigma(\pol
x)\rrparenthesis]\,),\pol
R,0\shortleftarrow\mathtt{Succ}(0);\mathtt{Call}~{}0,[]\rangle,&\textrm{by
Lemma~{}\ref{lem:existenceofeams}\eqref{lem:existenceofeams3},}\\\ &=&\langle
R_{0}=\\#\llparenthesis\sigma,M^{\prime}\rrparenthesis,\pol
R,;0\shortleftarrow\mathtt{Succ}(0);\mathtt{Call}~{}0,[]\rangle\\\
&\twoheadrightarrow_{\mathsf{c}}&\langle R_{0}=n,\pol
R,0\shortleftarrow\mathtt{Succ}(0);\mathtt{Call}~{}0,[]\rangle\twoheadrightarrow_{\mathsf{c}}&\\#^{-1}(n+1)\\\
\end{array}$

Case 8: $(\mathrm{ifz_{>0}})$

$M=\mathbf{ifz}(L,N_{1},N_{2})$, $\sigma\triangleright
L\Downarrow_{d}\underline{n+1}$, $\sigma\triangleright N_{2}\Downarrow_{d}V$
for some $n\geq 0$. By IH we get
$\llparenthesis\sigma,L\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket\underline{n+1}\rrbracket$,
and since the $(n+1)$-th numeral machine is in final state, we derive
$\llparenthesis\sigma,L\rrparenthesis\twoheadrightarrow_{\mathsf{c}}\\#^{-1}(n+1)$.
Then

$\begin{array}[]{lcl}\llparenthesis\sigma,\mathbf{ifz}(L,N_{1},N_{2})\rrparenthesis&=&\llbracket\mathbf{ifz}(L,N_{1},N_{2})\rrbracket^{x_{1},\dots,x_{n}}\,@\,[\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
&=&\mathsf{Ifz}_{n}\,@\,[\\#\llbracket
L\rrbracket^{x_{1},\dots,x_{n}},\\#\llbracket
N_{1}\rrbracket^{x_{1},\dots,x_{n}},\\#\llbracket
N_{2}\rrbracket^{x_{1},\dots,x_{n}},\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
&\twoheadrightarrow_{\mathsf{c}}&\left\langle\begin{aligned}
R_{0}=\\#\llparenthesis\sigma,L\rrparenthesis,R_{1}=\\#\llparenthesis\sigma,N_{1}\rrparenthesis,R_{2}=\\#\llparenthesis\sigma,N_{2}\rrparenthesis,\pol
R,0\shortleftarrow\mathtt{Test}(0,\,1,\,2);\mathtt{Call}~{}0,[]\end{aligned}\right\rangle,\\\
&&\textrm{by
Lemma~{}\ref{lem:existenceofeams}(\ref{lem:existenceofeams5}),}\\\
&\twoheadrightarrow_{\mathsf{c}}&\left\langle\begin{aligned}
R_{0}={n+1},R_{1}=\\#\llparenthesis\sigma,N_{1}\rrparenthesis,R_{2}=\\#\llparenthesis\sigma,N_{2}\rrparenthesis,\pol
R,0\shortleftarrow\mathtt{Test}(0,\,1,\,2);\mathtt{Call}~{}0,[]\end{aligned}\right\rangle\\\
&\twoheadrightarrow_{\mathsf{c}}&\llparenthesis\sigma,N_{2}\rrparenthesis\end{array}$

We conclude since, by IH,
$\llparenthesis\sigma,N_{2}\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket
V\rrbracket$.

Case 9: $(\mathrm{ifz_{0}})$

$M=\mathbf{ifz}(L,N_{1},N_{2})$, $\sigma\triangleright
L\Downarrow_{d}\underline{0}$, $\sigma\triangleright N_{1}\Downarrow_{d}V$. By
IH we get
$\llparenthesis\sigma,L\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket\underline{0}\rrbracket$,
and since the $(n+1)$-th numeral machine is in final state, we derive
$\llparenthesis\sigma,L\rrparenthesis\twoheadrightarrow_{\mathsf{c}}\\#^{-1}(0)$.
Then

$\begin{array}[]{rl}\llparenthesis\sigma,\mathbf{ifz}(L,N_{1},N_{2})\rrparenthesis=&\llbracket\mathbf{ifz}(L,N_{1},N_{2})\rrbracket^{x_{1},\dots,x_{n}}\,@\,[\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
=&\mathsf{Ifz}_{n}\,@\,[\\#\llbracket
L\rrbracket^{x_{1},\dots,x_{n}},\\#\llbracket
N_{1}\rrbracket^{x_{1},\dots,x_{n}},\\#\llbracket
N_{2}\rrbracket^{x_{1},\dots,x_{n}},\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
\twoheadrightarrow_{\mathsf{c}}&\left\langle\begin{aligned}
R_{0}=\\#\llparenthesis\sigma,L\rrparenthesis,R_{1}=\\#\llparenthesis\sigma,N_{1}\rrparenthesis,R_{2}=\\#\llparenthesis\sigma,N_{2}\rrparenthesis,\pol
R,0\shortleftarrow\mathtt{Test}(0,\,1,\,2);\mathtt{Call}~{}0,[]\end{aligned}\right\rangle,\\\
&\textrm{by Lemma~{}\ref{lem:existenceofeams}(\ref{lem:existenceofeams5}),}\\\
\twoheadrightarrow_{\mathsf{c}}&\left\langle\begin{aligned}
R_{0}={0},R_{1}=\\#\llparenthesis\sigma,N_{1}\rrparenthesis,R_{2}=\\#\llparenthesis\sigma,N_{2}\rrparenthesis,\pol
R,0\shortleftarrow\mathtt{Test}(0,\,1,\,2);\mathtt{Call}~{}0,[]\end{aligned}\right\rangle\\\
\twoheadrightarrow_{\mathsf{c}}&\llparenthesis\sigma,N_{1}\rrparenthesis\end{array}$

We conclude since, by IH,
$\llparenthesis\sigma,N_{1}\rrparenthesis\leftrightarrow_{\mathsf{c}}\llbracket
V\rrbracket$.

Case $(\mathrm{fix})$:

Then $M=\mathbf{fix}\,M^{\prime}$ and $\sigma\triangleright
M^{\prime}\cdot(\mathbf{fix}\,M^{\prime})$. Then

$\begin{array}[]{lcll}\llparenthesis\sigma,\mathbf{fix}\,M^{\prime}\rrparenthesis&=&\llbracket\mathbf{fix}\,M^{\prime}\rrbracket^{x_{1},\dots,x_{n}}\,@\,[\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
&=&\mathsf{Y}_{n}\,@\,[\\#\llbracket
M^{\prime}\rrbracket^{x_{1},\dots,x_{n}},\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
&\twoheadrightarrow_{\mathsf{c}}&\llbracket M^{\prime}\rrbracket^{\pol
x}\,@\,[\\#\llparenthesis\sigma(\pol
x)\rrparenthesis,\\#(\mathsf{Y}_{n}\,@\,[\\#\llbracket
M^{\prime}\rrbracket^{\pol x},\\#\llparenthesis\sigma(\pol
x)\rrparenthesis]\,)]\\\ &=&\llbracket M^{\prime}\rrbracket^{\pol
x}\,@\,[\\#\llparenthesis\sigma(\pol
x)\rrparenthesis,\\#(\llbracket\mathbf{fix}\,M^{\prime}\rrbracket^{\pol
x}\,@\,[\\#\llparenthesis\sigma(\pol x)\rrparenthesis]\,)]\,,&\textrm{by
Lemma~{}\ref{lem:existenceofeams}\eqref{lem:existenceofeams2}},\\\
&{}_{\mathsf{c}}\\!\\!\twoheadleftarrow&\mathsf{Apply}_{n}\,@\,[\\#\llbracket
M^{\prime}\rrbracket^{\pol
x},\\#\llbracket\mathbf{fix}\,M^{\prime}\rrbracket^{\pol
x},\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
&=&\llbracket
M^{\prime}\cdot(\mathbf{fix}\,M^{\prime})\rrbracket^{x_{1},\dots,x_{n}}\,@\,[\\#\llparenthesis\sigma(x_{1})\rrparenthesis,\dots,\\#\llparenthesis\sigma(x_{n})\rrparenthesis]\\\
&=&\llparenthesis\sigma,M^{\prime}\cdot(\mathbf{fix}\,M^{\prime}\rrparenthesis.\end{array}$

This concludes the proof.

######  Proof A.4 (Proof of Theorem 4.20(1)).

For an EPCF term $M$, an EPCF value $V$ and an explicit substitution $\sigma$,
we show $\sigma\triangleright
M\Downarrow_{d}V\Rightarrow(\sigma,M)^{*}\Downarrow([\,],V)^{*}$ by induction
on a derivation of $\sigma\triangleright M\Downarrow_{d}V$.

Case $(\mathrm{nat})$:

In this case $M=V=\underline{n}$ for some $n\geq 0$. By definition,
$(\sigma,\underline{n})^{*}=\underline{n}$, so we apply PCF’s rule
$(\mathrm{val})$ and get $\underline{n}\Downarrow\underline{n}$.

Case $(\mathrm{fun})$:

We have $M=\lambda x.M^{\prime}\langle\sigma^{\prime}\rangle$ and $V=\lambda
x.M^{\prime}\langle\sigma+\sigma^{\prime}\rangle$.
As $(\sigma,\lambda
x.M^{\prime}\langle\sigma^{\prime}\rangle)^{*}=([\,],\lambda
x.M^{\prime}\langle\sigma+\sigma^{\prime}\rangle)^{*}=\lambda
x.(\sigma+\sigma^{\prime},M^{\prime})^{*}$ and the latter is a PCF value, we
can apply PCF’s rule $(\mathrm{val})$ to conclude $(\sigma,\lambda
x.M^{\prime}\langle\sigma^{\prime}\rangle)^{*}\Downarrow([\,],\lambda
x.M^{\prime}\langle\sigma+\sigma^{\prime}\rangle)^{*}.$

Case $(\mathrm{var})$:

In this case $M=x$, $\sigma(x)=(\rho,N)$ and $\rho\triangleright
N\Downarrow_{d}V$. By IH $(\rho,N)^{*}\Downarrow([],V)^{*}$. We conclude since
$(\sigma,M)^{*}=(\rho,N)^{*}$.

Case $(\beta_{v})$:

In this case $M=M_{1}\cdot M_{2}$ with $\sigma\triangleright
M_{1}\Downarrow_{d}\lambda x.M_{1}^{\prime}\langle\rho\rangle$, wlog
$x\notin\mathrm{dom}(\rho+\sigma)$, and
$\rho+[x\leftarrow(\sigma,M_{2})]\triangleright
M_{1}^{\prime}\Downarrow_{d}V$. By IH we obtain
$(\sigma,M_{1})^{*}\Downarrow([\,],\lambda
x.M_{1}^{\prime}\langle\rho\rangle)^{*}$ and
$(\rho+[x\leftarrow(\sigma,M_{2})],M_{1}^{\prime})^{*}\Downarrow([\,],V)^{*}$.
By Lemma 4.18(1)
$(\rho+[x\leftarrow(\sigma,M_{2})],M_{1}^{\prime})^{*}=(\rho,M_{1}^{\prime})^{*}[(\sigma,M_{2})^{*}/x]$.
By definition, $([\,],\lambda x.M_{1}^{\prime}\langle\rho\rangle)^{*}=\lambda
x.(\rho,M_{1}^{\prime})^{*}$ and
$(\sigma,M_{1})^{*}\cdot(\sigma,M_{2})^{*}=(\sigma,M_{1}\cdot M_{2})^{*}$.
Thus

$(\sigma,M_{1}\cdot
M_{2})^{*}\Downarrow([\,],V)^{*}\lx@proof@logical@and(\sigma,M_{1})^{*}\Downarrow\lambda
x.(\sigma^{\prime},M_{1}^{\prime})^{*}(\sigma^{\prime},M_{1}^{\prime})^{*}[(\sigma,M_{2})^{*}/x]\Downarrow([\,],V)^{*}$

Case $(\mathrm{fix})$:

In this case $M=\mathbf{fix}\,{N}$ and $\sigma\triangleright
N\cdot(\mathbf{fix}\,N)\Downarrow_{d}V$. From the IH we get
$(\sigma,N\cdot(\mathbf{fix}\,N))^{*}\Downarrow([\,],V)^{*}$. By definition,
we have
$(\sigma,N\cdot(\mathbf{fix}\,N))^{*}=(\sigma,N)^{*}\cdot(\mathbf{fix}\,(\sigma,N)^{*})$
and $\mathbf{fix}\,(\sigma,N)^{*}=(\sigma,\mathbf{fix}\,N)^{*}$. By applying
PCF’s rule $(\mathrm{fix})$, we obtain

$(\sigma,\mathbf{fix}\,N)^{*}\Downarrow([\,],V)^{*}(\sigma,N\cdot(\mathbf{fix}\,N))^{*}\Downarrow([\,],V)^{*}$

All other cases derive straightforwardly from the IH.

######  Proof A.5 (Proof of Theorem 4.20(2)).

For a PCF program $P$ and PCF value $U$, we show that $P\Downarrow U$ entails:

$\forall(\sigma,M)\in P^{\dagger},\,\exists V\in\mathrm{Val}\,.\,(\
\sigma\triangleright M\Downarrow_{d}V\textrm{ and }([\,],V)\in U^{\dagger}\ )$

By induction on the lexicographically ordered pairs, whose first component is
the length of a derivation of $P\Downarrow U$ and second component is
$|{(\sigma,M)}|$.

First, consider the case $M=y$ and $\sigma(y)=(\rho,N)$, with $(\rho,N)\in
P^{\dagger}$. In this case, the length of the derivation
$(\rho,N)^{*}\Downarrow U$ remained unchanged, while
$|{(\rho,N)}|<|{(\sigma,M)}|$. Thus, we may use the IH and conclude by
applying $(\mathrm{var})$. Therefore, in the following we assume that $M$ is
not a variable.

Case $(\mathrm{val})$:

In this case $P=U$. Given $(\sigma,M)\in P^{\dagger}$, we distinguish several
cases:

  * •

Case $P=U=\lambda x.P_{0}$. Then, $M=\lambda x.M_{0}\langle\rho\rangle$ with
$P_{0}=(\sigma+\rho,M_{0})^{*}$. Setting $V=\lambda
x.M_{0}\langle\sigma+\rho\rangle$ we obtain $M\Downarrow_{d}V$ by
$(\mathrm{fun})$ with $([],V)^{*}=\lambda x.(\sigma+\rho,M_{0})=\lambda
x.P_{0}=U.$

  * •

$P=U=\mathbf{0}$. It follows $M=V=\mathbf{0}$ and
$\sigma\triangleright\mathbf{0}\Downarrow_{d}\mathbf{0}$ by $(\mathrm{nat})$.

  * •

$P=U=\mathbf{succ}\,(\underline{n})$, for some $n\in{\rm Nature}$, and $M$ is
not a variable.

There are two possibilities:

    * –

$M=\mathbf{succ}\,(\underline{n})$ in which case we are done, since
$\sigma\triangleright\underline{n+1}\Downarrow_{d}\underline{n+1}$.

    * –

$M=\mathbf{succ}\,(\underline{y})$ with $\sigma(y)=(\rho,N)$ and
$(\rho,N)\in\underline{n}^{\dagger}$. Again, the length of the derivation
$(\rho,N)^{*}\Downarrow\underline{n}$ is unchanged, while
$|{(\rho,N)}|<|{(\sigma,M)}|$. Once applied the IH, we conclude by
$(\mathrm{var})+(\mathrm{sc})$.

Case $(\beta_{v})$:

$P=P_{1}\cdot P_{2}$ with $P_{1}\Downarrow\lambda x.Q_{1}$ and
$Q_{1}[P_{2}/x]\Downarrow U$ for some $Q_{1}$. Notice that, since $P$ is
closed so are $P_{1},P_{2}$ and hence $\mathrm{FV}(Q_{1})\subseteq\\{x\\}$.
Now, $(\sigma,M)^{*}=P$ entails $M=M_{1}\cdot M_{2}$ with $(\sigma,M_{1})\in
P_{1}^{\dagger}$ and $(\sigma,M_{2})\in P_{2}^{\dagger}$. By ind. hyp., there
is $V^{\prime}\in\mathrm{Val}$ such that $\sigma\triangleright
M_{1}\Downarrow_{d}V_{1}$ with $([],V_{1})\in(\lambda x.Q_{1})^{\dagger}$.
This implies $V_{1}=\lambda x.N_{1}\langle\rho\rangle$ for some
$(\rho,N_{1})\in Q_{1}^{\dagger}$. By Lemma 4.18(2), we get
$(\rho+[x\leftarrow(\sigma,M_{2})],N_{1})\in(Q_{1}[P_{2}/x])^{\dagger}$. By
ind. hyp., there is $V\in\mathrm{Val}$ such that
$\rho+[x\leftarrow(\sigma,M_{2})]\triangleright N_{1}\Downarrow_{d}V$ and
$V\in U^{\dagger}$. Conclude by EPCF’s $(\beta_{v})$.

Case $(\mathrm{fix})$:

$P=\mathbf{fix}\,Q$ and $Q\cdot(\mathbf{fix}\,Q)\Downarrow V$. Then
$(\sigma,M)\in P^{\dagger}$ entails $M=\mathbf{fix}\,N$ with $(\sigma,N)\in
Q^{\dagger}$. It follows that
$(\sigma,N\cdot(\mathbf{fix}\,N))\in(Q\cdot(\mathbf{fix}\,Q))^{\dagger}$,
therefore by IH we get $\sigma\triangleright
N\cdot(\mathbf{fix}\,{N})\Downarrow_{d}V$ for some $V\in U^{\dagger}$. We
conclude by applying EPCF’s rule $(\mathrm{fix})$.

All other cases derive straightforwardly from the IH.