$[\vec{u}\,^{-}\mapsto\vec{a}\,^{-}]$ denote the effect of the substitution
$[\vec{y}\,^{-}\mapsto\vec{t}\,^{-}]$ followed by ${}^{\circ}=[\vec{w}\
\mapsto\vec{r}\,]$ (the order is important here as $\vec{y}\,^{-}$ and
$\vec{w}$ may overlap). Since $\vec{u}\,^{-}\subseteq\vec{y}\cup\vec{w}$ and
$x,\vec{w}\vdash\vec{t}\,^{-}$ and $x\vdash\vec{r}$, this substitution does
indeed cover at least the variables of $\vec{u}\,^{-}$ and we have
$x\vdash\vec{a}\,^{-}$. We may now verify that
$\vec{u}\,^{-}\vdash{q^{\prime}}^{\wr}$ and $x\vdash\vec{a}\,^{-}$ constitute
a pseudo-retraction as follows:

$\displaystyle x^{\prime}$ $\displaystyle\vdash$
$\displaystyle\ll{q^{\prime}}^{\wr}[\vec{u}\,^{-}\mapsto\vec{a}\,^{-}]\gg$
$\displaystyle=$ $\displaystyle\ll
q^{\prime*}[\vec{w}\,^{+}\mapsto\vec{r}\,^{+}][\vec{y}\,^{-}\mapsto\vec{t}\,^{-}][\vec{w}\
\mapsto\vec{r}\,]\gg$ $\displaystyle=$
$\displaystyle\ll(q^{\prime*}[\vec{y}\,^{-}\mapsto\vec{t}\,^{-}])[\vec{w}\
\mapsto\vec{r}\,]\gg$ $\displaystyle=$
$\displaystyle\ll{o^{\prime}}^{\circ}\gg~{}\succeq~{}{x^{\prime}}^{\eta}\;.$

As regards the second equation here, the first substitution
$[\vec{w}\,^{+}\mapsto\vec{r}\,^{+}]$ may be safely omitted as $\vec{w}\,^{+}$
and $\vec{y}\,^{-}$ are disjoint and the terms $\vec{r}\,^{+}$ do not contain
any of the $\vec{w}\,^{+}$ or $\vec{y}\,^{-}$ free. We therefore have
$\overline{k}$ as a pseudo-retract of a product of level $<k$ types. This
contradicts Theorem 12, so the proof of Claim 1 is complete.

We may therefore suppose that in the evaluation
$\ll\\!e^{\dagger}\\!\gg=E[c]$, the originating occurrence of the head $g$ in
$c$ is as indicated by $\Gamma,x^{\prime},\vec{v}\vdash e=C[d^{\prime}]$,
where $\Gamma,x^{\prime},\vec{v},\vec{v}\,^{\prime\prime}\vdash
d^{\prime}={\mathtt{case}}\;gp^{\prime}q^{\prime}\;{\mathtt{of}}\;(\cdots)$.
(Here $\vec{v}\,^{\prime\prime}$ is the local environment for $C[-]$. The
symbols $d^{\prime},p^{\prime},q^{\prime}$ are available for recycling now
that the proof of Claim 1 is complete.)

In order to continue our analysis to greater depth, note that we may write

$\Gamma,x^{\prime},\vec{v}\,^{\prime}\vdash~{}\ll\\!e^{\dagger}\\!\gg~{}=~{}\ll(\lambda\vec{v}.\,C[d^{\prime}])\vec{s}\gg~{}=~{}E[c]\;,$

where $c$ is head-spinal w.r.t. $x^{\prime},\vec{y}\,^{\prime}$, and the head
$g$ of $d^{\prime}$ is the origin of the head $g$ of $c$. (Recall that
$\vec{y}\,^{\prime}$ is the local environment for $E[-]$ and that
$\Gamma,x^{\prime},\vec{v}\vdash e=C[d^{\prime}]$ is regular, whence
${\mathrm{lv}}(\vec{v}\,^{\prime\prime})\leq k$.)

We claim that once again we are in the situation of Lemma 26, taking
$\Gamma,K,d,K^{\prime},c$ of the lemma to be respectively
$(\Gamma,x^{\prime},\vec{v}\,^{\prime})$, $(\lambda\vec{v}.\,C[-])\vec{s}$,
$d^{\prime},E,c$. Condition 2 of the lemma is immediate in the present setup;
for condition 1, we again note that
$\Gamma,x^{\prime},\vec{v}\,^{\prime}\vdash C[d^{\prime}]=e$ and
$\Gamma,\vec{v}\,^{\prime}\vdash\vec{s}$ are regular, so by Proposition 22
contain no bound variables of level $>k$; hence the same is true for
$(\lambda\vec{v}.\,C[d^{\prime}])\vec{s}$. Applying Lemma 26, we obtain a
substitution ${}^{{\dagger}^{\prime}}=[\vec{v}\,^{+}\mapsto\vec{s}\,^{+}]$ of
level $\leq k$ (with $\vec{v}\,^{+}=\vec{v},\vec{v}\,^{\prime\prime}$), where
$\Gamma,x^{\prime},\vec{v}\,^{\prime},\vec{v}\,^{+}\vdash d^{\prime}$ and
$\Gamma,x^{\prime},\vec{v}\,^{\prime},\vec{y}\,^{\prime}\vdash\vec{s}\,^{+}$
are regular, such that

$\Gamma,x^{\prime},\vec{v}\,^{\prime},\vec{y}\,^{\prime}\;\vdash\;\ll
d^{\prime}[\vec{v}\,^{+}\\!\mapsto\\!\vec{s}\,^{+}]\gg$

is head-spinal w.r.t. $x^{\prime},\vec{y}\,^{\prime}$, and indeed of the form
${\mathtt{case}}\;gF^{\prime}o^{\prime}\;{\mathtt{of}}\;(\cdots)$ with
$F^{\prime},o^{\prime}$ as above. (We may in fact write just
$\Gamma,x^{\prime},\vec{v}\,^{+}\vdash d^{\prime}$ since, by assumption, the
variables of $\vec{v}\,^{\prime}$ do not overlap with the free or bound
variables of $d$ so do not appear in $d$.) We may also read off that
$\ll(p^{\prime})^{{\dagger}^{\prime}}\gg\,=F^{\prime}$ and
$\ll(q^{\prime})^{{\dagger}^{\prime}}\gg\,=o^{\prime}$. As regards the
substitution ${}^{{\dagger}^{\prime}}=[\vec{v}\,^{+}\mapsto\vec{s}\,^{+}]$, it
is clear that this extends $[\vec{v}\mapsto\vec{s}\,]$ since the evaluation of
$(\lambda\vec{v}.\,C[d^{\prime}])\vec{s}$ starts by $\beta$-reducing this
term. Moreover, the argument of Lemma 26(iii) shows that
${}^{{\dagger}^{\prime}}$ is trivial for any level $k$ variables in
$\vec{v}\,^{\prime\prime}$, as $C[-]$ is in normal form.

We are now back precisely where we started, in the sense that
$d^{\prime},\vec{v}\,^{+},\vec{s}\,^{+}$ themselves satisfy the hypotheses of
Lemma 27, with $(\Gamma,x^{\prime})$ now playing the role of $\Gamma$ and
$(\vec{v}\,^{\prime},\vec{y}\,^{\prime})$ that of $\vec{v}\,^{\prime}$.
Explicitly, we have regular terms

$\Gamma,x,\vec{v}\,^{+}\vdash
d^{\prime}={\mathtt{case}}\;gp^{\prime}q^{\prime}\;{\mathtt{of}}\;(\cdots)\;,~{}~{}~{}~{}~{}~{}~{}~{}\Gamma,x,\vec{v}\,^{\prime},\vec{y}\,^{\prime}\vdash\vec{s}\,^{+}$

(so that
${\mathrm{lv}}(\vec{v}\,^{+}),{\mathrm{lv}}(\vec{v}\,^{\prime},\vec{y}\,^{\prime})\leq
k$) where $\Gamma,x,\vec{v}\,^{\prime},\vec{y}\,^{\prime}\vdash\ll
d^{\prime}[\vec{v}\,^{+}\mapsto\vec{s}\,^{+}]\gg$ is head-spinal w.r.t.
$x^{\prime},\vec{y}\,^{\prime}$. We can therefore iterate the whole of the
above argument to obtain an infinite descending chain of subterms

$\begin{array}[]{rrlrl}\Gamma,\vec{v}\vdash&d=&{\mathtt{case}}\;gpq\;{\mathtt{of}}\;(\cdots)\;,&p=&\lambda
x^{\prime}.\,C[d^{\prime}]\;,\\\
\Gamma,\vec{v},x^{\prime},\vec{v}\,^{\prime\prime}\vdash&d^{\prime}=&{\mathtt{case}}\;gp^{\prime}q^{\prime}\;{\mathtt{of}}\;(\cdots)\;,&p^{\prime}=&\lambda
x^{\prime\prime}.\,C^{\prime}[d^{\prime\prime}]\;,\\\
\Gamma,\vec{v},x^{\prime},\vec{v}\,^{\prime\prime},x^{\prime\prime},\vec{v}\,^{\prime\prime\prime\prime}\vdash&d^{\prime\prime}=&{\mathtt{case}}\;gp^{\prime\prime}q^{\prime\prime}\;{\mathtt{of}}\;(\cdots)\;,&p^{\prime\prime}=&\lambda
x^{\prime\prime\prime}.\,C^{\prime\prime}[d^{\prime\prime\prime}]\;,\\\
&\cdots&&\cdots&\end{array}$

along with associated substitutions †, ${}^{{\dagger}^{\prime}}$,
${}^{{\dagger}^{\prime\prime}},\ldots$ applicable to
$d,d^{\prime},d^{\prime\prime},\ldots$ respectively, such that
$\ll\\!p^{\dagger}\\!\gg$, $\ll(p^{\prime})^{{\dagger}^{\prime}}\\!\gg$,
$\ll(p^{\prime\prime})^{{\dagger}^{\prime\prime}}\\!\gg,\ldots$ coincide with
the successive procedure subterms $F,F^{\prime},F^{\prime\prime},\ldots$ from
the spine of the original term $\ll\\!d^{\dagger}\\!\gg$, and likewise
$\ll\\!q^{\dagger}\\!\gg$, $\ll(q^{\prime})^{{\dagger}^{\prime}}\\!\gg$,
$\ll(q^{\prime\prime})^{{\dagger}^{\prime\prime}}\\!\gg,\ldots$ coincide with
$o,o^{\prime},o^{\prime\prime}\ldots$.

We cannot quite conclude that $d$ is head-spinal, because the critical $x$ in
$q^{\dagger}$ might originate not from $q$ but from a level $k$ term in
$\vec{s}$ (for example). However, we can show that this problem does not arise
for $q^{\prime},q^{\prime\prime},\ldots$, essentially because
$x^{\prime},x^{\prime\prime},\ldots$ are bound locally within $p$. We will in
fact show that $d^{\prime}$ is head-spinal w.r.t.
$x^{\prime},\vec{v}\,^{\prime\prime}$, where $\vec{v}\,^{\prime\prime}$ is the
local environment for $C[-]$; this will imply that $d$ is spinal. In the light
of Definition 24, it will be sufficient to show that
$(q^{\prime})^{\circ^{\prime}}\succeq{x^{\prime}}^{\eta}$ for some
$x^{\prime},\vec{v}\,^{\prime\prime}$-closed specialization
${}^{\circ^{\prime}}$ covering the free variables of $q^{\prime}$ except
$x^{\prime}$ (namely those of $\Gamma,\vec{v},\vec{v}\,^{\prime\prime}$); the
same argument will then obviously apply also to
$q^{\prime\prime},q^{\prime\prime\prime},\ldots$.

Recall that $\Gamma,\vec{v},\vec{v}\,^{\prime\prime},x^{\prime}\vdash
q^{\prime}$ and $\Gamma,\vec{v}\,^{\prime},\vec{y}\,^{\prime},x^{\prime}\vdash
o^{\prime}$. Since $gF^{\prime}o^{\prime}$ is head-spinal w.r.t.
$x,\vec{y}\,^{\prime}$, we may as before take
${}^{\circ}=[\vec{w}\mapsto\vec{r}\,]$ $x^{\prime},\vec{y}\,^{\prime}$-closed
such that ${o^{\prime}}^{\circ}\succeq{x^{\prime}}^{\eta}$, where
$\vec{w}=\Gamma,\vec{v}\,^{\prime},\vec{y}\,^{\prime}$ and
$x^{\prime}\vdash\vec{r}$. Now define

${}^{\circ^{\prime}}~{}=~{}[\vec{v}\mapsto\vec{s}\,^{\circ},\;\vec{v}\,^{\prime\prime}\mapsto(\vec{s}\,^{\prime\prime})^{\circ},\;\vec{w}\,^{\Gamma}\mapsto\vec{r}\,^{\Gamma}]$

(where we write $\vec{s}\,^{+}$ as $\vec{s},\vec{s}\,^{\prime\prime}$, and
$\vec{w}\,^{\Gamma}\mapsto\vec{r}\,^{\Gamma}$ denotes the restriction of ∘ to
$\Gamma$). This covers the free variables of $q^{\prime}$ except $x^{\prime}$,
and we have
$x^{\prime}\vdash\vec{s}\,^{\circ},(\vec{s}\,^{\prime\prime})^{\circ},\vec{r}\,^{\Gamma}$
because $\vec{w}\vdash\vec{s},\vec{s}\,^{\prime\prime}$ and $x\vdash\vec{r}$.
Moreover, we have

