Definability and Full Abstraction for PCF

Proof. $(\Rightarrow )$ is immediate: the applications are particular contexts.

$(\Leftarrow )$ Assume the right-hand condition and let $C[]$ be a context with $C[M]\Downarrow \underset{―}{n}$. Argue by induction on the length of the evaluation. PCF evaluation is deterministic and proceeds by decomposing the term into an evaluation context and a redex (lemma 154.3 applies verbatim to the recursion-free redexes and to $\mathsf{fix}$). If the hole is not in the redex position, the same decomposition applies to $C[N]$ and the induction hypothesis finishes. If the hole is in redex position, then the occurrence of $M$ is applied to some closed arguments $P_1,\dots ,P_j$ and the whole is in an evaluation context, so the computation reaches $M[\gamma ]P_1\cdots P_j$ and this converges; the assumed condition supplies the same convergence for $N$, and the induction hypothesis applies to the remainder of the evaluation. Note that the arguments are closed because the surrounding context binds every variable of $\mathrm{\Gamma }$ at the moment the redex is reached. ◻

Proof. The interpretation is functorial (theorem 157.11) and monotone in each argument for inclusion (lemma 157.18), so $[[C[M]]]\subseteq [[C[N]]]$ for every context. If $C[M]\Downarrow \underset{―}{n}$ then $qn\in [[C[M]]]$ by proposition 157.20, hence $qn\in [[C[N]]]$, hence $C[N]\Downarrow \underset{―}{n}$ by theorem 157.21. ◻

Proof. Congruence for composition: if $\rho {\lesssim }_{\mathrm{int}}{\rho }^{\prime }$ and $\beta$ is a strategy, then for every test $\alpha$ the composite $\alpha \circ \beta$ is again a test, so $\beta \circ \rho {\lesssim }_{\mathrm{int}}\beta \circ {\rho }^{\prime }$; and precomposition is handled by the same argument with $\alpha \circ (-\circ \gamma )$. Pairing and currying are congruences because by proposition 157.16 currying is the identity on sets of plays, and by proposition 157.15 a test on a product factors through one summand. The cartesian closed structure descends because its equations hold already in ${\mathcal{G}}_{\mathrm{i}}$. ◻

Proof. An innocent strategy is determined by its view function (definition 157.12), and every finite subset of a view function that is closed under even-length prefixes of views generates an innocent strategy contained in it; these form a directed family with union the whole. Finiteness in the dcppo: if $\rho$ is compact and $\rho \subseteq \bigcup _i{\rho }_i$ with the family directed, each of the finitely many views of $\rho$ lies in some ${\rho }_i$, and directedness gives a single one. Conversely a finite element is contained in the union of its compact approximations, hence equals one of them. ◻

Proof. The initial move of an arrow arena is initial in the result arena by definition 157.3, so it is $q$. A $P$-move after $q$ must be enabled by a move in the current $P$-view, which is $q$ alone; the moves enabled by $q$ are the answers of $\gamma$ and the initial moves of the $[[{\sigma }_i]]$, again by definition 157.3. In case (1) well-bracketing closes the only pending question, so no further move is legal and the view function is as displayed. ◻

Proof. After $q$ and the initial question of $[[{\sigma }_i]]$, the legal $O$-moves are the initial questions of the $[[{\tau }_j]]$ — the argument asking for its $j$th input — and the answers $c$ of $\delta$. Innocence means $\rho$ is determined by its behaviour on each of these branches separately. Define ${\rho }_j$ to be the strategy whose view function consists of the views of ${\mathrm{f}}_{\rho }$ beginning with $q$, the question of $[[{\sigma }_i]]$, and the initial question of $[[{\tau }_j]]$, with that three-move prefix replaced by the initial question of ${\tau }_j$; and ${\rho }_c$ similarly for the branch after the answer $c$, with the prefix replaced by $q$. Each is innocent by construction, well-bracketed because the deleted prefix opens and closes nothing, and compact because ${\mathrm{f}}_{\rho }$ is finite. Each has strictly fewer views than $\rho$, since the view $q$ followed by the question of $[[{\sigma }_i]]$ belongs to ${\mathrm{f}}_{\rho }$ and to none of them. The displayed equation is the statement that $\rho$’s behaviour on every play is recovered by dispatching on the branch, which is exactly innocence together with the case analysis of the legal $O$-moves. ◻