$q^{\prime\circ^{\prime}}~{}=~{}(q^{\prime}[\vec{v}\,^{+}\mapsto(\vec{s}\,^{+})^{\circ}])[\vec{w}\,^{\Gamma}\mapsto\vec{r}\,^{\Gamma}]~{}=~{}(q^{\prime{\dagger}^{\prime}})^{\circ}~{}\approx~{}o^{\circ}~{}\succeq~{}x^{\prime\eta}$

since $(\vec{s}\,^{+})^{\circ}$ contains no free variables except $x$. To
check that ${}^{\circ^{\prime}}$ is
$x^{\prime},\vec{v}\,^{\prime\prime}$-closed, it remains to show that that
$u^{\circ^{\prime}}$ may contain $x^{\prime}$ free only when
$u\in\vec{v},^{\prime\prime}$ and $u$ is of level $<k$. (Indeed, it is because
of the possibility of $x^{\prime}$ occurring free in these terms that the
machinery of $x,V$-closed substitutions is necessary at all.) The remaining
cases are handled as follows:

  * •

The terms $\vec{s}$ exist in environment $\Gamma,\vec{v}\,^{\prime}$, so do
not involve $x^{\prime}$ or any of the variables of $\vec{y}\,^{\prime}$.
Since ∘ is $x^{\prime},\vec{y}\,^{\prime}$-closed, it follows that the terms
$\vec{s}\,^{\circ}$ do not involve $x^{\prime}$.

  * •

For any variables $v\in\vec{v}\,^{\prime\prime}$ of level $k$, we have
$v^{{\dagger}^{\prime}}=v^{\eta}$ which contains no free variables of level
$<k$, so that $(v^{{\dagger}^{\prime}})^{\circ}$ cannot involve $x^{\prime}$.

  * •

The $\vec{r}\,^{\Gamma}$ cannot involve $x^{\prime}$, since ∘ is
$x^{\prime},\vec{y}\,^{\prime}$-closed and $\Gamma$ is disjoint from
$\vec{y}\,^{\prime}$.

This completes the verification that $d$ is spinal. $\Box$

From the above lemma we may immediately conclude, for example, that in the
setting of Lemma 26(ii) the term $d$ is spinal.

We are now ready for the main result of this section:

###### Theorem 28

Every ${\mathrm{PCF}}^{\Omega}_{k}$-denotable procedure $\Gamma\vdash p$ is
non-$g$-spinal where $g:(k+1)\rightarrow(k+1)$.

Proof In the light of Section 3, it will suffice to show that the clauses of
Theorem 20 cannot generate spinal terms from non-spinal ones. For clauses 1–5
this is very easily seen. For clause 6, it will be sufficient to show that
non-spinal terms are closed under $k$-plugging, and it is here that the
machinery of Lemmas 26 and 27 comes into play.

Suppose that $t=\,\ll\Pi_{\Gamma,Z}(e,\xi)\gg$ where $\Gamma,Z\vdash e$ and
$\Gamma,Z\vdash\xi(z)$ for each $z\in Z$. For later convenience, to each
$z_{i}\in Z$ let us associate the procedure $\Gamma\vdash
r_{i}=\,\ll\Pi_{\Gamma,Z}(\xi(z_{i}),\xi)\gg$; it is then clear from the
definition of plugging and the evaluation theorem that $t=\,\ll
e[\vec{z}\mapsto\vec{r}\,]\gg$ and that
$r_{i}=\,\ll\xi(z_{i})[\vec{z}\mapsto\vec{r}\,]\gg$ for each $i$.

It will be natural to frame the argument contrapositively. Suppose that $t$ is
spinal, i.e. $t$ contains some head-spinal expression $c$ at position $K[-]$.
We shall focus on the head occurrence of $g$ in $c$. Clearly this occurrence
must originate from one of the ingredients $\Gamma,Z\vdash e$ or
$\Gamma,Z\vdash\xi(z)$ of the plugging $\Pi_{\Gamma,Z}(e,\xi)$; let us denote
this ingredient by $\Gamma,Z\vdash t_{0}$. We will show that $t_{0}$ itself is
spinal.

Suppose that the relevant occurrence of $g$ in $t_{0}$ is as indicated by

$\Gamma,Z\;\vdash\;t_{0}~{}=~{}L[d]\;,~{}~{}~{}~{}~{}~{}\Gamma,Z,\vec{v}\;\vdash\;d~{}=~{}{\mathtt{case}}\;gpq\;{\mathtt{of}}\;(\cdots)\;,$

where $\vec{v}$ is the local environment for $L[-]$. Writing ⋆ for
$[\vec{z}\mapsto\vec{r}\,]$, we have $\ll\Pi(t_{0},\xi)\gg\,=\,\ll
t_{0}^{\star}\gg$; and if $C[-]$ is the context encapsulating the remainder of
the plugging $\Pi(e,\xi)$, then we may write

$\Gamma\vdash~{}K[c]~{}=~{}t~{}=~{}\ll C[\Pi(t_{0},\xi)]\gg~{}=~{}\ll
C[t_{0}^{\star}]\gg~{}=~{}\ll C[L^{\star}[\ll\\!d^{\star}\\!\gg]]\gg\;,$

where

$\ll\\!d^{\star}\\!\gg~{}=~{}{\mathtt{case}}\;g\ll\\!p^{\star}\\!\gg\ll\\!q^{\star}\\!\gg\\!\;{\mathtt{of}}\;(\cdots)\;.$

We claim that we are in the situation of Lemma 26, taking
$\Gamma,K,d,K^{\prime},c$ of the lemma to be respectively
$\Gamma,C[L^{\star}[-]],\ll\\!\\!d^{\star}\\!\\!\gg,K,c$. Condition 1 of the
lemma holds because $C[t_{0}^{\star}]$ is constructed by substitution from
normal-form terms of level $\leq k$, and condition 2 is immediate in the
present setup.

By Lemma 26, we may therefore conclude that for a suitable substitution
$[\vec{v}\mapsto\vec{s}\,]$ with $\Gamma,\vec{v}\,^{\prime}\vdash\vec{s}$
regular, $\Gamma\vdash\,\ll\ll\\!d^{\star}\\!\gg[\vec{v}\mapsto\vec{s}\,]\gg$
is head-spinal. (Note that the local variables of $C[-]$ do not appear in
$d^{\star}$, because $\Gamma,Z\vdash t_{0}$ and $\Gamma\vdash\vec{r}$.)
Equivalently, we may say that $\ll d[\vec{v}\,^{+}\\!\mapsto\vec{s}\,^{+}]\gg$
is head-spinal, where

$[\vec{v}\,^{+}\mapsto\vec{s}\,^{+}]~{}=~{}[\vec{z}\mapsto\vec{r},~{}\vec{v}\mapsto\vec{s}\,]\;,$

so that $\Gamma,\vec{v}\,^{\prime}\vdash\vec{s}\,^{+}$ and
${\mathrm{lv}}(\vec{v}\,^{+}),{\mathrm{lv}}(\vec{v}\,^{\prime})\leq k$. (Note
that the $\vec{z}$ do not appear free in $\vec{s}$, nor the $\vec{v}$ in
$\vec{r}$.)

Since $\Gamma,Z,V\vdash d$ and $\Gamma,\vec{v}\,^{\prime}\vdash\vec{s}\,^{+}$
are regular, we are in the situation of Lemma 27, so may conclude that $d$
itself is spinal, and hence that $t_{0}$ is spinal. We have thus shown that
$k$-plugging cannot assemble spinal terms from non-spinal ones, and this
completes the proof. $\Box$

In particular, since the procedure $g\vdash F_{k+1}[g]$ mentioned at the start
of the section is spinal, we may conclude that this procedure is not
${\mathrm{PCF}}^{\Omega}_{k}$-denotable, and hence neither is the procedure
$Y_{k+1}$. This establishes Theorem 11.

We conclude the section by mentioning some minor variations on Theorem 28 that
we will require below. First, as already indicated, the whole of the above
proof goes through for the modified notion of spinal term appropriate to a
variable $g:0\rightarrow(k+1)\rightarrow(k+1)$. Secondly, the theorem also
holds for an innocuous extension of ${\mathrm{PCF}}^{\Omega}_{k}$ with a
constant
${\mathit{byval}}:({\mathtt{N}}\rightarrow{\mathtt{N}})\rightarrow{\mathtt{N}}\rightarrow{\mathtt{N}}$,
whose denotation in ${\mathsf{SP}}^{0}$ we take to be

$\lambda
fx.\;{\mathtt{case}}\;x\;{\mathtt{of}}\;(i\Rightarrow{\mathtt{case}}\;fi\;{\mathtt{of}}\;(j\Rightarrow
j))\;.$

To see that the proof of Theorem 28 goes through in the presence of
${\mathit{byval}}$, it suffices simply to add an extra clause to the inductive
proof noting that the procedure for ${\mathit{byval}}$ is non-spinal. This
mild extension will allow a significant simplification of the forms of
procedures that we need to consider in Section 5.888The operator
${\mathit{byval}}$ plays a major role in [17, Section 7.1], where it is shown
that every element of ${\mathsf{SP}}^{0}$ is denotable in
${\mathrm{PCF}}^{\Omega}+{\mathit{byval}}$. The sense in which it is innocuous
is that its denotation in ${\mathsf{SF}}$ coincides with that of $\lambda
fx.\,{\mathit{ifzero}}\,x\,(fx)(fx)$; thus ${\mathit{byval}}$ adds nothing to
the expressivity of ${\mathrm{PCF}}^{\Omega}_{k}$ as regards ${\mathsf{SF}}$.

##  5 Non-definability in the extensional model

To obtain corresponding non-definability results for ${\mathsf{SF}}$ rather
than ${\mathsf{SP}}^{0}$, one must show not only that the canonical procedures
$Y_{\tau}$ considered above are not ${\mathrm{PCF}}^{\Omega}_{k}$-denotable,
but also that no extensionally equivalent procedures are. It is easy to see
that there are indeed many other procedures $Z$ with the same extension as
$Y_{\tau}$. To give a trivial example, we may present the canonical procedure
$Y_{k+1}$ as $\lambda gx.C[g,x]$, where

$C[g,x]~{}=~{}{\mathtt{case}}\;A[g,x]\;{\mathtt{of}}\;(i\Rightarrow
i)\;,~{}~{}~{}~{}~{}~{}~{}~{}A[g,x]~{}=~{}g(\lambda
x^{\prime}.C[g,x^{\prime}])x^{\eta}\;.$

However, another candidate for the fixed point operator is

$Z_{0}~{}=~{}\lambda
gx.\,{\mathtt{case}}\;A[g,x]\;{\mathtt{of}}\;(i\Rightarrow{C[g,x]})\;.$

Intuitively, this computes the desired value twice, discarding the first
result.

As a slightly more subtle example, consider the procedure

$Z_{1}~{}=~{}\lambda gx.\,{\mathtt{case}}\;g(\lambda
x^{\prime}.{\mathtt{case}}\;A[g,x]\;{\mathtt{of}}\;(i\Rightarrow{C[g,x^{\prime}]}))x^{\eta}\;{\mathtt{of}}\;(k\Rightarrow
k)\;.$

Here, within the $\lambda x^{\prime}$ subterm, we have smuggled in a
repetition of the top-level computation $A[g,x]$ before proceeding to evaluate
what is really required. The effect is that $\lambda
x^{\prime}.{\mathtt{case}}\;A[g,x]\;{\mathtt{of}}\;(i\Rightarrow
C[g,x^{\prime}])$ may be extensionally below $\lambda
x^{\prime}.C[g,x^{\prime}]$, and this may indeed affect the result when $g$ is
applied. However, this can only happen when $Y_{k+1}gx$ is undefined anyway,
so it is easy to see that $Z_{1}$ as a whole will have the same extension as
$Y_{k+1}$.

Yet another way to construct procedures extensionally equivalent to $Y_{k+1}$
is to vary the subterms of the form $x^{\eta}$ (where $x$ has type $k$). For
instance, in the case $k=1$, we could replace $x^{\eta}$ by an extensionally
equivalent term such as

$X_{0}~{}=~{}\lambda
y^{0}.\,x(\lambda.\,{\mathtt{case}}\;y\;{\mathtt{of}}\;(0\Rightarrow{\mathtt{case}}\;x(\lambda.0)\;{\mathtt{of}}\;(j\Rightarrow
0)\mid i+1\Rightarrow i+1))\;.$

This is different in character from the previous examples: rather than simply
repeating the computation of $xy^{\eta}$, we are performing the specific
computation $x(\lambda.0)$ which we can see to be harmless given that this
point in the tree has been reached. Clearly, such ‘time-wasting’ tricks as the
above may be combined and elaborated to yield more complex examples of
procedures equivalent to $Y$.

However, all of the above are rather innocuous variations and do not really
yield a fundamentally different method of computing fixed points. For example,
the bodies of both $Z_{0},Z_{1}$ are still head-spinal terms, and it is
essentially the spines that are really computing the desired fixed point by
the canonical method. This suggests that we should try to show that every
procedure extensionally equivalent to $Y_{k+1}$ is spinal; from this it would
follow easily by Theorem 28 that the fixed point functional $Y_{k+1}$ in
${\mathsf{SF}}$ is not denotable in ${\mathrm{PCF}}^{\Omega}_{k}$.

Unfortunately, we are currently unable to show this in the case of $Y_{k+1}$:
indeed, the syntactic analysis of procedures $Z\approx Y_{k+1}$ appears to
present considerable technical difficulties. We shall establish the result for
$Y_{0\rightarrow(k+1)}$, although even here, it is simplest to concentrate not
on $Y_{0\rightarrow(k+1)}$ itself, but on a certain functional that is readily
definable from it, namely the functional $\Phi_{k+1}$ introduced in Section 1.
Nonetheless, the above examples of ‘time-wasting’ procedures illustrate some
of the situations that our proof will need to deal with, and they may help to
motivate some of the technical machinery that follows.

Specifically, within ${\mathrm{PCF}}_{k+1}$, let us define

$\displaystyle\Phi_{k+1}$ $\displaystyle:$
$\displaystyle({0}\rightarrow(k+1)\rightarrow(k+1))\rightarrow({0}\rightarrow(k+1))$
$\displaystyle\Phi_{k+1}\,g^{0\rightarrow(k+1)\rightarrow(k+1)}$
$\displaystyle=$ $\displaystyle Y_{{0}\rightarrow(k+1)}\,(\lambda
f^{0\rightarrow(k+1)}.\lambda n.\,g\,n\,(f({\mathit{suc}}\;n)))\;,$

so that informally

$\Phi_{k+1}\,g\,n~{}=~{}g\,n\,(g\,(n+1)\,(g\,(n+2)\,(\cdots)))\;.$

For the rest of this section we will write $\Phi_{k+1}$ simply as $\Phi$. For
each $n\in\mathbb{N}$, let $g\vdash\Phi^{n}[g]=\Phi\,g\,\widehat{n}:{k+1}$,
and let $p_{n}\in{\mathsf{SP}}(k+1)$ be the canonical NSP for $\Phi^{n}[g]$
(that is, the one arising from the above ${\mathrm{PCF}}$ definition via the
standard interpretation in ${\mathsf{SP}}^{0}$). These procedures may be
defined simultaneously by:

$g~{}\vdash~{}p_{n}~{}=~{}\lambda
x^{k}.\,{\mathtt{case}}\;g\,(\lambda.n)\,p_{n+1}\,x^{\eta}\;{\mathtt{of}}\;(i\Rightarrow
i)~{}:~{}k+1\;.$

By a syntactic analysis of the possible forms of (simple) procedures $g\vdash
q\approx p_{n}$, we will show that any such $q$ is necessarily spinal. Here we
have in mind the modified notion of spinal term that is applicable to terms
involving a global variable $g:\rho$, where
$\rho={0}\rightarrow(k+1)\rightarrow(k+1)$ (see the explanation following
Definition 24). Using Theorem 28 (adapted to this modified setting), it will
then be easy to conclude that within ${\mathsf{SF}}$, the element
$[\\![\lambda g.\,\Phi^{0}[g]]\\!]$, and hence $Y_{{0}\rightarrow(k+1)}$
itself, is not ${\mathrm{PCF}}^{\Omega}_{k}$-denotable in ${\mathsf{SF}}$.

To show that any $q\approx p_{n}$ is head-spinal, our approach will be as
follows. First, we show that any such $q$ must broadly resemble $p_{n}$ in at
least its top-level structure, in that $q$ must have the form $\lambda
x.\,{\mathtt{case}}\;garo\;{\mathtt{of}}\;(\cdots)$, where the arguments
$a,r,o$ are closely related to the corresponding arguments
$(\lambda.n),p_{n+1},x^{\eta}$ occurring within $p_{n}$. We do this by showing
that if $q$ were to deviate in any way from this prescribed form, we would be
able to cook up procedures $G\in{\mathsf{SP}}^{0}(\rho)$ and
$X\in{\mathsf{SP}}^{0}(k)$ manifesting an extensional difference between $q$
and $p_{n}$, i.e. such that $q[g\mapsto G]X\not\approx p_{n}[g\mapsto G]X$.
(Contrary to our usual convention, we will here use the uppercase letters
$G,X$ to range over normal-form closed procedures that may be substituted for
$g,x$ respectively.) In particular, we shall establish a sufficiently close
relationship between $r$ and $p_{n+1}$ that the same analysis can then be
iterated to arbitrary depth, showing that $q$ has a spinal structure as
required.

The main complication is that $r$ need not superficially resemble $p_{n+1}$,
since within $r$, the crucial application of $g$ that effectively computes the
value of $p_{n+1}$ may be preceded by other ‘time-wasting’ applications of $g$
(the idea is illustrated by the example $Z_{1}$ above). However, it turns out
that such time-wasting subterms $ga^{1}r^{1}o^{1}$ must be of a certain kind
if the extensional behaviour $q\approx p_{n}$ is not to be jeopardized: in
particular, the first argument $a^{1}$ must evaluate to some $i<n$. (As in the
example of $Z_{1}$, the idea is that if the subterm $ga^{1}r^{1}o^{1}$ merely
repeats some ‘outer’ evaluation, it will make no overall difference to the
extension if the evaluation of this subterm does not terminate.) In order to
formulate the relationship between $r$ and $p_{n+1}$, we therefore need a
means of skipping past such time-wasting applications in order to reach the
application of $g$ that does the real work. We achieve this with the help of a
_masking_ operator $\mu_{n,n^{\prime}}$, which (for any $n\leq n^{\prime}$)
overrides the behaviour of $g$ on numerical arguments $n\leq i<n^{\prime}$
with a trivial behaviour returning the dummy value $0$.

We now proceed to our formal development. As a brief comment on notation, we
recall from Section 2 that the relations $\approx$ and $\preceq$ of
observational equivalence and inequality make sense not just for elements of
${\mathsf{SP}}^{0}$ but for arbitrary meta-terms (including applications),
closed or otherwise. Throughout this section, for typographical convenience,
we will tend to express the required relationships mostly at the level of
meta-terms, writing for instance $pq\approx\lambda.n$ rather than the
equivalent $\ll pq\gg\,=\lambda.n$ or $p\cdot q=\lambda.n$. We shall also
perpetrate other mild abuses of notation, such as writing a procedure
$\lambda.n$ simply as $n$ (except for special emphasis), $\lambda\vec{x}.\bot$
as $\bot$, $x^{\eta}$ as $x$, a meta-expression
${\mathtt{case}}\;A\;{\mathtt{of}}\;(i\Rightarrow i)$ just as $A$, and
abbreviating a substitution $[g\mapsto G,\,x\mapsto X]$ to $[G,X]$.

We shall say that $G\in{\mathsf{SP}}^{0}(0\rightarrow(k+1)\rightarrow(k+1))$
is _strict_ if $G\bot ro\approx\bot$ for any $r,o$. Clearly, $G$ is strict iff
$G\approx\lambda izx.\,{\mathtt{case}}\;i\;{\mathtt{of}}\;(j\Rightarrow
G(\lambda.j)z^{\eta}x^{\eta})$. In connection with meta-terms with free
variable $g$, we shall write $T\approx^{\prime}T^{\prime}$ to mean that
$T[g\mapsto G]\approx T^{\prime}[g\mapsto G]$ for all _strict_ $G$; the
notation $\preceq^{\prime}$ is used similarly. We shall actually analyse the
syntactic forms of procedures $g\vdash q$ based on the assumption that
$q\succeq^{\prime}p_{n}$, where $p_{n}$ is the canonical procedure for
$\Phi^{n}[g]$ as above.

We shall say a procedure $g\vdash q$ is _simple_ if for every application
$garo$ appearing within $q$, the first argument $a$ is just a numeral
$\lambda.n$. The following observation simplifies our analysis of terms
considerably; it uses the operator ${\mathit{byval}}$ and its NSP
interpretation, as introduced at the end of Section 4.

###### Proposition 29

If there is a procedure $g\vdash q\succeq^{\prime}p_{n}$-denotable in
${\mathrm{PCF}}^{\Omega}_{k}$, then there is a simple procedure $g\vdash
q^{\prime}\succeq^{\prime}p_{n}$ denotable in
${\mathrm{PCF}}^{\Omega}_{k}+{\mathit{byval}}$.

Proof Suppose $g\vdash q$ is ${\mathrm{PCF}}^{\Omega}_{k}$-denotable where
$q\succeq^{\prime}p_{n}$, and write

$S[g]~{}=~{}\lambda izx.\,{\mathtt{case}}\;i\;{\mathtt{of}}\;(j\Rightarrow
g(\lambda.j)z^{\eta}x^{\eta})\;.$

It is easy to see that

$S[g]~{}=~{}[\\![\lambda izx.\,{\mathit{byval}}\,(\lambda
j.gjzx)\,i\,]\\!]_{g}\;.$

Take $g\vdash q^{\prime}=\,\ll q[g\mapsto S[g]]\gg$, so that $q^{\prime}$ is
denotable in ${\mathrm{PCF}}^{\Omega}_{k}+{\mathit{byval}}$. Then
$q\approx^{\prime}q^{\prime}$ since $S[G]\approx G$ for all strict $G$, so
$q^{\prime}\succeq^{\prime}p_{n}$. Finally, $q^{\prime}$ is clearly simple:
every occurrence of $g$ within $q[g\mapsto S[g]]$ has a numeral as its first
argument, so the same will be true of $\ll q[g\mapsto S[g]]\gg$. $\Box$

For any $n\leq n^{\prime}$, let us define the _masking_
$\mu_{n,n^{\prime}}(g)$ of $g$ to be the following procedure term (here
$\rho=0\rightarrow(k+1)\rightarrow(k+1)$):

$g^{\rho}~{}\vdash~{}\mu_{n,n^{\prime}}(g)~{}=~{}\lambda
izx.\,{\mathtt{case}}\;i\;{\mathtt{of}}\;(n\Rightarrow 0\mid\cdots\mid
n^{\prime}-1\Rightarrow 0\mid-\Rightarrow gizx)~{}:~{}\rho\;.$

(The wildcard symbol ‘$-$’ covers all branch indices not covered by the
preceding clauses.) We may also write $\mu_{n,n^{\prime}}(P)$ for
$\mu_{n,n^{\prime}}(g)[g\mapsto P]$ if $P$ is any meta-procedure of type
$\rho$. We write $\mu_{n,n+1}$ simply as $\mu_{n}$; note also that
$\mu_{n,n}(g)\approx^{\prime}g$. Clearly
$\mu_{n}(\mu_{n+1}(\cdots(\mu_{n^{\prime}-1}(g))\cdots))\approx\mu_{n,n^{\prime}}(g)$.

We shall say that a closed meta-term $\vdash P:\rho$ is _trivial at $n$_ if
$P(\lambda.n)\bot\bot\approx 0$. Note that $\mu_{n,n^{\prime}}(G)$ is trivial
at each of $n,\ldots,n^{\prime}-1$ for any closed $G$; indeed, $G$ is trivial
at $n,\ldots,n^{\prime}-1$ iff $G\succeq^{\prime}\mu_{n,n^{\prime}}(G)$.

The following lemma now implements our syntactic analysis of the top-level
structure of simple procedures $q\succeq^{\prime}p_{n}$.

###### Lemma 30

Suppose $g\vdash q$ is simple and $q\succeq^{\prime}p_{n}$. Then $q$ has the
form $\lambda x^{k}.\,{\mathtt{case}}\;garo\;{\mathtt{of}}\;(\cdots)$, where:

  1. 1.

$a=\lambda.n$,

  2. 2.

$o[g\mapsto G]\succeq x^{\eta}$ whenever $\vdash G$ is trivial at $n$,

  3. 3.

$r[g\mapsto\mu_{n}(g),\,x\mapsto X]\succeq^{\prime}p_{n+1}$ for any $X$.

Proof Suppose $q=\lambda x^{k}.e$. Clearly $e$ is not constant since $q\succeq
p_{n}$; and if $e$ had head variable $x$, we would have $q[g\mapsto\lambda
izx.\,{\mathtt{case}}\;i\;{\mathtt{of}}\;(-\Rightarrow 0)](\lambda
w.\bot)=\bot$, whereas $p_{n}[g\mapsto\lambda
izx.\,{\mathtt{case}}\;i\;{\mathtt{of}}\;(-\Rightarrow 0)](\lambda w.\bot)=0$,
contradicting $q\succeq^{\prime}p_{n}$. So $e$ has the form
${\mathtt{case}}\;garo\;{\mathtt{of}}\;(\cdots)$.

For claim 1, we have $a=\lambda.m$ for some $m\in\mathbb{N}$ because $q$ is
simple. Suppose that $m\neq n$, and consider

$G^{\prime}~{}=~{}\lambda
izx.\,{\mathtt{case}}\;i\;{\mathtt{of}}\;(n\Rightarrow
0\mid-\Rightarrow\bot)\;.$

Then for any $X$, clearly $q[G^{\prime}]X\approx\bot$, whereas
$p_{n}[G^{\prime}]X\approx G^{\prime}(\lambda.n)(\cdots)X\approx 0$,
contradicting $q\succeq^{\prime}p_{n}$. Thus $a=\lambda.n$.

For claim 2, suppose that $G(\lambda.n)\bot\bot\approx 0$ but not $o[G]\succeq
x^{\eta}$; then we may take $X\in{\mathsf{SP}}^{0}({k})$ and
$u\in{\mathsf{SP}}^{0}({k-1})$ such that $Xu\approx l\in\mathbb{N}$ but
$o[G,X]u\not\approx l$. Now define

$G^{\prime}~{}=~{}\lambda
izx.\,{\mathtt{case}}\;i\;{\mathtt{of}}\;(j\Rightarrow{\mathtt{case}}\;xu\;{\mathtt{of}}\;(l\Rightarrow
Gjzx\mid-\Rightarrow\bot))\;.$

Then $G^{\prime}\preceq G$, so $o^{*}u\not\approx l$ where
${}^{*}=[G^{\prime},X]$; hence $G^{\prime}a^{*}r^{*}o^{*}\approx\bot$ and so
$q[G^{\prime}]X\approx\bot$. On the other hand, we have