Proof. Induction on the size of ${\mathrm{f}}_{\rho }$, with lemma 158.9 and lemma 158.10 as the case analysis. Write $\sigma ={\sigma }_1\to \cdots \to {\sigma }_k\to \gamma$ and, using proposition 157.16, regard $\rho$ as a morphism out of $[[\mathrm{\Gamma }]]\times [[{\sigma }_1]]\times \cdots \times [[{\sigma }_k]]$.

If ${\mathrm{f}}_{\rho }=\mathrm{\varnothing }$, take $M:=\lambda \overrightarrow{x}.{\mathrm{\Omega }}_{\gamma }$; its strategy is $\mathrm{\varnothing }$ by definition 157.19. If $\rho$ answers immediately with $c$, take $M:=\lambda \overrightarrow{x}.c$. Otherwise lemma 158.10 supplies the smaller strategies; by the induction hypothesis they are $[[M_j]]$ and $[[M_c]]$ for terms in the extended context, and $$M:=\lambda \overrightarrow{x}.\mathsf{case}(x_i{M}_1\cdots M_m)\mathsf{of}(c\mapsto M_c)$$ has $[[M]]=\rho$, since the interpretation of $\mathsf{case}$ and of application are exactly the dispatch and the question in lemma 158.10, and the interpretation is functorial. Two points require care and are the only ones where the argument is delicate. First, the case analysis over answers $c$ of $\delta$ is infinite when $\delta =\iota$; compactness makes all but finitely many branches equal to $\mathrm{\varnothing }$, and the finitely many exceptions are enumerated by a nest of $\mathsf{if}$-tests on equality with a numeral, definable in PCF. Second, the pointer structure must be respected: the term above reconstructs the pointer of each $O$-move as the occurrence of $x_i$ that asked, which is correct because a compact innocent strategy’s views determine the justifiers uniquely (lemma 157.5). ◻

Proof. $(\Leftarrow )$ Let $C[]$ be a context with $C[M]\Downarrow \underset{―}{n}$. The interpretation of a context is a strategy $\alpha$ with $[[C[M]]]=\alpha \circ [[M]]$, by functoriality (theorem 157.11). By proposition 157.20 and theorem 157.21, $qn\in \alpha \circ [[M]]$; the hypothesis gives $qn\in \alpha \circ [[N]]$; and adequacy again gives $C[N]\Downarrow \underset{―}{n}$.

$(\Rightarrow )$ Let $\alpha :[[\sigma ]]\Rightarrow \iota$ and suppose $qn\in \alpha \circ [[M]]$. A single interaction sequence witnesses this, and it is finite, so by lemma 158.7 there are compact ${\alpha }_0\subseteq \alpha$ and a compact ${\rho }_0\subseteq [[M]]$ with $qn\in {\alpha }_0\circ {\rho }_0$. By theorem 158.11 there is a term $x:\sigma ⊢A:\iota$ with $[[A]]={\alpha }_0$. Take the context $C[]:=A[/x]$, closing $\mathrm{\Gamma }$ by any closed terms. Then $qn\in [[C[M]]]$ because ${\alpha }_0\circ {\rho }_0\subseteq [[C[M]]]$ and inclusion is monotone, so $C[M]\Downarrow \underset{―}{n}$ by theorem 157.21. The hypothesis $M\lesssim N$ gives $C[N]\Downarrow \underset{―}{n}$, hence $qn\in {\alpha }_0\circ [[N]]$ by soundness, hence $qn\in \alpha \circ [[N]]$ by monotonicity. As $\alpha$ and $n$ were arbitrary, this is $[[M]]{\lesssim }_{\mathrm{int}}[[N]]$. ◻

Proof. Apply theorem 158.13 in both directions; the reformulation is the definition of the quotient. ◻

Proof. Both terms diverge in every context, since every application of either to any argument reduces to ${\mathrm{\Omega }}_{\iota }$; hence $T_1\approx T_2$ by lemma 158.2. Their strategies differ because $[[T_2]]$ contains the play in which the argument’s initial question is asked — the interpretation of $f{\mathrm{\Omega }}_{\iota }$ asks $f$ before diverging — and $[[T_1]]$ has empty view function beyond the initial question. ◻