$\displaystyle p_{n}[G^{\prime}]X$ $\displaystyle\approx$
$\displaystyle{\mathtt{case}}\;G^{\prime}(\lambda.n)p_{n+1}^{*}X\;{\mathtt{of}}\;(i\Rightarrow
i)$ $\displaystyle\approx$
$\displaystyle{\mathtt{case}}\;Xu\;{\mathtt{of}}\;(l\Rightarrow
G(\lambda.n)p_{n+1}^{*}X)~{}\approx~{}0\;,$

contradicting $q\succeq^{\prime}p_{n}$ (note that $G^{\prime}$ is strict).
Thus $o[G]\succeq x^{\eta}$.

For claim 3, suppose that $p_{n+1}[G]X^{\prime}\approx l$ for some strict
$G\in{\mathsf{SP}}^{0}(\rho)$ and $X^{\prime}\in{\mathsf{SP}}^{0}(k)$. We wish
to show that $r[\mu_{n}(G),X]X^{\prime}\approx l$ for any $X$. Suppose not,
and consider

$G^{\prime}~{}=~{}\lambda
izx.\,{\mathtt{case}}\;i\;{\mathtt{of}}\;(n\Rightarrow{\mathtt{case}}\;zX^{\prime}\;{\mathtt{of}}\;(l\Rightarrow
0\mid-\Rightarrow\bot)\mid-\Rightarrow Gizx)\;.$

Then $G^{\prime}\preceq\mu_{n}(G)$, so $r[G^{\prime},X]X^{\prime}\not\approx
l$. Moreover, since $a=\lambda.n$ by claim 1, we see that
$G^{\prime}a^{*}r^{*}o^{*}\approx\bot$, where ${}^{*}=[G^{\prime},X]$, so that
$q[G^{\prime}]X\approx\bot$. On the other hand, we have

$\displaystyle p_{n}[G^{\prime}]X$ $\displaystyle\approx$
$\displaystyle{\mathtt{case}}\;G^{\prime}(\lambda.n)p_{n+1}^{*}X\;{\mathtt{of}}\;(i\Rightarrow
i)$ $\displaystyle\approx$
$\displaystyle{\mathtt{case}}\;p_{n+1}^{*}X^{\prime}\;{\mathtt{of}}\;(l\Rightarrow
0)\;.$

Here, since $p_{n+1}$ does not contain $x$ free, we have
$p_{n+1}^{*}=p_{n+1}[G^{\prime}]$. But it is easy to see that
$p_{n+1}[G^{\prime}]\approx p_{n+1}[G]$, since every occurrence of $g$ within
$p_{n+1}$ is applied to $\lambda.n^{\prime}$ for some $n^{\prime}>n$, and for
all such $n^{\prime}$ we have $G^{\prime}(\lambda.n^{\prime})\approx
G(\lambda.n^{\prime})$. (Since $p_{n+1}$ contains infinitely many applications
of $g$, an appeal to continuity is formally required here.) But
$p_{n+1}[G]X^{\prime}\approx l$ by assumption; thus
$p_{n+1}^{*}X^{\prime}\approx l$, allowing us to complete the proof that
$p_{n}[G^{\prime}]X\approx 0$. Once again, this contradicts
$q\succeq^{\prime}p_{n}$, so claim 3 is established. $\Box$

In the light of Appendix A, one may strengthen claim 2 of the above lemma by
writing $o[g\mapsto G]\approx x^{\eta}$. This gives a fuller picture of the
possible forms of terms $q\approx p_{n}$, but is not needed for showing that
such $q$ are spinal.

We have now almost completed a circle, in the sense that claim 3 tells us that
$\ll r[g\mapsto\mu_{n}(g),x\mapsto X]\gg$ itself satisfies the hypothesis for
$q$ (with $n+1$ in place of $n$). However, there still remains a small
mismatch between the hypothesis and the conclusion, in that claim 3 concerns
not $r$ itself but rather $\ll r[g\mapsto\mu_{n}(g)]\gg$. (In the light of
claim 3, the variable $x$ may be safely ignored here.) This mismatch is
repaired by the following lemma, which lends itself to iteration to any depth.
Note the entry of a term context $E[-]$ here.

###### Lemma 31

Suppose $g\vdash q$ is simple and
$q[g\mapsto\mu_{n,n^{\prime}}(g)]\succeq^{\prime}p_{n^{\prime}}$. Then $q$ has
the form $\lambda x^{k}.\,E[{\mathtt{case}}\;garo\;{\mathtt{of}}\;(\cdots)]$,
where:

  1. 1.

$E[-]$ has empty local variable environment,

  2. 2.

$a=\lambda.n^{\prime}$,

  3. 3.

$o[g\mapsto G]\succeq x^{\eta}$ whenever $\vdash G$ is trivial at
$n,\cdots,n^{\prime}$,

  4. 4.

$r[g\mapsto\mu_{n,n^{\prime}+1}(g),\,x\mapsto
X]\succeq^{\prime}p_{n^{\prime}+1}$ for any $X$.

Proof Let $q^{\prime}=\,\ll q[g\mapsto\mu_{n,n^{\prime}}(g)]\gg$. Under the
above hypotheses, we have by Lemma 30 that $q^{\prime}$ is of the form
$\lambda
x.\,{\mathtt{case}}\;ga^{\prime}r^{\prime}o^{\prime}\;{\mathtt{of}}\;(\cdots)$,
where $a^{\prime}=\lambda.n^{\prime}$, $o^{\prime}[g\mapsto G]\succeq
x^{\eta}$ whenever $G$ is trivial at $n^{\prime}$, and
$r^{\prime}[g\mapsto\mu_{n^{\prime}}(g)]\succeq^{\prime}p_{n^{\prime}+1}$.
Write $q$ as $\lambda x.\,E[{\mathtt{case}}\;garo\;{\mathtt{of}}\;(\cdots)]$
where the displayed occurrence of $g$ originates the head $g$ of $q^{\prime}$
via the substitution ${}^{\dagger}=[g\mapsto\mu_{n,n^{\prime}}(g)]$.

Suppose that the hole in $E[-]$ appeared within an abstraction $\lambda y.-$;
then the hole in $E[g\mapsto\mu_{n,n^{\prime}}(g)][-]$ would likewise appear
within such an abstraction. Moreover, the evaluation of
$q[g\mapsto\mu_{n,n^{\prime}}(g)]$ consists simply of the contraction of
certain expressions
$\mu_{n,n^{\prime}}(g)(\lambda.m)r^{\prime\prime}o^{\prime\prime}$ to either
$0$ or $g(\lambda.m)r^{\prime\prime}o^{\prime\prime}$, followed by some
reductions ${\mathtt{case}}\;0\;{\mathtt{of}}\;(i\Rightarrow
e_{i})\rightsquigarrow e_{0}$; thus, any residue in $q^{\prime}$ of the
critical $g$ identified above will likewise appear underneath $\lambda y$. But
this is impossible, because the head $g$ of $q^{\prime}$ is a residue of this
$g$ by assumption. This establishes condition 1.

In the light of this, by Lemma 26(i) we have $a^{\prime}\approx a^{\dagger}$,
$o^{\prime}\approx o^{\dagger}$ and $r^{\prime}\approx r^{\dagger}$. But since
$q$ is simple, $a$ is a numeral, so $a=\lambda.n^{\prime}$, giving condition
2. For condition 3, suppose $G$ is trivial at $n,\ldots,n^{\prime}$. Then
$G\succeq\mu_{n,n^{\prime}+1}(G)$, so that

$o[g\mapsto
G]~{}\succeq~{}o[g\mapsto\mu_{n,n^{\prime}}(\mu_{n^{\prime}}(G))]~{}\approx~{}o^{\dagger}[g\mapsto\mu_{n^{\prime}}(G)]~{}\approx~{}o^{\prime}[g\mapsto\mu_{n^{\prime}}(G)]~{}\succeq~{}x^{\eta}\;,$

since $\mu_{n^{\prime}}(G)$ is trivial at $n^{\prime}$. Condition 4 also holds
since $r^{\prime}[g\mapsto\mu_{n^{\prime}}(g)]\approx
r^{\dagger}[g\mapsto\mu_{n^{\prime}}(g)]\approx
r[g\mapsto\mu_{n,n^{\prime}+1}(g)]$, where
$r^{\prime}[g\mapsto\mu_{n^{\prime}}(g)]\succeq^{\prime}p_{n^{\prime}+1}$.
$\Box$

###### Corollary 32

If $g\vdash q$ is simple and $q\succeq^{\prime}p_{n}$, then $q$ is spinal (in
the modified sense).

Proof Since condition 3 of the above lemma matches its hypotheses, starting
from the assumption that
$q\approx^{\prime}q[g\mapsto\mu_{n,n}(g)]\succeq^{\prime}p_{n}$, we may apply
the lemma iteratively to obtain a spinal structure as prescribed by Definition
24 (subject to the relevant adjustments for
$g:0\rightarrow(k+1)\rightarrow(k+1)$). Note that at each level, a suitable
substitution ∘ will be the closed one that specializes $g$ to $\lambda izx.0$
(which is trivial at all $n$), and all variables $x^{k}$ other than the
innermost-bound one to $\bot$. $\Box$

Thus, if there exists a ${\mathrm{PCF}}^{\Omega}_{k}$-denotable procedure
$t\approx\lambda g.p_{0}$, for instance, then by Proposition 29 there is also
a simple such procedure $t^{\prime}$ denotable in
${\mathrm{PCF}}^{\Omega}_{k}+{\mathit{byval}}$, and by Corollary 32, this
$t^{\prime}$ will be spinal in the modified sense. But this contradicts
Theorem 28 (understood relative to the modified setting, and applied to
${\mathrm{PCF}}^{\Omega}_{k}+{\mathit{byval}}$ as indicated at the end of
Section 4). We conclude that no $t\approx\lambda g.p_{0}$ can be
${\mathrm{PCF}}^{\Omega}_{k}$-denotable. Since the interpretation of
${\mathrm{PCF}}^{\Omega}_{k}$ in ${\mathsf{SF}}$ factors through
${\mathsf{SP}}^{0}$, this in turn means that within the model ${\mathsf{SF}}$,
the element $[\\![\lambda g.\,\Phi^{0}[g]]\\!]$ is not denotable in
${\mathrm{PCF}}^{\Omega}_{k}$. On the other hand, this element is obviously
denotable relative to $Y_{{0}\rightarrow(k+1)}\in{\mathsf{SF}}$ even in
${\mathrm{PCF}}_{1}$, so the proof of Theorems 1(i) and 2(i) is complete. This
establishes Berger’s conjecture, and also suffices for the proof of Corollary
3.

##  6 Extensional non-definability of $Y_{k+1}$

We have so far shown that the element $Y_{0\rightarrow(k+1)}\in{\mathsf{SF}}$
is not ${\mathrm{PCF}}^{\Omega}_{k}$-denotable. We shall now refine our
methods slightly to show that even $Y_{k+1}\in{\mathsf{SF}}$ is not
${\mathrm{PCF}}^{\Omega}_{k}$-denotable. Since $\overline{k+1}$ is clearly a
${\mathrm{PCF}}_{0}$-definable retract of every level $k+1$ type, this will
establish that no $Y_{\sigma}\in{\mathsf{SF}}$ where
${\mathrm{lv}}(\sigma)=k+1$ is denotable in ${\mathrm{PCF}}^{\Omega}_{k}$.

The idea is as follows. Within each type level $k\geq 1$, we can stratify the
types into _sublevels_ $(k,l)$ where $l=1,2,\ldots$, essentially by taking
account of the ‘width’ of the type as well as its depth. We thus obtain a
sublanguage ${\mathrm{PCF}}^{\Omega}_{k,l}$ of ${\mathrm{PCF}}^{\Omega}_{k}$
by admitting $Y_{\sigma}$ only for types $\sigma$ of sublevel $(k,l)$ or
lower. We show that, roughly speaking, all our previous methods can be adapted
to show that for a given $k$, the languages ${\mathrm{PCF}}^{\Omega}_{k,l}$
for $l=1,2,\ldots$ form a strict hierarchy. (This is true as regards
definability in ${\mathsf{SP}}^{0}$; for ${\mathsf{SF}}$, we will actually
show only that ${\mathrm{PCF}}^{\Omega}_{k,l}$ is strictly weaker than
${\mathrm{PCF}}^{\Omega}_{k,l+2}$.) This more refined hierarchy is of some
interest in its own right, and illustrates that the structure of
${\mathsf{SF}}$ is much richer than that manifested by the pure types.999This
contrasts with the situation for extensional _total_ type structures over
$\mathbb{N}$, for example. There, under mild conditions, every simple type is
isomorphic to a pure type: see Theorem 4.2.9 of [17].

Any term of ${\mathrm{PCF}}^{\Omega}_{k}$ will be a term of some
${\mathrm{PCF}}^{\Omega}_{k,l}$. Previously we showed only that no such term
could define $Y_{0\rightarrow(k+1)}\in{\mathsf{SF}}$; however, we now see that
there is actually plenty of spare headroom between
${\mathrm{PCF}}^{\Omega}_{k,l}$ and the pure type $k+1$. Specifically, there
are operators $Y_{\sigma}$ in ${\mathrm{PCF}}^{\Omega}_{k,l+2}$ that are not
${\mathrm{PCF}}^{\Omega}_{k,l}$-denotable; and since all such $\sigma$ are of
level $\leq k$ and are thus easily seen to be retracts of $\overline{k+1}$, we
may conclude that $Y_{k+1}\in{\mathsf{SF}}$ is not
${\mathrm{PCF}}^{\Omega}_{k}$-denotable.

The following definition sets out the more fine-grained stratification of
types that we shall use.

###### Definition 33

(i) The _width_ $w(\sigma)$ of a type $\sigma$ is defined inductively as
follows:

$w({\mathtt{N}})~{}=~{}0\;,~{}~{}~{}~{}~{}~{}~{}~{}w(\sigma_{0},\ldots,\sigma_{r-1}\rightarrow{\mathtt{N}})~{}=~{}\max(r,w(\sigma_{0}),\ldots,w(\sigma_{r-1}))\;.$

For $k,l\geq 1$, we say $\sigma$ has _sublevel_ $(k,l)$ if
${\mathrm{lv}}(\sigma)=k$ and $w(\sigma)=l$. If $\sigma={\mathtt{N}}$, we
simply say that $\sigma$ has _sublevel_ $0$. We order sublevels in the obvious
way: $0$ is the lowest sublevel, and $(k,l)<(k^{\prime},l^{\prime})$ if either
$k<k^{\prime}$ or $k=k^{\prime}$ and $l<l^{\prime}$.

(ii) For each $k,l$ we define a type $\rho_{k,l}$ by:

$\rho_{0,l}~{}=~{}{\mathtt{N}}\;,~{}~{}~{}~{}~{}~{}~{}~{}\rho_{k+1,l}~{}=~{}\rho_{k,l},\ldots,\rho_{k,l}\rightarrow{\mathtt{N}}\mbox{~{}~{}($l$
arguments)}\;.$

When $k,l\geq 1$, we may call $\rho_{k,l}$ the _homogeneous_ type of sublevel
$(k,l)$.

The following facts are easily established. Here we shall say that $\sigma$ is
a _simple retract_ of $\tau$ if there is a ${\mathrm{PCF}}_{0}$-definable
retraction $\sigma\lhd\tau$ within ${\mathsf{SP}}^{0}$.

###### Proposition 34

(i) For $k\geq 1$, every type of sublevel $(k,l)$ or lower is a simple retract
of $\rho_{k,l}$. Hence, for all $k\geq 0$, for every finite list of types
$\sigma_{i}$ of level $\leq k$, there is some $l$ such that each $\sigma_{i}$
is a simple retract of $\rho_{k,l}$.

(ii) Every finite product of level $\leq k$ types is a simple retract of
$\overline{k+1}$.

(iii) If $\sigma$ is a simple retract of $\tau$, then $Y_{\sigma}$ is
${\mathrm{PCF}}_{0}$-definable from $Y_{\tau}$ in ${\mathsf{SP}}_{0}$.

Proof (i) The first claim (for $k\geq 1$) is easy by induction on $k$, and the
second claim (which is trivial when $k=0$) follows easily.

(ii) By induction on $k$. The case $k=0$ is easy. For $k\geq 1$, suppose
$\sigma_{0},\ldots,\sigma_{m-1}$ are level $\leq k$ types, where
$\sigma_{i}=\tau_{i0},\ldots,\tau_{i(n_{i}-1)}\rightarrow{\mathtt{N}}$ for
each $i$. Here the $\tau_{ij}$ are of level at most $k-1$, so by (i), we may
choose $l$ such that each $\tau_{ij}$ is a simple retract of $\rho_{k-1,l}$.
Taking $n=\max_{i}n_{i}$, we then have that each $\sigma_{i}$ is a simple
retract of $\rho_{k-1,l},\ldots,\rho_{k-1,l}\rightarrow{\mathtt{N}}$ (with $n$
arguments). The product $\Pi_{i}\sigma_{i}$ is therefore a simple retract of
the type
$\sigma={\mathtt{N}},\rho_{k-1,l},\ldots,\rho_{k-1,l}\rightarrow{\mathtt{N}}$.
But by the induction hypothesis, the product of
${\mathtt{N}},\rho_{k-1,l},\ldots,\rho_{k-1,l}$ is a simple retract of
$\overline{k}$ whence $\sigma$ itself is a simple retract of $\overline{k+1}$.

We leave (iii) as an exercise. $\Box$

Next, we adapt the proof of Theorem 12 to establish the crucial gap between
$\rho_{k,l}$ and $\rho_{k,l+1}$. This gives an indication of how our methods
may be used to map out the embeddability relation between types in finer
detail, although we leave an exhaustive investigation of this to future work.

###### Theorem 35

Suppose $k\geq 1$. Within ${\mathsf{SF}}$, the type $\rho_{k,l+1}$ is not a
pseudo-retract of any finite product of types of sublevel $\leq(k,l)$ or
lower.

Proof In view of Proposition 34(i), it will suffice to show that
$\rho_{k,l+1}$ is not a pseudo-retract of a finite power of $\rho_{k,l}$. We
argue by induction on $k$. The arguments for both the base case $k=1$ and the
step case $k>1$ closely parallel the argument for the step case in Theorem 12,
so we treat these two cases together as far as possible, omitting details that
are easy adaptations of those in the earlier proof.

Suppose for contradiction that there were procedures

$z^{\rho}\vdash
t_{i}:\sigma~{}~{}(i<m)\;,~{}~{}~{}~{}~{}~{}~{}~{}x_{0}^{\sigma},\ldots,x_{m-1}^{\sigma}\vdash
r:\rho\;,$

where $\rho=\rho_{k,l+1}$, $\sigma=\rho_{k,l}$, such that $z\vdash
r[\vec{x}\mapsto\vec{t}\,]\succeq z^{\eta}$. Let $v=\,\ll
r[\vec{x}\mapsto\vec{t}\,]\gg$, so that $z\vdash v\succeq z^{\eta}$. As in the
proof of Theorem 12, one may show that $v$ has the form $\lambda f_{0}\ldots
f_{l}.\,{\mathtt{case}}\;zp_{0}\ldots p_{l}\;{\mathtt{of}}\;(\cdots)$ where
$p_{i}[z\mapsto\lambda\vec{w}.0]\succeq f_{i}$ for each $i$. Next, we note
that $r[\vec{x}\mapsto\vec{t}\,]$ reduces in finitely many steps to a head
normal form $\lambda f_{0}\ldots f_{l}.\,{\mathtt{case}}\;zP_{0}\ldots
P_{l}\;{\mathtt{of}}\;(\cdots)$ where $\ll P_{i}\gg\,=p_{i}$ for each $i$;
moreover, the ancestor of the leading $z$ here must lie within some $t_{i}$,
say at the head of some subterm $z\vec{P}\,^{\prime}$, where $\vec{P}$ is an
instance of $\vec{P}\,^{\prime}$ via some substitution †.

At this point, the arguments for the base case and step case part company. In
the base case $k=1$, we have that $z^{\rho}\vdash t_{i}:\sigma$ where
$\rho={\mathtt{N}}^{l+1}\rightarrow{\mathtt{N}}$ and
$\sigma={\mathtt{N}}^{l}\rightarrow{\mathtt{N}}$; thus there are no bound
variables within $t_{i}$ except the top-level ones—say $w_{0},\ldots,w_{l-1}$,
all of type ${\mathtt{N}}$. So in fact † has the form
$[\vec{w}\mapsto\vec{W}]$ for certain meta-terms
$f_{0}^{\mathtt{N}},\ldots,f_{l}^{\mathtt{N}},z\vdash W_{j}:{\mathtt{N}}$. Now
consider the terms $f_{0},\ldots,f_{l}\vdash\vec{W}^{*}$ and
$\vec{w}\vdash\vec{P}\,^{\prime}{}^{*}$, writing ∗ for the substitution
$[z\mapsto\lambda w.0]$. These compose to yield
$\vec{f}\,\vdash\,\ll\vec{P}\,^{*}\gg\,=\,\ll\vec{p}\,^{*}\gg\,\succeq f$, so
we have expressed ${\mathtt{N}}^{l+1}$ as a pseudo-retract of
${\mathtt{N}}^{l}$ within ${\mathsf{SF}}$. As already noted in the course of
the proof of Theorem 12, this is impossible.

For the step case $k>1$, we proceed much as in the proof of Theorem 12, using
the substitution † to express $\rho_{k-1,l+1}$ as a retract of a finite
product of types of sublevel $(k-1,l)$ or lower, contrary to the induction
hypothesis. We leave the remaining details as an exercise. $\Box$

We now outline how the ideas of Sections 3, 4 and 5 may be adapted to show
that $Y_{\rho_{k,l+1}}\in{\mathsf{SP}}^{0}$ is not
${\mathrm{PCF}}^{\Omega}_{k,l}$-denotable. We assume that $k\geq 2$ for the
time being (the case $k=1$ will require special treatment). The adaptations
are mostly quite systematic: the type $\rho_{k,l+1}$ now plays the role of
$\overline{k+1}$; types of sublevel $\leq(k,l)$ play the role of types of
level $\leq k$; $\rho_{k-1,l+1}$ plays the role of $\overline{k}$; and types
of sublevel $\leq(k-1,l)$ play the role of types of level $<k$. Since the
proof we are adapting is quite lengthy, we leave many routine details to be
checked by the reader.

First, the evident adaptation of Definition 18 yields a notion of _$k,l$
-plugging_ where the plugging variables are required to be of sublevel
$\leq(k,l)$, and we thus obtain an inductive characterization of the
${\mathrm{PCF}}^{\Omega}_{k,l}$-denotable procedures analogous to Theorem 20.
We also adapt the notion of _regular_ meta-term as follows:

###### Definition 36

Suppose $g:\rho_{k,l+1}\rightarrow\rho_{k,l+1}$ for $k,l\geq 1$. An
environment $\Gamma$ is _$g$ -($k,l$-)regular_ if $\Gamma$ contains $g$ but no
other variables of sublevel $>(k,l)$. A meta-term $T$ is $g$-regular if it
contains no variables of sublevel $>(k,l)$ except possibly for free
occurrences of $g$. We say $\Gamma\vdash T$ is $g$-regular if both $\Gamma$
and $T$ are $g$-regular.

Next, we proceed to the ideas of Section 4. Our convention here will be that
$\Gamma$ ranges over regular environments, and Roman capitals $V,Z$ range over
sets of variables of sublevel $\leq(k,l)$. The notions of $x,V$-closed
substitution and spinal term carry over as follows:

###### Definition 37

Suppose $g:\rho_{k,l+1}\rightarrow\rho_{k,l+1}$ where $k\geq 2$ and $l\geq 1$.

(i) If $\vec{x}$ is a list of variables of type $\rho_{k-1,l+1}$ and $V$ a set
of variables of sublevel $\leq(k,l)$, a substitution
${}^{\circ}=[\vec{w}\mapsto\vec{r}\,]$ is called _$\vec{x},V$ -closed_ if the
$r_{i}$ contain no free variables, except that if $w_{i}\in V$ and $w_{i}$ is
of sublevel $\leq(k-1,l)$ then $r_{i}$ may contain the $\vec{x}$ free.

(ii) Suppose $\Gamma\vdash e$ is $g$-$k,l$-regular and
$\vec{x},V\subseteq\Gamma$. We coinductively declare $e$ to be _$g$ -head-
spinal_ w.r.t. $\vec{x},V$ iff $e$ has the form
${\mathtt{case}}\;g(\lambda\vec{x}\,^{\prime}.E[e^{\prime}])\vec{o}\;{\mathtt{of}}\;(\cdots)$,
where $E[-]$ is an expression context, and

  * •

for some $\vec{x},V$-closed specialization ∘ covering the free variables of
$\vec{o}$ other than those of $\vec{x}$, we have
$\vec{o}\,^{\circ}\succeq\vec{x}^{\,\eta}$,

  * •

$e^{\prime}$ is $g$-head-spinal w.r.t. $\vec{x}\,^{\prime},V^{\prime}$, where
$V^{\prime}$ is the local variable environment for $E[-]$.

(iii) We say a regular term $\Gamma\vdash t$ is _$g$ -spinal_ if it contains a
$g$-head-spinal subexpression w.r.t. some $\vec{x},V$.

Lemma 26 and its proof go through with the above adaptations; here the local
environments $\vec{v},\vec{v}\,^{\prime}$ are now of sublevel $\leq(k,l)$, and
part (iii) of the lemma now states that if $K[-]$ contains no redexes with
operator of sublevel $>(k,l)$, then the substitution † is trivial for
variables of sublevel $\geq(k-1,l+1)$. The crucial Lemma 27, which forms the
heart of our proof, now translates as follows:

###### Lemma 38

Suppose $g:\rho_{k,l+1}\rightarrow\rho_{k,l+1}$ and we have $g$-regular terms

$\Gamma,\vec{v}\;\vdash~{}d~{}=~{}{\mathtt{case}}\;gpq\;{\mathtt{of}}\;(\cdots)\;,~{}~{}~{}~{}~{}~{}\Gamma,\vec{v}\,^{\prime}\vdash\vec{s}\,,$

where $\vec{v},\vec{v}\,^{\prime}$ are of sublevel $\leq(k,l)$, and
$\Gamma,\vec{v}\,^{\prime}\vdash\,\ll d[\vec{v}\mapsto\vec{s}\,]\gg$ is
$g$-head-spinal with respect to some $\vec{x},V$. Then $d$ itself is
$g$-spinal.

The entire proof of this lemma translates systematically according to the
correspondences we have indicated, invoking Theorem 35 for the fact that
$\rho_{k-1,l+1}$ is not a pseudo-retract of a product of sublevel
$\leq(k-1,l)$ types. The analogue of Theorem 28 now goes through readily, so
we obtain:

###### Theorem 39

If $k\geq 2$ and $l\geq 1$, every ${\mathrm{PCF}}^{\Omega}_{k,l}$-denotable
procedure is non-$g$-spinal where $g:\rho_{k,l+1}\rightarrow\rho_{k,l+1}$.
$\Box$

As in our original proof, we will actually use a version of this theorem for
the modified notion of spinal term that incorporates the extra argument $b$,
and for the extension of ${\mathrm{PCF}}^{\Omega}_{k,l}$ with the operator
${\mathit{byval}}$.

To adapt the material of Section 5, we now take $g$ to be a variable of type
$0\rightarrow\rho_{k,l+1}\rightarrow\rho_{k,l+1}$, and argue that the
${\mathrm{PCF}}_{k,l+2}$-denotable element $\Phi=\lambda
g.\,Y_{0\rightarrow\rho_{k,l+1}}(\lambda fn.\,g\,n\,(f({\mathit{suc}}\,n)))$
within ${\mathsf{SF}}$ is not ${\mathrm{PCF}}^{\Omega}_{k,l}$-denotable. The
proof is a completely routine adaptation of that in Section 5. Since
$Y_{0\rightarrow\rho_{k,l+1}}$ is readily definable from $Y_{k+1}$ by
Proposition 34, this implies that $Y_{k+1}\in{\mathsf{SF}}$ is not
${\mathrm{PCF}}^{\Omega}_{k,l}$-denotable. We have thus shown:

###### Theorem 40

(i) For $k\geq 2$ and $l\geq 1$, the element
$Y_{0\rightarrow\rho_{k,l+1}}\in{\mathsf{SF}}$ is denotable in
${\mathrm{PCF}}_{k,l+2}$ but not in ${\mathrm{PCF}}^{\Omega}_{k,l}$.

(ii) For $k\geq 2$, the element $Y_{k+1}\in{\mathsf{SF}}$ is not denotable in
${\mathrm{PCF}}^{\Omega}_{k}$.

A slightly different approach is needed for the case $k=1$. This is because at
level $0$ our only type is ${\mathtt{N}}$, so we are unable to make a
distinction between sublevels $l$ and $l+1$. To establish Lemma 38 in this
case, we again wish to show that we cannot pass in the content of the relevant
$\vec{x}\,^{\prime}$ to the relevant $s_{i}$, but now the idea is to appeal to
the fact that $\vec{x}\,^{\prime}$ consists of $l+1$ variables of type
${\mathtt{N}}$, whereas $s_{i}$ accepts at most $l$ arguments of type
${\mathtt{N}}$. (We have already seen that ${\mathtt{N}}^{l+1}$ cannot be a
retract of ${\mathtt{N}}^{l}$.) However, we also need to exclude the
possibility that the substitution ∘ is being used to import some components of
$\vec{x}\,^{\prime}$. We can achieve this if we require ∘ to be actually
closed rather than just $\vec{x}\,^{\prime},V^{\prime}$-closed, and it turns
out that this is permissible if we also tighten our notion of spinal term
slightly, essentially to ensure that no intermediate applications of $g$
appear in between those declared to constitute the spine of the term:

###### Definition 41

Suppose $g:\rho_{1,l+1}\rightarrow\rho_{1,l+1}$ where $l\geq 1$.

Suppose $\Gamma\vdash e$ is $g$-$1,l$-regular and $\vec{x}\subseteq\Gamma$. We
coinductively declare $e$ to be _strongly $g$-head-spinal_ w.r.t. $\vec{x}$
iff $e$ has the form
${\mathtt{case}}\;g(\lambda\vec{x}\,^{\prime}.E[e^{\prime}])\vec{o}\;{\mathtt{of}}\;(\cdots)$,
where $E[-]$ is an expression context, and

  * •

the hole within $E[-]$ does not itself occur within an application $gpq$,

  * •

for some closed substitution ∘ covering the free variables of $\vec{o}$ other
than those of $\vec{x}$, we have $\vec{o}\,^{\circ}\succeq\vec{x}^{\,\eta}$,

  * •

$e^{\prime}$ is strongly $g$-head-spinal w.r.t. $\vec{x}\,^{\prime}$.

The notion of strongly $g$-spinal term follows suit.

The counterpart of Lemma 26 goes through as expected, although without part
(iii): the relevant sublevel distinction does not exist at type level $0$, and
we cannot conclude that the substitution in question is trivial for all
variables of type ${\mathtt{N}}$. We may now indicate the required changes to
Lemma 38 and its proof:

###### Lemma 42

Suppose $g:\rho_{1,l+1}\rightarrow\rho_{1,l+1}$ and we have $1,l$-regular
terms

$\Gamma,\vec{v}\;\vdash~{}d~{}=~{}{\mathtt{case}}\;gpq\;{\mathtt{of}}\;(\cdots)\;,~{}~{}~{}~{}~{}~{}\Gamma,\vec{v}\,^{\prime}\vdash\vec{s}\,,$

where $\vec{v},\vec{v}\,^{\prime}$ are of sublevel $\leq(1,l)$, and
$\Gamma,\vec{v}\,^{\prime}\vdash\,\ll d[\vec{v}\mapsto\vec{s}\,]\gg$ is
strongly $g$-head-spinal with respect to some $\vec{x}$. Then $d$ itself is
strongly $g$-spinal.

Proof The proof of Lemma 27 up to the end of the proof of Claim 1 adapts
straightforwardly, and is somewhat simplified by the fact that the
substitution ∘ is closed. As sketched above, the crucial contradiction is
provided by the fact that ${\mathtt{N}}^{l+1}$ is not a pseudo-retract of
${\mathtt{N}}^{l}$ in ${\mathsf{SF}}$.

For the remainder of the proof, the key point to note is that
$\vec{v}\,^{\prime\prime}$ (the local environment for $C[-]$) is actually
empty in this case. This is because $C[-]$ is in normal form and contains no
free variables of level $\geq 2$ except $g$, so any $\lambda$-term containing
the hole would need to appear as an argument to $g$. It would then follow that
the hole within $E[-]$ lay within an argument to some occurrence of $g$, as
precluded by the definition of strongly spinal term.

It follows trivially that the
$\vec{x}\,^{\prime},\vec{v}\,^{\prime\prime}$-closed substitution
${}^{\circ^{\prime}}$ constructed at the very end of the proof is actually
closed. Moreover, the spinal structure of $d^{\prime}$ identified by the proof
cannot contain any intermediate applications of $g$, since these would give
rise under evaluation to intermediate applications of $g$ in the spine of $\ll
d[\vec{v}\mapsto\vec{s}\,]\gg$ as precluded by Definition 41. Thus, the
identified spinal structure in $d^{\prime}$ is actually a strongly spinal
structure, and the argument is complete. $\Box$

A trivial adaptation of the proof of Theorem 28 now yields:

###### Theorem 43

No ${\mathrm{PCF}}^{\Omega}_{1,l}$-denotable procedure can be strongly
$g$-spinal where $g:\rho_{1,l+1}\rightarrow\rho_{1,l+1}$. $\Box$

As before, this adapts easily to a variable $g$ of type
$0\rightarrow\rho_{1,l+1}\rightarrow\rho_{1,l+1}$. From here on, we again
follow the original proof closely. The only additional point to note is that
in place of Corollary 32 we now require that any simple $g\vdash q$ with
$q\succeq^{\prime}p_{n}$ must be _strongly_ spinal, but this is already clear
from the proof of Lemma 31. We therefore have everything we need for:

###### Theorem 44

(i) For any $l\geq 1$,
$Y_{{\mathtt{N}}^{l+2}\rightarrow{\mathtt{N}}}\in{\mathsf{SF}}$ is not
denotable in ${\mathrm{PCF}}^{\Omega}_{1,l}$.

(ii) $Y_{2}\in{\mathsf{SF}}$ is not denotable in
${\mathrm{PCF}}^{\Omega}_{1}$. $\Box$

The proof of Theorems 1 and 2 is now complete.

##  7 Related and future work

###  7.1 Other hierarchies of Y-combinators

There have been a number of previous results from various research traditions
showing that in some sense the power of level $k$ recursions increases
strictly with $k$. Whilst many of these results look tantalizingly similar to
ours, it turns out on inspection that their mathematical substance is quite
different, and we do not expect any substantial technical connections with our
own work to be forthcoming. Nonetheless, it is interesting to see how
strikingly different ideas and methods arising in other contexts can lead to
superficially similar results.

Previous results to the effect that $Y$-combinators for level $k+1$ are not
definable from those for level $k$ have been obtained by Damm [6] and Statman
[27]. It is convenient to discuss the latter of these first. Statman works in
the setting of the simply typed _$\lambda Y$ -calculus_, essentially the pure
$\lambda$-calculus extended with constants
$Y_{\sigma}:(\sigma\rightarrow\sigma)\rightarrow\sigma$ and reduction rules
$Y_{\sigma}M\rightsquigarrow M(Y_{\sigma}M)$. He gives a succinct proof that
$Y_{k+1}$ is not definable from $Y_{k}$ up to computational equality, based on
the following idea. If $Y_{k+1}$ were definable from $Y_{k}$, it would follow
that the recursion equation $Y_{k+1}g=g(Y_{k+1}g)$ could be derived with only
finitely many uses of the equation $Y_{k}M=M(Y_{k}M)$ (say $m$ of them). It
would then follow, roughly speaking, that $mn$ recursion unfoldings for
$Y_{k}$ would suffice to fuel $n$ recursion unfoldings for $Y_{k+1}$. On the
other hand, it can be shown that the size of normal-form terms definable using
$n$ unfoldings of $Y_{k+1}$ (as a function of the size of the starting term)
grows faster than can be accounted for with $mn$ unfoldings of $Y_{k}$.

The language $\lambda Y$ is seemingly less powerful than
${\mathrm{PCF}}$,101010One might consider translating ${\mathrm{PCF}}$ into
$\lambda Y$ by representing natural numbers as Church numerals; however, it
appears that predecessor is not $\lambda Y$-definable for this representation.
although this is perhaps not the most essential difference between Statman’s
work and ours. More fundamentally, Statman’s method establishes the non-
definability only up to computational equality (that is, the equivalence
relation generated by the reduction rules), whereas we have been concerned
with non-definability modulo observational (or extensional) equivalence. Even
for non-denotability in ${\mathsf{SP}}^{0}$, an approach along Statman’s lines
would be unlikely to yield much information, since there is no reason why the
number of unfoldings of $Y_{k}$ required to generate the NSP for $Y_{k+1}$ to
depth $n$ should not grow dramatically as a function of $n$.

A result very similar to Statman’s was obtained earlier in Damm [6], but by a
much more indirect route as part of a far-reaching investigation of the theory
of tree languages. In Damm’s setting, programs are _recursion schemes_
—essentially, families of simultaneous (and possibly mutually recursive)
defining equations in typed $\lambda$-calculus—but in essence these can be
considered as terms of $\lambda Y$ relative to some signature consisting of
typed constants. (Actually, Damm’s $\lambda$-terms involve a restriction to
_derived types_ , which has the effect of limiting attention to what are
elsewhere called _safe_ recursion schemes.) Any such program can be expanded
to an infinite tree (essentially a kind of Böhm tree), and Damm’s result
(Theorem 9.8 of [6]) is that if programs are considered up to _tree equality_
, then safe level $k+1$ recursions give more expressive power than safe level
$k$ ones. Damm’s result is thus distinguished from Statman’s in two ways: by
the restriction to safe recursion schemes, and by the use of tree equality in
place of the stricter computational equality. This latter point brings Damm’s
work somewhat closer in spirit to our work: indeed, in the case of pure
$\lambda Y$, tree equality agrees with equality of innocent strategies if the
base type is interpreted as a certain trivial game—or equivalently with
equality in a variant of our ${\mathsf{SP}}^{0}$ with no ground type values.
However, in the case of a signature for ${\mathrm{PCF}}$, tree equality will
still be considerably more fine-grained than equality in ${\mathsf{SP}}^{0}$,
let alone in ${\mathsf{SF}}$, since in effect the ${\mathrm{PCF}}$ constants
are left uninterpreted. It therefore seems unlikely that an approach to our
theorems via Damm’s methods is viable.

The strictness of the recursion scheme hierarchy was further investigated by
Ong [22], who used innocent game semantics to show that the complexity of
certain model checking problems for trees generated by level $k$ recursions
increases strictly with $k$. It was also shown by Hague, Murawski, Ong and
Serre [7] that the trees generated by level $k$ recursion schemes (with no
safety restriction) were precisely those that could be generated by
_collapsible pushdown automata_ of order $k$. Later, Kartzow and Parys [10]
used pumping lemma techniques to show that the collapsible pushdown hierarchy
was strict, hence so was the recursion scheme hierarchy with no safety
restriction. Again, despite the intriguing parallels to our work, these
results appear to be manifesting something quite different: in our setting,
the power of level $k$ recursion has nothing to do with the ‘difficulty of
computing’ the relevant NSPs in the sense of automata theory, since the full
power of Turing machines is required even at level 1.

Also of interest is the work of Jones [9] from the functional programming
community. Jones’s motivation is close to ours in that he seeks to give
mathematical substance to the programming intuition that some (combinations
of) language features yield ‘more expressive power’ than others. As Jones
notes, an obvious obstacle to obtaining such results is that all programming
languages of practical interest are Turing complete, so that no such
expressivity distinctions are visible at the level of the (first-order)
computable functions. Whereas we have responded to this by considering the
situation at higher types, where genuine expressivity differences do manifest
themselves, Jones investigates the power of (for example) recursion at
different type levels in the context of a restricted language of ‘read-only’
or ‘cons-free’ programs. Amongst other results, he shows that in such a
language, if data values and general recursion of type level $k\geq 1$ are
admitted, then the computable functions from lists of booleans to booleans are
exactly the expktime computable ones. These results inhabit a mathematical
territory very different from ours, although yet again, the basic moral that
the power of recursion increases strictly with its type level shines through.

###  7.2 Relationship to game semantics

Next, we comment briefly how our work relates to the known _game models_ of
PCF [1, 8]. It is known that these models are in fact isomorphic to our
${\mathsf{SP}}^{0}$, although the equivalence between the game-theoretic
definition of application and our own is mathematically non-trivial (see [17,
Section 7.4]). This raises the obvious question of whether our proofs could be
conducted equally well, or better, in a game-semantical setting.

Whilst a direct translation is presumably possible, our present impression is
that the sequential procedure presentation, and our calculus of meta-terms in
particular, allows one to see the wood for the trees more clearly, and also to
draw more easily on familiar intuitions from $\lambda$-calculus. However, a
closer look at game-semantical approaches would be needed in order to judge
whether either approach really offers some genuine mathematical or conceptual
advantage over the other.

###  7.3 Sublanguages of ${\mathrm{PCF}}$: further questions

We now turn our attention to some potential extensions and generalizations of
our work.

So far, we have worked mainly with a coarse stratification of types in terms
of their levels, although we have illustrated in Section 6 how finer
stratifications are also possible. Naturally, there is scope for a still more
fine-grained analysis of types and the relative strength of their
$Y$-combinators; this is of course closely related to the task of mapping out
the embeddability relation between types (as in Subsection 2.4) in finer
detail.

Even at level 1, there is some interest here. Our analysis in Section 6 has
shown that, for $l\geq 1$,

  * •

the element
$Y_{{\mathtt{N}}^{l+1}\rightarrow{\mathtt{N}}}\in{\mathsf{SP}}^{0}$ is not
${\mathrm{PCF}}^{\Omega}_{0}$-definable from
$Y_{{\mathtt{N}}^{l}\rightarrow{\mathtt{N}}}$,

  * •

the element $Y_{{\mathtt{N}}^{l+2}\rightarrow{\mathtt{N}}}\in{\mathsf{SF}}$ is
not ${\mathrm{PCF}}^{\Omega}_{0}$-definable from
$Y_{{\mathtt{N}}^{l}\rightarrow{\mathtt{N}}}$.

However, this leaves us with a small gap for ${\mathsf{SF}}$: e.g. we have not
shown either that $Y_{{\mathtt{N}}\rightarrow{\mathtt{N}}}$ is strictly weaker
than $Y_{{\mathtt{N}}^{2}\rightarrow{\mathtt{N}}}$ or that
$Y_{{\mathtt{N}}^{2}\rightarrow{\mathtt{N}}}$ is strictly weaker than
$Y_{{\mathtt{N}}^{3}\rightarrow{\mathtt{N}}}$, although according to classical
logic, at least one of these must be the case. (This is reminiscent of some
well-known situations from complexity theory.) We expect that a more delicate
analysis will allow us to fill this gap. One can also envisage an even more
fine-grained hierarchy obtained by admitting other base types such as the
booleans or unit type.

A closely related task is to obtain analogous results for the _call-by-value_
interpretation of the simple types (as embodied in Standard ML, for example).
As is shown in [17, Section 4.3], a call-by-value (partial) type structure
${\mathsf{SF}}_{v}$ can be constructed by fairly general means from
${\mathsf{SF}}$: here, for example, ${\mathsf{SF}}_{v}(\overline{1})$ consists
of all partial functions $\mathbb{N}\rightharpoonup\mathbb{N}$ rather than
(monotone) total functions $\mathbb{N}_{\bot}\rightarrow\mathbb{N}_{\bot}$,
and ${\mathsf{SF}}_{v}(\overline{2})$ consists of partial functions
$\mathbb{N}_{\bot}^{\mathbb{N}}\rightharpoonup\mathbb{N}$. From known results
on the interencodability of call-by-name and call-by-value models (see [17,
Section 7.2]), it is easy to read off the analogue of Corollary 3 for
${\mathsf{SF}}_{v}^{\mbox{\scriptsize\rm eff}}$; however, more specific
results on the relative strengths of various $Y$-combinators within
${\mathsf{SF}}_{v}$ would require some further reworking of our arguments.

Of course, one can also pose relative definability questions for other
elements besides $Y$-combinators. For instance, it is natural to consider the
_higher-order primitive recursors_ ${\mathit{rec}}_{\sigma}$ of System T, as
well as the closely related _iterators_ ${\mathit{iter}}_{\sigma\tau}$:

$\displaystyle{\mathit{rec}}_{\sigma}$ $\displaystyle:$
$\displaystyle\sigma\rightarrow(\sigma\rightarrow{\mathtt{N}}\rightarrow\sigma)\rightarrow{\mathtt{N}}\rightarrow\sigma\;,$
$\displaystyle{\mathit{iter}}_{\sigma\tau}$ $\displaystyle:$
$\displaystyle(\sigma\rightarrow(\sigma+\tau))\rightarrow\sigma\rightarrow\tau\;.$

The idea behind the latter is to embody the behaviour of a _while_ construct
for imperative-style loops with state $\sigma$ and exit type $\tau$.111111The
sum type $\sigma+\tau$ is not officially part of our system, but can (for any
given $\sigma,\tau$) be represented as a retract of some existing simple type.

It is shown in [17, Section 6.3] that each ${\mathit{rec}}_{\sigma}$ may be
interpreted by a _left-well-founded_ procedure (cf. Subsection 2.5), and it is
not hard to check that the same is true for each
${\mathit{iter}}_{\sigma\tau}$. Furthermore, it is clear that all left-well-
founded procedures are non-spinal, so it requires only the addition of an easy
base case in the proof of Theorem 28 to show that $Y_{k+1}$ cannot be defined
even in ${\mathrm{PCF}}_{k}^{\Omega}$ extended with all primitive recursors
and iterators. (Actually, we can dispense with the primitive recursors here,
as it is straightforward to define them from suitable iterators.)

The dual question, roughly speaking, is whether any or all of the recursors
${\mathit{rec}}_{\sigma}$ or iterators ${\mathit{iter}}_{\sigma{\mathtt{N}}}$
for types $\sigma$ of level $k+1$ are definable in ${\mathrm{PCF}}_{k}$. We
conjecture that they are not, and that this could be shown by suitably
choosing a substructure of ${\mathsf{SP}}^{0}$ so as to exclude such
${\mathit{iter}}_{\sigma{\mathtt{N}}}$. (This would incidentally answer
Question 2 of [4, Section 5].) One could also look for substructures that more
precisely determine the strength of various _bar recursion_ operators or the
_fan functional_. All in all, our experience leads us to expect that many
further substructures of ${\mathsf{SP}}^{0}$ should be forthcoming, leading to
a harvest of non-definability results exhibiting a rich ‘degree structure’
among ${\mathrm{PCF}}$-computable functionals.

Another very natural kind of question is the following: given a particular
sublanguage ${\mathcal{L}}$ of ${\mathrm{PCF}}$, what is the _simplest_
possible type for an element of ${\mathsf{SF}}^{\mbox{\scriptsize\rm eff}}$
that is not denotable in ${\mathcal{L}}$? Or to look at it another way: given
a type $\sigma$, what is the smallest natural sublanguage of ${\mathrm{PCF}}$
that suffices for defining all elements of
${\mathsf{SF}}^{\mbox{\scriptsize\rm eff}}(\sigma)$? Here the analysis of [17,
Section 7.1] yields several positive definability results, whilst the analysis
of the present paper provides ammunition on the negative side. The current
state of our knowledge is broadly as follows. As in [17], we write
${{\mathsf{Klex}}^{\mbox{\scriptsize\rm min}}}$ of the language of _Kleene
$\mu$-recursion_: this is equivalent (in its power to denote elements of
${\mathsf{SF}}$) to ${\mathrm{PCF}}_{0}$ extended with a strict primitive
recursor for ground type and a strict iterator for ground type, but with no
form of general recursion.

  * •

For first-order types $\sigma$, even ${{\mathsf{Klex}}^{\mbox{\scriptsize\rm
min}}}$ suffices for defining all elements of
${\mathsf{SF}}^{\mbox{\scriptsize\rm eff}}(\sigma)$; likewise, the oracle
version ${{\mathsf{Klex}}^{\mbox{\scriptsize\rm min}}}^{\Omega}$ suffices for
${\mathsf{SF}}(\sigma)$.

  * •

For second-order types $\sigma$ of the special form
$({\mathtt{N}}\rightarrow{\mathtt{N}})^{r}\rightarrow{\mathtt{N}}$,
${{\mathsf{Klex}}^{\mbox{\scriptsize\rm min}}}^{\Omega}$ still suffices for
${\mathsf{SF}}(\sigma)$; however, this result is non-constructive, and
${{\mathsf{Klex}}^{\mbox{\scriptsize\rm min}}}$ does not suffice for
${\mathsf{SF}}^{\mbox{\scriptsize\rm eff}}(\sigma)$. (We draw here on some
recent work of Dag Normann [20].)

  * •

For general second-order types, ${{\mathsf{Klex}}^{\mbox{\scriptsize\rm
min}}}^{\Omega}$ no longer suffices, but the languages ${\mathrm{PCF}}_{1}$,
${\mathrm{PCF}}_{1}^{\Omega}$ suffice for ${\mathsf{SF}}^{\mbox{\scriptsize\rm
eff}}$, ${\mathsf{SF}}$ respectively—indeed, even the single recursion
operator $Y_{{\mathtt{N}}\rightarrow{\mathtt{N}}}$ is enough here.

  * •

For third-order types, we do not know whether ${\mathrm{PCF}}_{1}$ suffices
(for ${\mathsf{SF}}^{\mbox{\scriptsize\rm eff}}$). We do know that
${\mathrm{PCF}}_{2}$ suffices, and that
$Y_{{\mathtt{N}}\rightarrow{\mathtt{N}}}$ alone is not enough.

  * •

For types of level $k\geq 4$, ${\mathrm{PCF}}_{k-3}$ does not suffice, but
${\mathrm{PCF}}_{k-2}$ does.

Again, there is scope for a more fine-grained view of the hierarchy of types.

###  7.4 Other languages and models

We have so far concentrated almost entirely on ${\mathrm{PCF}}$-style
sequential computation. To conclude, we briefly consider which other notions
of higher-order computation are likely to present us with an analogous
situation.

As already noted at the end of Subsection 2.4, several extensions of
${\mathrm{PCF}}$ studied in the literature present a strikingly different
picture: in these settings, universal types exist quite low down, and as a
consequence, only $Y$-combinators of low type (along with the other constants
of the language) are required for full definability. There is, however, one
important language which appears to be more analogous to pure ${\mathrm{PCF}}$
in these respects, namely an extension with _local state_ (essentially
Reynolds’s _Idealized Algol_). This language was studied in [2], where a fully
abstract game model was provided (consisting of well-bracketed but possibly
non-innocent strategies). Unpublished work by Jim Laird has shown that there
is no universal type in this setting. We would conjecture also that the
recursion hierarchy for this language is strict, where we consider
expressibility modulo observational equivalence in Idealized Algol. This would
constitute an interesting variation on our present results.

Related questions also arise in connection with _total_ functionals. Consider,
for example, the type structure ${\mathsf{Ct}}$ of total continuous
functionals, standardly constructed as the extensional collapse (relative to
$\mathbb{N}$) of the Scott model ${\mathsf{PC}}$ of partial continuous
functionals. It is shown by Normann [19] that every effective element of
${\mathsf{Ct}}$ is represented by a _${\mathrm{PCF}}$ -denotable_ element of
${\mathsf{PC}}$, and the proof actually shows that ${\mathrm{PCF}}_{1}$
suffices here. (The further generalization of these ideas by Longley [15]
makes some use of second-order recursions as in ${\mathrm{PCF}}_{2}$; we do
not know whether these can be eliminated.) Thus, in this setting, only
recursions of low type are needed to obtain all computable functionals.
Similar remarks apply to the total type structure ${\mathsf{HEO}}$, obtained
as the extensional collapse of ${\mathsf{PC}}^{\mbox{\scriptsize\rm eff}}$.

On the other hand, one may consider the _Kleene computable_ functionals over
${\mathsf{Ct}}$, or over the full set-theoretic type structure ${\mathsf{S}}$,
as defined by the schemes S1–S9. As explained in [17, Chapter 6], sequential
procedures can be seen as abstracting out the algorithmic content common to
both ${\mathrm{PCF}}$-style and Kleene-style computation (note that Kleene’s
S9 in some sense does duty for the $Y$-combinators of ${\mathrm{PCF}}$). This
naturally suggests that our strict hierarchy for ${\mathrm{PCF}}$ may have an
analogue for the Kleene computable functionals (say over ${\mathsf{S}}$ or
${\mathsf{Ct}}$), where at level $k$ we consider the evident restriction of S9
to types of level $\leq k$. We conjecture that this is indeed the case,
although the required counterexamples may be more difficult to find given that
we are limited to working with total functionals.

## Appendix A: Super-identity procedures

In the course of our proof, we have frequently encountered assertions of the
form $p\succeq x^{\eta}$ for various procedures $x^{k}\vdash p$. Although not
necessary for our main argument, it is natural to ask whether there are any
such procedures other than those for which $p\approx x^{\eta}$. The following
theorem shows that the answer is no: in other words, no procedure $\lambda
x.p:\overline{k}\rightarrow\overline{k}$ can extensionally ‘improve on’ the
identity function. We present this as a result of some interest in its own
right, whose proof is perhaps less trivial than one might expect.

Recall that $\preceq$ denotes the extensional order on ${\mathsf{SF}}$, as
well as the associated preorder on ${\mathsf{SP}}^{0}$. Within
${\mathsf{SF}}$, we will write $f\prec f^{\prime}$ to mean $f\preceq
f^{\prime}$ but $f\neq f^{\prime}$; we also write $f\sharp f^{\prime}$ to mean
that $f,f^{\prime}$ have no upper bound with respect to $\preceq$.

We call an element of ${\mathsf{SP}}^{0}$ _finite_ if it is a finite tree once
branches of the form $i\Rightarrow\bot$ have been deleted. We say an element
of ${\mathsf{SF}}$ is _finite_ if it is represented by some finite element of
${\mathsf{SP}}^{0}$. We write ${\mathsf{SP}}^{0,{\mbox{\scriptsize\rm
fin}}}(\sigma),{\mathsf{SF}}^{\mbox{\scriptsize\rm fin}}(\sigma)$ for the set
of finite elements in ${\mathsf{SP}}^{0}(\sigma),{\mathsf{SF}}(\sigma)$
respectively.

###### Theorem 45

(i) If $f\in{\mathsf{SF}}^{\mbox{\scriptsize\rm fin}}(k)$ and $f\prec
f^{\prime}$, then there exists $f^{\prime\prime}\sharp f^{\prime}$ with
$f\prec f^{\prime\prime}$.

(ii) If $\Phi\in{\mathsf{SF}}(k\rightarrow k)$ and $\Phi\succeq{\mathit{id}}$,
there can be no $f\in{\mathsf{SF}}(k)$ with $\Phi(f)\succ f$; hence
$\Phi={\mathit{id}}$.

Proof (i) The cases $k=0,1$ are easy, so let us assume $k\geq 2$. Suppose
$f\prec f^{\prime}$ where $f$ is finite. Then for some
$g\in{\mathsf{SF}}(k-1)$ we have $f(g)=\bot$ but
$f^{\prime}(g)=n\in\mathbb{N}$, say, and by continuity in ${\mathsf{SP}}^{0}$
we may take $g$ here to be finite. Take
$p,q\in{\mathsf{SP}}^{0,{\mbox{\scriptsize\rm fin}}}$ representing $f,g$
respectively; we may assume that $p,q$ are ‘pruned’ so that every subtree
containing no leaves $m\in\mathbb{N}$ must itself be $\bot$.

Case 1: $g(\bot^{k-2})=a\in\mathbb{N}$. In this case, we may suppose that
$q=\lambda x.a$. Consider the computation of $p\cdot q$. Since all calls to
$q$ trivially evaluate to $a$, this computation follows the rightward path
through $p$ consisting of branches $a\Rightarrow\cdots$. But since $p$ is
finite and $p\cdot q=\bot$ (because $f(g)=\bot$), this path must end in a leaf
occurrence of $\bot$ within $p$. Now extend $p$ to a procedure $p^{\prime}$ by
replacing this leaf occurrence by some $n^{\prime}\neq n$; then clearly
$p^{\prime}\cdot q=n^{\prime}$. Taking $f^{\prime\prime}$ to be the function
represented by $p^{\prime}$, we then have $f\preceq f^{\prime\prime}$ and
$f^{\prime\prime}(g)=n^{\prime}\,\sharp\,n=f^{\prime}(g)$, so
$f^{\prime\prime}\sharp f^{\prime}$ (whence also $f^{\prime\prime}\neq f$ so
$f\prec f^{\prime\prime}$).

Case 2: $g(\bot^{k-2})=\bot$. Take $N$ larger than $n$ and all numbers
appearing in $p,q$. Define $p^{\prime}\sqsupseteq p$ as follows: if $p=\lambda
x.\bot$, take $p^{\prime}=\lambda x.N$, otherwise obtain $p^{\prime}$ from $p$
by replacing each case branch $j\Rightarrow\bot$ anywhere within $p$ by
$j\Rightarrow N$ whenever $j\leq N$. Extend $q$ to $q^{\prime}$ in the same
way. Note in particular that every ${\mathtt{case}}$ subterm within
$p^{\prime},q^{\prime}$ will now be equipped with a branch $N\Rightarrow N$.

Now consider the computation of $p\cdot q$. Since $p,q$ are finite and
$f(g)=\bot$, this evaluates to an occurrence of $\bot$ which originates from
$p$ or $q$. Since no numbers $>N$ ever arise in the computation, this
occurrence of $\bot$ cannot be part of a branch $j\Rightarrow\bot$ for $j>N$,
so will have been replaced by $N$ in $p^{\prime}$ or $q^{\prime}$. Now suppose
that we head-reduce $pq$ until $\bot$ first appears in head position, and let
$U$ be the resulting meta-term. Then it is easy to see that
$p^{\prime}q^{\prime}$ correspondingly reduces to a meta-term $U^{\prime}$
with $N$ in head position. (Formally, we reason here by induction on the
length of head-reduction sequences not involving the rule for
${\mathtt{case}}\;\bot\;{\mathtt{of}}\;(\cdots)$.)

We now claim that $p^{\prime}\cdot q^{\prime}=N$. Informally, this is because
the head occurrence of $N$ in $U^{\prime}$ will be propagated to the top level
by the case branches $N\Rightarrow N$ within both $p^{\prime}$ and
$q^{\prime}$. More formally, let us define the set of meta-expressions _led by
$N$_ inductively as follows:

  * •

$N$ is led by $N$.

  * •

If $E$ is led by $N$, then so is
${\mathtt{case}}\;E\;{\mathtt{of}}\;(i\Rightarrow D_{i})$.

We say that an NSP meta-term $T$ is _saturated at $N$_ if every
${\mathtt{case}}$ subterm within $T$ has a branch $N\Rightarrow E$ where $E$
is led by $N$. Clearly $p^{\prime}q^{\prime}$ is saturated at $N$, and it is
easy to check that the terms saturated at $N$ are closed under head
reductions; thus $U^{\prime}$ is saturated at $N$. But we have also seen that
$U^{\prime}$ has $N$ in head position, so is led by $N$. Finally, an easy
induction on term size shows that every finite meta-term that is led by $N$
and saturated at $N$ evaluates to $N$ itself. This shows that $p^{\prime}\cdot
q^{\prime}=N$.

To conclude, let $f^{\prime\prime},g^{\prime}$ be the functions represented by
$p^{\prime},q^{\prime}$ respectively, so that $f\preceq f^{\prime\prime}$ and
$g\preceq g^{\prime}$. Then $f^{\prime}(g^{\prime})=n$, but
$p^{\prime\prime}\cdot q=N$ so $f^{\prime\prime}(g^{\prime})=N\neq n$, whence
$f^{\prime\prime}\sharp f^{\prime}$ (and also $f^{\prime\prime}\neq f$ so
$f\prec f^{\prime\prime}$).

(ii) Suppose $\Phi\succeq{\mathit{id}}$ and $\Phi(f)\succ f$ for some $f$.
Again by continuity, we may take $f$ to be finite. Then by (i), we may take
$f^{\prime\prime}\succ f$ such that $f^{\prime\prime}\,\sharp\,\Phi(f)$. But
this is impossible because $\Phi(f^{\prime\prime})\succeq f^{\prime\prime}$
and $\Phi(f^{\prime\prime})\succeq\Phi(f)$. Thus $\Phi={\mathit{id}}$. $\Box$

It is easy to see that the above theorem holds with any finite type over
${\mathtt{N}}$ in place of $\overline{k}$. However, it will trivially fail if
the unit type ${\mathtt{U}}$ is admitted as an additional base type: e.g. the
function $(\lambda
x.\top)\in{\mathsf{SF}}({\mathtt{U}}\rightarrow{\mathtt{U}})$ strictly
dominates the identity. An interesting question is whether the theorem holds
for all finite types over the type ${\mathtt{B}}$ of booleans: note that the
above proof fails here since it requires the base type to be infinite. For
comparison, we mention that in other models of computation, improvements on
the identity are sometimes possible for such types. For example, if
$\sigma={\mathtt{B}}\rightarrow{\mathtt{B}}$, then a functional of type
$\sigma\rightarrow\sigma$ strictly dominating the identity exists in the Scott
model. Indeed, such a function $J$ can be defined in ${\mathrm{PCF}}$
augmented with the parallel conditional ${\mathit{pif}}$, e.g. as

$J~{}=~{}\lambda f^{\sigma}.\lambda
x^{\mathtt{B}}.\,\mathit{vote}(f(x),f({\mathit{tt}}),f({\mathit{ff}}))\;.$

Here $\mathit{vote}$ is Sazonov’s voting function, definable by

$\mathit{vote}(x,y,z)~{}=~{}{\mathit{pif}}(x,{\mathit{pif}}(y,{\mathit{tt}},z),{\mathit{pif}}(y,z,{\mathit{ff}}))\;.$

The point is that $J$ will ‘improve’ the function $\lambda
x.\,{\mathit{if}}(x,{\mathit{tt}},{\mathit{tt}})$ to $\lambda
x.{\mathit{tt}}$. We do not know whether phenomena of this kind can arise
within the model ${\mathsf{SF}}$.

## References

  * [1] Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation 163(2), 409–470 (2000)
  * [2] Abramsky, S., McCusker, G.: Game semantics. In: Schwichtenberg, H., Berger, U. (eds.) Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School, pp. 1-56. Springer, Heidelberg (1999)
  * [3] Amadio, R., Curien, P.-L.: Domains and Lambda Calculi. Cambridge Tracts in Theoretical Computer Science 46, Cambridge University Press (1998)
  * [4] Berger, U.: Minimisation vs. recursion on the partial continuous functionals. In: Gärdenfors, P., Woleński, J., Kijania-Placek, K. (eds.) In the Scope of Logic, Methodology and Philosophy of Science: Volume One of the 11th International Congress of Logic, Methodology and Philosophy of Science, Cracow, August 1999, pp. 57-64. Kluwer, Dordrecht (2002)
  * [5] Cartwright, R., Felleisen, M.: Observable sequentiality and full abstraction. In: Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 328-342. ACM Press, New York (1992)
  * [6] Damm, W.: The IO- and OI-hierarchies. Theoretical Computer Science 20, 95-207 (1982)
  * [7] Hague, M., Murawski, A.S., Ong, C.-H.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: Proceedings of the 23th Annual IEEE Symposium on Logic in Computer Science, pp. 452-461. IEEE Computer Society (2008)
  * [8] Hyland, J.M.E., Ong, C.-H.L.: On full abstraction for PCF: I, II, and III. Information and Computation 163, 285–408 (2000)
  * [9] Jones, N.D.: The expressive power of higher-order types, or, life without CONS. Journal of Functional Programming 11, 5–94 (2001)
  * [10] Kartzow, A., Parys, P.: Strictness of the collapsible pushdown hierarchy. In: B. Rovan, V. Sassone and P. Widmayer (eds.), Mathematical Foundations of Computer Science 2012, pp. 566-577. Lecture Notes in Computer Science 7464, Springer (2012)
  * [11] Kleene, S.C.: Unimonotone functions of finite types (Recursive functionals and quantifiers of finite types revisited IV). In: A. Nerode and R.A. Shore (eds.), Proceedings of the AMS-ASL Summer Institute on Recursion Theory, pp. 119-138. American Mathematical Society, Providence (1985)
  * [12] Kristiansen, L.: Higher types, finite domains and resource-bounded Turing machines. Journal of Logic and Computation 22(2), 281–304 (2012)
  * [13] Loader, R.: Finitary PCF is not decidable. Theoretical Computer Science 266(1-2), 341–364 (2001)
  * [14] Longley, J.R.: The sequentially realizable functionals. Annals of Pure and Applied Logic 117(1), 1–93 (2002)
  * [15] Longley, J.R.: On the ubiquity of certain total type structures. Mathematical Structures in Computer Science 17(5), 841–953 (2007)
  * [16] Longley, J.R.: Bar recursion is not computable via iteration. Available from arxiv.org/abs/1804.07277; submitted for publication (2018). Earlier version as Informatics Research Report EDI-INF-RR-1420, University of Edinburgh (2015)
  * [17] Longley, J. and Normann, D.: Higher-Order Computability. Theory and Applications of Computability, Springer-Verlag (2015)
  * [18] Milner, R.: Fully abstract models of typed $\lambda$-calculi. Theoretical Computer Science 4(1), 1–22 (1977)
  * [19] Normann, D.: Computability over the partial continuous functionals. Journal of Symbolic Logic 65(3), 1133–1142 (2000)
  * [20] Normann, D.: The sequential functionals of type $(\iota\rightarrow\iota)^{n}\rightarrow\iota$ form a dcpo for all $n\in\mathbb{N}$. CoRR, abs/1607.02970 (2016)
  * [21] Normann, D., Sazonov, V.Yu.: The extensional ordering of the sequential functionals. Annals of Pure and Applied Logic 163(5) 575–603 (2012)
  * [22] Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, pp. 81-90. IEEE Computer Society (2006)
  * [23] Plotkin, G.D.: LCF considered as a programming language. Theoretical Computer Science 5(3), 223–255 (1977)
  * [24] Sazonov, V.Yu.: Expressibility in D. Scott’s LCF language. Algebra and Logic 15(3), 192–206 (1976)
  * [25] Sazonov, V.Yu.: An inductive definition and domain theoretic properties of fully abstract models of PCF and PCF+. Logical Methods in Computer Science 3(3), 50 pages (2007)
  * [26] Scott, D.S.: A type-theoretical alternative to ISWIM, CUCH, OWHY. In: A collection of contributions in honor of Corrado Böhm on the occasion of his 70th birthday. (Edited version of an unpublished note first circulated in 1969.) Theoretical Computer Science 121(1-2), 411–440 (1993).
  * [27] Statman, R.: On the $\lambda Y$ calculus. Annals of Pure and Applied Logic 130, 325–337 (2004).