Games, Full Abstraction and Full Completeness

First published Thu Jan 12, 2017; substantive revision Tue Feb 2, 2021

Computer programs are particular kinds of texts. It is thereforenatural to ask what is the meaning of a program or, more generally,how can we set up a formal semantical account of a programminglanguage.

There are many possible answers to such questions, each motivated bysome particular aspect of programs. So, for instance, the fact thatprograms are to be executed on some kind of computing machine givesrise to operational semantics, whereas the similarities of programminglanguages with the formal languages of mathematical logic havemotivated the denotational approach that interprets programs and theirconstituents by means of set-theoretical models.

Each of these accounts induces its own synonymy relation on thephrases of the programming language: in a nutshell, the fullabstraction property states that the denotational and operationalapproaches define the same relation. This is a benchmark property fora semantical account of a programming language, and its failure for anintuitive denotational account of a simple language based onlambda-calculus has led eventually to refinements of the technicaltools of denotational semantics culminating in game semantics, partlyinspired by the dialogue games originally used in the semantics ofintuitionistic logic by Lorenzen and his school, and later extended byBlass and others to the interpretation of Girard’s linear logic.This bridge between constructive logic and programming has alsosuggested stronger forms of relation between semantics andproof-theory, of which the notion of full completeness is perhaps themost remarkable instance.

1. Introduction

1.1 Interpretations of programming languages

The notion of full abstraction arises from the Scott-Strachey approachto the semantical analysis of programming languages (Scott &Strachey 1971; Strachey 1966, 1967), also known asdenotational semantics. One fundamental aim of a denotationalsemantics of a programming language ${L}$ is to give acompositional interpretation ${\mathcal{M}}: {L}\to D$ oftheprogram phrases of ${L}$ as elements of abstractmathematical structures (domains) $D$.

We may choose another way of giving meaning to programs, based ontheir execution. Thisoperational interpretation is onlydefined on the setProg of programs of${L}$, and involves the definition of a suitable set of programvalues, which are theobservables of ${L}$. If theexecution of program $e$ terminates with value $v$, a situationexpressed by the notation $e \opDownarrow v$, then $v$ is theoperational meaning of $e$. This defines the operationalinterpretation of programs as a partial function ${\mathcal{O}}$from programs to values, where ${\mathcal{O}}(e) = v$ when $e\opDownarrow v$.

Both interpretations induce natural equivalence relations on programphrases. In one of its formulations, full abstraction states thecoincidence of the denotational equivalence on a language with oneinduced by the operational semantics. Full abstraction has been firstdefined in a paper by Robin Milner (1975), which also exposes theessential conceptual ingredients of denotational semantics:compositionality, and the relations between observational anddenotational equivalence of programs. For this reason, fullabstraction can be taken as a vantage point into the vast landscape ofprogramming language semantics, and is therefore quite relevant to thecore problems of the philosophy of programming languages (White 2004)and of computer science (Turner 2016).

1.2 Compositionality

Compositionality (Szabó 2013) is a desirable feature of asemantical analysis of a programming language, because it allows oneto calculate the meaning of a program as a function of the meanings ofits constituents. Actually, in Milner’s account (see especially1975: sec. 1, 4), compositionality applies even more generally tocomputing agents assembled from smaller ones by means ofappropriate composition operations. These agents may include, besideprograms, hardware systems like a computer composed of a memory,composed in turn of two memory registers, and a processing unit, whereall components are computing agents. This allows one to include in oneframework systems composed of hardware, of software and even of both.Now, the syntactic rules that define inductively the variouscategories of phrases of a programming language allow us to regard${L}$ as analgebra of program phrases, whose signature isdetermined by these rules. One account of compositionality that isespecially suitable to the present setting (Szabó 2013: sec. 2)identifies a compositional interpretation of programs with ahomomorphism from this algebra to the domain of denotationsassociating with every operation of the algebra of programs acorresponding semantical operation on denotations.

As an example, consider a simple imperative language whose programs$\mathtt{c}$ denote state transformations${\mathcal{M}}(\mathtt{c}) : \Sigma \to \Sigma$. Among theoperations on programs of this language there issequentialcomposition, building a program $\mathtt{c}_1 ; \mathtt{c}_2$from programs $\mathtt{c}_1$ and $\mathtt{c}_2$. The intendedoperational meaning of this program is that, if $\mathtt{c}_1 ;\mathtt{c}_2$ is executed starting from a state $\sigma \in\Sigma$, we first execute $\mathtt{c}_1$ starting form state$\sigma$. If the execution terminates we obtain a state $\sigma'$,from which we start the execution of $\mathtt{c}_2$ reaching, if theexecution terminates, a state $\sigma''$. The latter state is thestate reached by the execution of $\mathtt{c}_1 ; \mathtt{c}_2$ fromstate $\sigma$. From a denotational point of view, we have theoperation of composition on functions $\Sigma \to \Sigma$, and thecompositional interpretation of our program is given by the followingidentity, to be read as a clause of a definition of ${\mathcal{M}}$by induction on the structure of programs: \[{\mathcal{M}}(\mathtt{c}_1 ; \mathtt{c}_2) = {\mathcal{M}}(\mathtt{c}_2) \circ {\mathcal{M}}(\mathtt{c}_1)\] or, moreexplicitly, for any state $\sigma$: \[{\mathcal{M}}(\mathtt{c}_1 ; \mathtt{c}_2) (\sigma) = {\mathcal{M}}(\mathtt{c}_2) ({\mathcal{M}}(\mathtt{c}_1) (\sigma)).\] As most programminglanguages have several categories of phrases (for instanceexpressions, declarations, instructions) the algebras of programs willgenerally be multi-sorted, with one sort for each category of phrase.Denotational semantics pursues systematically the idea of associatingcompositionally to each program phrase a denotation of the matchingsort (see Stoy 1977 for an early account).

1.3 Program equivalence and full abstraction

The existence of an interpretation of a programming language ${L}$induces in a standard way anequivalence of programphrases:

Definition 1.1 (Denotational equivalence). Given anytwo program phrases $e,e'$, they aredenotationallyequivalent, written $e \simeq_{\mathcal{M}}e'$, when${\mathcal{M}}(e) = {\mathcal{M}}(e')$.

If ${\mathcal{M}}$ is compositional, then ${\simeq_{\mathcal{M}}}$is a congruence over the algebra of programs, whose derivedoperations, those obtained by composition of operations of thesignature, are calledcontexts. A context $C\blbr$represents a program phrase with a “hole” that can befilled by program phrases $e$ of appropriate type to yield theprogram phrase $C[e]$. By means of contexts we can characterizeeasily the compositionality of a semantic mapping:

Proposition 1.1. If ${\mathcal{M}}$ iscompositional, then for all phrases $e,e'$ and all contexts$C\blbr$: \[\tag{1}\label{compositionality}{e \simeq_{\mathcal{M}} e'} \Rightarrow {C[e] \simeq_{\mathcal{M}} C[e']}.\]

This formulation highlights another valuable aspect ofcompositionality, namely thereferentially transparency ofall contexts, equivalently theirextensionality:denotationally equivalent phrases can be substituted in any contextleaving unchanged the denotation of the resulting phrase. Theimplication ($\ref{compositionality}$) states, in particular, that${\simeq_{\mathcal{M}}}$ is a congruence. In order to comparedenotational and operational congruence, therefore, we must carve acongruence out of the naive operational equivalence defined by setting$e \sim e'$ if and only if ${\mathcal{O}}(e) = {\mathcal{O}}(e')$.This can be done by exploitingprogram contexts $C\blbr$,representing a program with a “hole” that can be filled byprogram phrases $e$ of suitable type to yield a complete program$C[e]$.

Definition 1.2 (Observational equivalence) Given anytwo program phrases $e,e'$, they areobservationalequivalent, written $e \simeq_{\mathcal{O}}e'$, when, for allprogram contexts $C\blbr$ and all program values $v$: \[C[e] \opDownarrow v\ \text{ if and only if }\ C[e'] \opDownarrow v.\]

Observational equivalence is then a congruence over the algebra ofprogram phrases, and in fact it is the largest congruence contained in$\sim$. From the general point of view of the account of Milner(1975), that we are following closely, the context of a computingagent represents one of its possible environments. If we adopt theprinciple that “the overt behavior constitutes thewhole meaning of a computing agent” (Milner 1975: 160),then the contexts represents intuitively the observations that we canmake on the behavior of the computing agent. In the case of programs,the observables are the values, so observational equivalenceidentifies phrases that cannot be distinguished by means ofobservations whose outcomes are distinct values. One consequence ofMilner’s methodological principle is that a computing agentbecomes a

transducer, whose input sequence consists of enquiries by, orresponses from, its environment, and whose output sequence consists ofenquiries of, or responses to, its environment. (Milner 1975: 160)

A behavior of a computing agent takes then the form of adialogue between the agent and its environment, a metaphorthat will be at the heart of the game theoretic approaches tosemantics to be discussed inSection 3. This behavioral stance, which has its roots in the work of engineerson finite state devices has also been extended by Milner to amethodology of modeling concurrent systems, with the aim

to describe a concurrent system fully enough to determine exactly whatbehaviour will be seen or experienced by an external observer. Thusthe approach is thoroughly extensional; two systems areindistinguishable if we cannot tell them apart without pulling themapart. (Milner 1980: 2)

In addition, the roles of system and observer are symmetric, to suchan extent that

we would like to represent the observer as a machine, then torepresent the composite observer/machine as a machine, then tounderstand how this machine behaves for a new observer. (Milner 1980:19)

While observational equivalence is blind to the inner details of acomputing agent but only observes the possibleinteractionswith its environment in which it takes part, denotational equivalencetakes as given the internal structure of a computing agent and, in acompositional way, synthesizes its description from those of itsinternal parts. The notion of full abstraction is precisely intendedto capture the coincidence of these dual perspectives:

Definition 1.3 (Full abstraction). A denotationalsemantics ${\mathcal{M}}$ isfully abstract with respect toan operational semantics ${\mathcal{O}}$ if the induced equivalences${\simeq_{\mathcal{M}}}$ and ${\simeq_{\mathcal{O}}}$coincide.

As a tool for investigating program properties, full abstraction canbe seen as acompleteness property of denotational semantics:every equivalence of programs that can be proved operationally, canalso be proved by denotational means. Equivalently, a denotationalproof that two terms are not equivalent will be enough to show thatthey are not interchangeable in every program context.

Full abstraction also functions as a criterion for assessing atranslation $\vartheta$ from a language ${L}_1$ into a (notnecessarily different) language ${L}_2$, provided the two languageshave the same sets of observables, sayObs (Riecke 1993).Then $\vartheta$ isfully abstract if observationalequivalence (defined with respect toObs) of $e,e' \in{L}_1$ is equivalent to observational equivalence of$\vartheta(e),\vartheta(e')$ in ${L}_2$. The existence of fullyabstract translation between languages can be used to compare theirexpressive power, following a suggestion of (Mitchell 1993; Riecke1993): ${L}_1$ is no more expressive than ${L}_2$ if there is afully abstract translation of ${L}_1$ into ${L}_2$.

Before going on in this general introduction to full abstraction andrelated notions in the area of programming languages semantics, inorder to show the broad relevance of these notions, it is interestingto observe that there is a very general setting in which it ispossible to study the full abstraction property, suggested by recentinvestigations on compositionality in natural and artificial languagesby Hodges (2001) and others. In this setting, full abstraction isconnected to the problem of finding a compositional extension of asemantic interpretation of a subset $X$ of a language $Y$ to aninterpretation of the whole language, via Frege’sContextPrinciple (see Janssen 2001 on this), stating that the meaning ofan expression in $Y$ is the contribution it makes to the meaning ofthe expressions of $X$ that contain it. In the original formulationby Frege $X$ was the set of sentences and $Y$ the set of allexpressions, while in programming theory $X$ is the set of programs,$Y$ the set of all program phrases.

A weakening of the definition of full abstraction represents anessential adequacy requirement for a denotational interpretation of alanguage:

Definition 1.4 (Computational adequacy). Adenotational semantics ${\mathcal{M}}$ iscomputationallyadequate with respect to an operational semantics${\mathcal{O}}$ if, for all programs $e$ and all values $v$\[{\mathcal{O}}(e) = v \ \text{ if and only if } \ {\mathcal{M}}(e) = {\mathcal{M}}(v).\]

An equivalent formulation of computational adequacy allows tohighlight its relation to full abstraction:

Proposition 1.2. Assume that ${\mathcal{M}}$ is acompositional denotational interpretation such that ${\mathcal{O}}(e)= v$ implies ${\mathcal{M}}(e) = {\mathcal{M}}(v)$. The followingtwo statements are equivalent:

${\mathcal{M}}$ is computationally adequate with respect to${\mathcal{O}}$;
for any twoprograms $e,e' \in {\texttt{Prog}}$,\[e \simeq_{\mathcal{M}} e' \ \text{ if and only if } \ e \simeq_{\mathcal{O}} e'\]

While the definition of the full abstractionproperty isstraightforward, fully abstract models for very natural examples ofprogramming languages have proved elusive, giving rise to a fullabstractionproblem. In our discussion of full abstraction weshall mainly concentrate on the full abstraction problem for thelanguage PCF (Programming language for Computable Functions, Plotkin1977), a simply typed $\lambda$-calculus with arithmetic primitivesand a fixed-point combinator at all types proposed in Scott 1969b.This language is important because it includes most of the programmingfeatures semantic analysis has to cope with: higher-order functions,types and recursion, with reduction rules that provide an abstractsetting for experimenting with several evaluation strategies.Furthermore, PCF is also a model for other extensions of simply typed$\lambda$-calculus used for experimenting with programming features,like the Idealized Algol of Reynolds (1981). The efforts towards asolution of the full abstraction problem for PCF contributed, as aside effect, to the systematic development of a set of mathematicaltechniques for semantical analysis whose usefulness goes beyond theiroriginal applications. We shall describe some of them inSection 2, devoted to the semantic analysis of PCF based on partially orderedstructures, thedomains introduced by Dana Scott (1970), thatwe examine inSection 2.3. Technical developments in the theory of domains and also in the newresearch area focussed on Girard’slinear logic (Girard1987) have led togame semantics (Abramsky, Jagadeesan, &Malacaria 2000; Hyland & Ong 2000), which is now regarded as aviable alternative to standard denotational semantics based ondomains. It is to this approach that we shall dedicateSection 3 trying to provide enough details to orient the reader in an extensiveand still growing literature documenting the applications of games tothe interpretation of a wide spectrum of programming languagefeatures.

2. Sequential higher-order computation: the full abstraction problem for PCF

The full abstraction problem has proved especially hard for a versionof simply typed $\lambda$-calculus with arithmetic primitives calledPCF (Programming with Computable Functions) (Plotkin 1977), a toyprogramming language based on the Logic for Computable Functions ofScott (1969) and Milner (1973). In this section we introduce (aversion of) the language with its operational and denotationalsemantics, and outline how the full abstraction problem arises forthis language. The problem has been one of the major concerns of thetheoretical investigation of programming languages for about twodecades, from its original formulation in the landmark papers (Milner1977; Plotkin 1977) to the first solutions proposed in 1993 (Abramskyet al. 2000; Hyland & Ong 2000) using game semantics, for whichseeSection 3.

2.1 Syntax of PCF

PCF is a language based on simply typed $\lambda$-calculus extendedwith arithmetic and boolean primitives, and its type system is definedaccordingly:

Definition 2.1 (PCF types). The setTypesof types of PCF is defined inductivelyas follows

theground typesnum (forterms representing natural numbers),bool(for terms representing boolean values)are types,
if $\sigma, \tau$ are types, also $(\sigma \to \tau)$ is atype.

Parentheses will be omitted whenever possible, with the conventionthat they associate to the right, so that a type $\sigma_1 \to \cdots\sigma_n \to \tau$ is equivalent to $(\sigma_1 \to (\sigma_2 \to(\cdots (\sigma_n \to \tau)\cdots)))$

PCF terms are the terms of simply typed $\lambda$-calculus extendedwith the following arithmetic constants, of the indicated type:

a constant ${0}$ of type $\texttt{num}$, representing thenatural number 0;
a constant $\texttt{succ}$ of type $\texttt{num}\to\texttt{num}$ representing the successor function over naturalnumbers;
a constant $\texttt{pred}$ of type $\texttt{num}\to\texttt{num}$ representing the predecessor function over naturalnumbers;
constants $\texttt{tt}$ and $\texttt{ff}$ of type$\texttt{bool}$;
constants of type $\texttt{bool}\to \texttt{num}\to\texttt{num}\to \texttt{num}$ and $\texttt{bool}\to \texttt{bool}\to\texttt{bool}\to \texttt{bool}$ for conditionals of typenumand of typebool,respectively: these are both written as${\texttt{if }\cdot\texttt{ then }\cdot\texttt{ else }\cdot}$, andwe let context make clear what is the intended type of theresult;
a constant $\texttt{zero?}$ for the test for zero of type$\texttt{num}\to \texttt{bool}$;
a unary function symbol ${\mathtt{Y}(\cdot)}$ for the fixedpoint combinator, where ${\mathtt{Y}(e)}:\sigma$ for any $e:\sigma\to \sigma$.

Terms are built inductively according to rules that allow to inferjudgements of the form $B \vdash e : \sigma$, stating thatterm $e$ is of type $\sigma$ under the assumption that thevariables occurring free in $e$ are given unique types in abasis $B$ of the form \[{\{ x_1:\sigma_1,\ldots,x_k:\sigma_k \}}.\] The rule for buildingPCF-terms are therefore inference rules for such judgements. Inparticular there are rules for typed constants, for example in anybasis $B$ there is a judgement $B \vdash \texttt{zero?} :\texttt{num}\to \texttt{bool}$, and we have rules for typed$\lambda$-abstractions \[\frac{B,x:\sigma \vdash e:\tau}{B \vdash {\lambda x:\sigma{\, . \,}e}:\sigma \to \tau}\] and applications \[\frac{B \vdash e_1 : \sigma \to \tau \qquad B \vdash e_2 : \sigma}{B \vdash e_1 e_2 : \tau}\] anda rule for the fixed-point operator: \[\frac{B \vdash e:\sigma \to \sigma} {B \vdash {\mathtt{Y}(e)}:\sigma}.\]

2.2 Operational semantics

A PCFprogram is a closed term of ground type. We specify howprograms are to be executed by defining an evaluation relation $e\opDownarrow v$ between closed terms $e$ andvalues $v$,where the values are the constants and abstractions of the form${\lambda x:\sigma{\, . \,}e}$. In particular, values of ground typebool are $\texttt{tt},\texttt{ff}$,and values of the ground typenum are${0}$ and all terms of the form \[\mathtt{n} = \underbrace{\texttt{succ}(\ldots \texttt{succ}}_{n}({0}) \ldots ) .\] Evaluation is definedby cases according to the structure of terms, by means of inferencerules for judgements of the form $e \opDownarrow v$. These rulesstate how the result of the evaluation of a term depends on the resultof the evaluation of other terms, the only axioms having the form $v\opDownarrow v$ for every value $v$. For example there is a rule\[\frac{e \opDownarrow v}{{\texttt{succ }e} \opDownarrow {\texttt{succ }v}}\] that states that, if the result of the evaluation of$e$ is $v$, then the result of the evaluation of ${\texttt{succ}e}$ is ${\texttt{succ } v}$. Similarly we can describe theevaluation of the other constants. The evaluation of a term of theform $e_1\ e_2$ proceeds as follows: first $e_1$ is evaluated; ifthe evaluation terminates with value $v'$, then the evaluation of$e_1\ e_2$ proceeds with the evaluation of $v'\ e_2$; if thisterminates with value $v$, this is the value of $e_1\ e_2$,formally \[\frac{e_1 \opDownarrow v' \qquad v'\ e_2 \opDownarrow v}{e_1\ e_2 \opDownarrow v}\] For a value of the form ${\lambda x:\sigma{\, .\,}e_1}$, its application to a term $e_2$ has the value (if any)obtained by evaluating the term $e_1[e_2/x]$ resulting bysubstituting $e_2$ to all free occurrences of $x$ in $e_1$:\[\frac{e_1[e_2/x] \opDownarrow v}{({\lambda x:\sigma{\, . \,}e_1}) e_2 \opDownarrow v}.\] These implement acall-by-name evaluationstrategy: in an application, the term in function position must beevaluated completely before the term in argument position, which isthen passed as actual parameter. The fixed point combinator isessential to the encoding of recursive definitions. Its evaluation isdescribed by the rule \[\frac{e({\mathtt{Y}(e)}) \opDownarrow v}{{\mathtt{Y}(e)} \opDownarrow v}\] which is the only rule whosepremiss involves the evaluation of a larger term than the one to beevaluated: this is why the definition of the evaluation relationcannot be reduced to structural induction.

We shall be especially interested in situations when the evaluation ofa term $e$ does not have a value; in these case we say that $e$diverges, and write $e \opUparrow$. It is in the presenceof divergent terms that the causal structure of the evaluation processis exposed. The initial example is in fact a term that diverges in avery strong sense:

Definition 2.2 (Undefined). For any ground type$\gamma$, define $\Omega:\gamma$ as \[{\mathtt{Y}({\lambda x:\gamma{\, . \,}x})}\]

By inspecting the evaluation rules we see that the only possibleevaluation process gives rise to an infinite regress, therefore$\Omega \opUparrow$.

We can define the usual boolean operations by means of the conditionaloperator, as in the following examples: \[\begin{align}\tag{2} \texttt{and} &= {\lambda x:\texttt{bool}, y:\texttt{bool}{\, . \,}{\texttt{if }x\texttt{ then }y\texttt{ else }\texttt{ff}}}. \label{etbivalente} \\\tag{3} \texttt{or} &= {\lambda x:\texttt{bool}, y:\texttt{bool}{\, . \,}{\texttt{if }x\texttt{ then }\texttt{tt}\texttt{ else }y}} \label{velbivalente}\end{align}\] with the usualtruth tables. However, we have now to take into account thepossibility of divergence of the evaluation process, for example in aterm like $\texttt{or}(\Omega,\texttt{tt})$, therefore we extend theusual truth tables by adding a new boolean value, representing absenceof information, $\bot$ (read as “undefined”) to$\texttt{tt}$ and $\texttt{ff}$, as the value of the term$\Omega$. Here, the first argument to be evaluated is the one on theleft, and if the evaluation of this diverges then the whole evaluationprocess diverges. Consider now an operatorporwhose interpretation is given by thetable \[\tag{4}\label{por} \begin{array}{r|lll} \texttt{por}& \textit{tt}& \textit{ff}&\bot \\\hline\textit{tt}& \textit{tt}& \textit{tt}&\textit{tt}\\ \textit{ff}& \textit{tt}& \textit{ff}&\bot\\ \bot & \textit{tt}& \bot &\bot \end{array}\] In this case $\texttt{por}(\texttt{tt},\Omega) =\texttt{por}(\Omega,\texttt{tt}) = \texttt{tt}$: this is theparallel-or which plays a central role in the fullabstraction problem for PCF. It will turn out that is is not definableby any PCF term, precisely because of its parallel nature. In order tocarry out a semantical analysis of PCF, we need a theory of data typeswithpartial elements and of functions over them that supportan abstract form of recursive definition through fixed pointequations: this is what is achieved in Scott’s theory ofdomains, the original mathematical foundation for denotationalsemantics of programming languages as conceived by Strachey (1966,1967).

2.3 Denotational semantics

2.3.1 Types as domains

What are the general structural properties of a space of partial data?The mathematical theory of computation elaborated by Dana Scott (1970)is an answer to this question, that takes partially ordered setsgenerically calleddomains as basic structures. The partialorder of a domain describes a qualitative notion of“information” carried by the elements. In such a frameworkit is natural to reify divergence by introducing a new element$\bot$ representing absence of information. When $x \sqsubseteq y$in this partial order,

$y$ isconsistent with $x$ and is (possibly)moreaccurate than $x [\ldots]$ thus $x \sqsubseteq y$ means that$x$ and $y$ want to approximate the same entity, but $y$ givesmore information about it. This means we have to allow“incomplete” entities, like $x$, containing only“partial” information. (Scott 1970: 171)

The resulting partially ordered sets should also have the propertythat sequences of approximations, in particular infinite chains $x_0\sqsubseteq x_1 \sqsubseteq \ldots$ should converge to alimit containing the information cumulatively provided by the$x_i$. The same structure is also exploited in Kleene’s proofof the First Recursion Theorem in Kleene 1952 (secs. 66,348–50), and will allow to define a notion of continuousfunction in terms of preservation of limits.

Definition 2.3 (Complete partial orders). A completepartial order (cpo) is a partially ordered set ${\langleD,\sqsubseteq \rangle}$ with a least element $\bot$, and such thatevery increasing chain $x_0 \sqsubseteq x_1 \sqsubseteq \ldots$ ofelements of $D$ has a least upper bound $\bigsqcup_n x_n$.

Given any set $X$, we write $X_{\bot}$ for the set $X \cup \{\bot \}$ obtained by adding a new element $\bot$. It is natural toorder the elements of $X_{\bot}$ according to their amount ofinformation, by setting for $x,y \in X_{\bot}$, \[\begin{aligned}x \sqsubseteq y &\Longleftrightarrow (x = \bot \ \text{ or } \ x = y).\end{aligned}\]Partially ordered structures of the form $X_\bot$ are calledflat domains, among which we have $\texttt{bool}= {\{{\textit{tt}},{\textit{ff}}\}}_\bot$ and $\texttt{num}={\mathbb{N}}_\bot$, that will be used to interpret the ground typesof PCF.

A general requirement on domains is that every element be a limit ofits finite approximations, for a notion of finiteness (orcompactness) that can be formulated entirely in terms of thepartial order structure:

Definition 2.4 (Finite elements of a cpo). If $D$is a cpo, an element $d \in D$ isfinite if, for everyincreasing chain $x_0 \sqsubseteq x_1 \sqsubseteq \ldots$\[d \sqsubseteq \bigsqcup_n x_n \Longrightarrow \exists x_i\ \left(d \sqsubseteq x_i \right).\] For $d \in D$, the notation $\mathcal{A}(d)$ denotesthe set of finite elements below $d$; $\mathcal{A}(D)$ is the setof finite elements of $D$. Finite elements are also calledcompact.

Observe that finite subsets of a set $X$ are exactly the finiteelements of the complete lattice of subsets of $X$. It is usefulalso to observe that this definition only partially matches ourintuition: consider for example the finite element $\infty + 1$ inthe cpo \[0 \sqsubseteq 1 \sqsubseteq 2 \sqsubseteq \cdots \sqsubseteq \infty \sqsubseteq \infty + 1.\]

Definition 2.5 (Algebraic cpo). A $D$ isalgebraic if, for every $d \in D$, there is an increasingchain $x_0 \sqsubseteq x_1 \sqsubseteq \ldots$ of finiteapproximations of $d$ such that \[d = \bigsqcup_n x_n.\] If $D$ is algebraic,we say that the finite elements form abasis of $D$.

One last completeness assumption on algebraic cpo’s is needed inorder to get a category of domains suitable for the interpretation ofPCF:

Definition 2.6. Given a cpo $D$, if $X \subseteqD$ has an upper bound we say that $X$ isconsistent, andwrite $\opuparrow X$, or $x \opuparrow y$ when $X = {\{ x,y\}}$. $D$ isconsistently complete if every $X \subseteqD$ such that $\opuparrow X$ has a least upper bound.

The following notion of domain that has proved extremely convenient asa framework for the denotational semantics of programming languages(Scott 1982):

Definition 2.7 (Domain). Adomain is aconsistently complete algebraic cpo with a countable basis.

2.3.2 An abstract theory of computable functions of higher-types

How can we use the notion of information implicit in the ordering onthe elements of domains to develop an abstract notion ofcomputability? Clearly, a computable function should preservemonotonically any increase of information on its inputs:$f(x) \sqsubseteq f(y)$ whenever $x \sqsubseteq y$. In particular,strict functions $f : D \to E$ over flat domains, those forwhich $f(\bot_D) = \bot_E$, are monotonic.

Consider the domain ${\{ 0,1 \}}^\infty$ whose elements are finiteand infinite sequences of bits $0,1$, where $u \sqsubseteq v$ ifeither $u$ is infinite and $u = v$, or $u$ is finite and $u$is a prefix of $v$. What properties should be true of a computablefunction taking as arguments an infinite sequence of bits ${\langleb_1,b_2,b_3,\ldots \rangle}$? Take as an example the function$\textit{search}:{\{ 0,1 \}}^\infty \to {\mathbb{B}}_\bot$ whosevalue is ${\textit{tt}}$ if, for $u \in {\{ 0,1 \}}^\infty$, $1$occurs in $u$ at least once, otherwise $\bot$. Think of thesequence ${\langle b_1,b_2,b_3,\ldots \rangle}$ as given one elementat a time: the initial segments obtained in this process are anincreasing chain of finite elements of ${\{ 0,1 \}}^\infty$,\[{\langle \rangle} \sqsubseteq {\langle b_1 \rangle} \sqsubseteq {\langle b_1,b_2 \rangle} \sqsubseteq {\langle b_1,b_2,b_3 \rangle} \sqsubseteq \ldots\] having ${\langle b_1,b_2,b_3,\ldots \rangle}$ as alimit (i.e., least upper bound). By monotonicity we have acorresponding increasing chain of values \[\textit{search}({\langle \rangle}) \sqsubseteq \textit{search}({\langle b_1 \rangle}) \sqsubseteq \textit{search}({\langle b_1,b_2 \rangle}) \sqsubseteq \textit{search}({\langle b_1,b_2,b_3 \rangle}) \sqsubseteq \ldots\] If$\textit{search}({\langle b_1,b_2,b_3,\ldots \rangle}) ={\textit{tt}}$, then there must be a finite initial segment${\langle b_1,b_2,\ldots,b_n \rangle}$ for which$\textit{search}({\langle b_1,b_2,\ldots,b_n \rangle}) ={\textit{tt}}$, and this will be the cumulative value of the functionfor the infinite sequence ${\langle b_1,b_2,b_3,\ldots \rangle}$. Ingeneral, a computable function $f : D \to E$ should (be monotonicand) have the property that a finite amount of information on theoutput $f(x)$ must be already obtainable by giving a finite amountof information on the input $x$. This is equivalent to the notion ofcontinuity originally introduced by Scott in his theory of computablefunctions over domains:

Definition 2.8 (Continuous functions). If ${\langleD,\sqsubseteq _D \rangle},{\langle E,\sqsubseteq _E \rangle}$ arecpo’s and $f : D \to E$ is monotonic, $f$ iscontinuous if \[f(\bigsqcup_i x_i) = \bigsqcup_i f(x_i)\] for every increasing chain $x_0\sqsubseteq x_1 \sqsubseteq \ldots \subseteq D$.

From the point of view of denotational semantics, a fundamentalproperty of continuous functions $D \to D$ is that they admit aleast fixed point, whose construction can be carried out uniformly andcontinuously:

Theorem 2.1 (The Fixed Point Theorem for continuousfunctions) Let $f : D \to D$ be a continuous function and $x \inD$ be such that $x \sqsubseteq f(x)$. Then the element \[\bigsqcup_{n \in {\mathbb{N}}} f^{(n)}(x)\]is the least $y \sqsupseteq x$ such that $f(y) = y$.

Definition 2.9. The least fixed point of a continuous$f : D \to D$ is the element of $D$ defined by \[{\texttt{fix}(f)} =_{\textrm{def}} \bigsqcup_{n \in {\mathbb{N}}} f^{(n)}(\bot).\]

The continuous functions from $D$ to $E$, for cpo’s${\langle D,\sqsubseteq _D \rangle}$ e ${\langle E,\sqsubseteq _E\rangle}$, form a cpo $[D \to E]$, ordered pointwise by setting,for $f,g:D \to E$: \[f \sqsubseteq g \Longleftrightarrow \forall d \in D. f(d) \sqsubseteq _E g(d).\] $[D \to E]$ is a domain if $D$and $E$ are, and ${\texttt{fix}(\cdot)}:[D \to D] \to D$ iscontinuous. A further construction on cpo’s which also extendsto domains and is very frequently used iscartesian product:given cpo’s $D,E$, their cartesian product is defined as theset $D \times E$ of pairs ${\langle d,e \rangle}$ where $d \inD$ and $e \in E$, ordered pointwise: ${\langle d,e \rangle}\sqsubseteq {\langle d',e' \rangle}$ if and only if $d \sqsubseteq_D d'$ and $e \sqsubseteq _E e'$. We can summarize theseconstructions in categorical language (Plotkin 1978, Other InternetResources), saying that the category whose objects are domains andwhose morphisms are the continuous functions iscartesianclosed.

2.3.3 Continuous semantics for PCF

Thestandard interpretation of PCF consists of a family ofcpos $D^\sigma$, for each type $\sigma$, where $D^\texttt{num}={\mathbb{N}}_{\bot}$ and $D^\texttt{bool}= {\mathbb{B}}_{\bot}$,$D^{\sigma \to \tau} = [D^\sigma \to D^\tau]$ and the PCF constantshave the natural interpretation as strict continuous functions of theappropriate type, for example $\texttt{cond}: {\mathbb{B}}_{\bot} \to{\mathbb{N}}_{\bot} \to {\mathbb{N}}_{\bot} \to {\mathbb{N}}_{\bot}$is interpreted as: \[\textit{cond}(b)(x)(y) = \left\{ \begin{array}{ll} x&\text{if $b = \texttt{tt}$}\\ y &\text{if $b = \texttt{ff}$}\\ \bot &\text{if $b = \bot$,} \end{array} \right.\] Furthermore, the operator${\mathtt{Y}(\cdot)}$ is interpreted as the continuous functional${\texttt{fix}(\cdot)}$ at the appropriate type. This is theinterpretation considered in Scott 1969b) and Milner 1973.

The possibility that $e$ may contain free occurrences of variables(whose types are given by a basis $B$) slightly complicates theinterpretation of terms, making it depend on a further parameter, anenvironment $\rho$ mapping each free variable $x:\tau$ of$e$ to an element of $D^\tau$ (if the latter condition issatisfied, we say that $\rho$respects $B$). Of course,the environment is irrelevant when $e$ is closed.

The standard interpretation of PCF terms $e:\sigma$ (from a basis$B$) is then an element ${\lll e\rll \rho} \in D^\sigma$, for anyenvironment $\rho$ such that $\rho$ respects $B$, built bystructural induction on terms, interpreting application as functionapplication and $\lambda$-abstractions by (continuous) functions.More generally, an interpretation iscontinuous if every$D^\sigma$ is a cpo and $D^{\sigma \to \tau}$ consists ofcontinuous functions $D^\sigma \to D^\tau$.

Amodel of PCF is an interpretation that satisfies theexpected identities between terms of the same type. We shall omit thedetails of the general characterization of models of PCF, for whichthe reader is referred to Ong (1995: sec. 3.2) and Berry, Curien,& Lévy (1985: sec. 4), but just to point out an example ofwhat must be taken into account when such a generality is needed, inorder to admit interpretations where the elements at function typesare not, strictly speaking, functions, we have to assume a family ofapplication operations \[\cdot_{\sigma\tau}: D^{\sigma \to \tau} \times D^\sigma \to D^\tau\] so that, if $B \vdashe_1 : \sigma \to \tau$ and $B \vdash e_2 ; \sigma$, ${\llle_1e_2\rll \rho} = {\lll e_1\rll \rho} \cdot_{\sigma\tau} {\llle_2\rll \rho} \in {{{D}^{\tau}}}$. A model isorder-extensional if, for all elements $f,g \in{{{D}^{\sigma \to \tau}}}$, $f \sqsubseteq g$ if and only if $f\cdot x \sqsubseteq g \cdot x$ for all $x \in {{{D}^{\sigma}}}$. Amodel isextensional if, for all elements $f,g \in{{{D}^{\sigma \to \tau}}}$, $f = g$ if and only if $f \cdot x = g\cdot x$ for all $x \in {{{D}^{\sigma}}}$. An element $d \inD^\sigma$ of a model isdefinable is there is a closed terms$e:\sigma$ such that $d = {\lll e\rll }$.

2.4 Relating operational and denotational semantics

The general setting for discussing full abstraction requires that weintroduce the following notions:

Definition 2.11 (Observational preorder andequivalence) Given PCF terms $e$ and $e'$ of the same type$\sigma$, we write $e \precsim_{\textrm{obs}} e'$ (read$e$is observationally less defined than $e'$) if, for everyprogram context $C\blbr$ with a hole of type $\sigma$ and anyvalue $v$, \[C[e] \opDownarrow v \ \text{ implies that } \ C[e'] \opDownarrow v.\] We say that $e$ and $e'$ areobservationally equivalent, and write $e\simeq_{\textrm{obs}} e'$, if $e \precsim_{\textrm{obs}} e'$ and$e' \precsim_{\textrm{obs}} e$.

Observational equivalence is a congruence. Another congruence on PCFterms is given by equality of denotations in a model:

Definition 2.11 (Denotational preorder andequivalence). Given PCF terms $e$ and $e'$ of the same type$\sigma$ relative to a basis $B$, we write $e\precsim_{\textrm{den}} e'$ if ${\lll e\rll \rho} \sqsubseteq {{\llle'\rll} \rho}$ for all environments $\rho$ respecting $B$. Wewrite $e \simeq_{\textrm{den}} e'$ if $e \precsim_{\textrm{den}}e'$ and $e' \precsim_{\textrm{den}} e$ .

Proposition 2.1 (Computational adequacy for PCF). Thefollowing two statements hold for the standard model of PCF, and areequivalent:

For any two PCF terms of the same ground type $e,e'$, $e\simeq_{\textrm{den}} e'$ implies $e \simeq_{\textrm{obs}}e'$;
For any closed PCF term $e$ of ground type and any value $v$of that type, ${\lll e\rll } = {\lll v\rll }$ if and only if $e\opDownarrow v$;

We can now justify our intuitive interpretation of $\bot$ in thestandard model, where ground types are interpreted as flatdomains:

Corollary 2.1. For any closed PCF term $e$ ofground type, $e \opUparrow$ if and only if ${\lll e\rll } =\bot$.

InSection 1.3 we have already defined a very general notion of (equational) fullabstraction, based on synonymy, i.e., equality of interpretation ofterms. In the case PCF, whose intended models are partially ordered atall types, we can define a stronger property:

Definition 2.12 (Inequational full abstraction). Acontinuous model ${\langle {\{ {{{D}^{\sigma}}} \mid \sigma \in\texttt{Types}}\},{\lll \cdot\rll \cdot} \rangle}$ of PCF isinequationally fully abstract if, for closed terms $e,e'$,$e \precsim_{\textrm{obs}} e'$ implies ${\lll e\rll } \sqsubseteq{\lll e'\rll }$.

Definability is the key to full abstraction, as shown by the followingimportant result of Milner and Plotkin:

Theorem 2.2. A continuous, order-extensional model ofPCF is fully abstract if and only if for every type $\sigma$,${{{D}^{\sigma}}}$ is a domain whose finite elements aredefinable.

We turn now to the failure of the full abstraction property for thestandard model of PCF, as shown by Plotkin in his classic study(Plotkin 1977):

Proposition 2.2. The standard model of PCF is notfully abstract with respect to call-by-name evaluation.

The proof is based on the observation that we can build PCF terms oftype $(\texttt{bool}\to \texttt{bool}\to \texttt{bool}) \to\texttt{num}$ that recognize the parallel-or function. Specifically,consider the “test” terms $T_i$ defined as follows,where $i = {0},1$:

$\lambda f : \texttt{bool}\to \texttt{bool} \to \texttt{bool.if } (f\texttt{ tt } \bot_{\texttt{bool}} \texttt{ then}$

$\texttt{if } (f \bot_{\texttt{bool}} \texttt{ tt}) \texttt{ then}$

$\texttt{if } (f \texttt{ ff ff}) \texttt{ then}$

$\bot_{\texttt{num}}$

$\texttt{else } i$

$\texttt{else } \bot_{\texttt{num}}$

Then, ${\mathcal{D}\lll T_{0}\rll}\ \texttt{por} = {0}\neq 1 ={\mathcal{D}\lll T_1 \rll }\ \texttt{por} $, whereporis defined by table $(\ref{por})$, so$T_{0} {\simeq_{\textrm{den}}}T_1$ does not hold. However, noprogram context in PCF can separate $T_{0}$ and $T_1$ becausepor is not definable. This can be shownby characterizing in a combinatorial way the relations of dependenceinduced by the evaluation process of a program among the evaluationprocesses of its (sub)terms, as Plotkin does in the Activity Lemma(Plotkin 1977: Lemma 4.2). As an alternative, it is possible to builda computationally adequate models of PCF whose functions enjoy a weaksequentiality property (that we discuss below, inSection 2.5.1) and where, therefore, the functionporis ruled out: a complete formal proof along these lines is given inGunter 1992 (sec. 6.1).

One option to solve the full abstraction problem is to extend thelanguage: a remarkable result of Plotkin (1977) shows that addingparallel-or is enough:

Proposition 2.3. The standard model is fully abstractfor the language PCF extended with parallel-or.

Milner (1977) has shown that there is a fully abstract model of PCF,by taking the set of closed terms at each type $\sigma$ identifyingobservationally equivalent terms and by completing the resultingpartially ordered set turning it into a cpo.

Corollary 2.2. There is a unique continuous, orderextensional, inequationally fully abstract model of PCF, up toisomorphism.

The full abstraction problem for PCF consists in finding a directdescription of the class of domains and continuous functions that makeup the fully abstract model. A solution to this problem would requirea precise criterion for assessing the extent to which a proposeddescription of the model is satisfactory. If one accepts the“precise minimal condition that a semantic solution of the fullabstraction problem should satisfy” given by Jung &Stoughton (1993), namely the possibility of describing in an effectiveway the domains $D^\sigma$ of a finitary version of PCF (whose onlyground type isbool), then the story offailed attempts to give such a direct description of the fullyabstract model is justified, with hindsight, by a result of Loader(2001):

Theorem 2.3. Observational equivalence for finitaryPCF is not decidable.

It is still possible, however, that one could find a directdescription of anintensionally fully abstract model(Abramsky et al. 2000: 411):

Definition 2.13 (Intensional full abstraction). Amodel of PCF isintensionally fully abstract if every$D^\sigma$ is algebraic and all its compact elements aredefinable.

Pursuing this line of development of the full abstraction problemleads us to game semantics, which will be the topic of the nextSection. Before that, we outline the main attempts to reduce the modelby means of a semantical characterization of higher-order sequentialcomputation.

2.5 Towards a sequential semantics

The reason for the failure of full abstraction of the continuoussemantics of PCF is the existence of functions whose evaluationrequires parallel computation. We describe now some proposals forcharacterizingsequentiality of functions by means ofproperties related to the structure of the domains on which they aredefined. This has been an area of intensive research toward thesolution of the full abstraction problem for PCF, and some of theinsights that emerged from it lead very naturally to the game modelsdiscussed inSection 3. In addition, the following summary of attempts at a characterizationof sequentiality is also a very interesting demonstration of theexpressive power of the language of partial order in the semanticanalysis of programming concepts.

Intuitively, a sequential function is one whose evaluation proceedsserially: this means that it is possible to schedule the evaluation ofits arguments so that the evaluation of the function terminates withthe correct value; if the evaluation of one of them diverges, thewhole evaluation diverges. At each stage of this process there is anargument whose value is needed to obtain more information on theoutput of the function. In order to account for this causal structureof computations at the semantical level, we need to enrich the domainstructure so that the order on the elements reflect the happening ofcomputationalevents and their causal order. This suggestsanother way of interpreting the abstract notion of information thatmotivated the axioms of a cpo inSection 2.3.1. Now,

information has to do with (occurrences of) events: namely theinformation that those events occurred. For example in the case of${\mathbb{N}}_{\bot}$, $\bot$ might mean that no event occurredand an integer $n$, might mean that the event occurred of theinteger $n$ being output (or, in another circumstance being input).(Plotkin 1978, Other Internet Resources)

2.5.1 Stability

One interpretation of events regards them as the production of valuesin the evaluation of an expression. This interpretation originates inthe context of bottom-up computation of recursive programs developedby Berry (1976), where a recursive definition is translated into agraph displaying the dependence of results of an expression on resultsof its subexpressions. This context naturally suggests the notion ofproducer of an event $x$, as a set of events that must havehappened in order that $x$ may happen. Reformulating thisobservation in the language of partial orders, Berry (1976)defined:

Definition 2.14 (Stability). Let $D_1,\ldots,D_n,D$ be flat cpo’s and $f: D_1\times \ldots \times D_n \to D$monotonic (hence continuous). Then $f$ isstable if forevery $\vec{x} = {\langle x_1,\ldots,x_n \rangle} \in D_1\times\ldots \times D_n$ there is a unique minimal element $m(f,x)\sqsubseteq \vec{x}$ such that $f(m(f,\vec{x})) = f(\vec{x})$.

Clearly, the parallel-or function is not stable: the value$\texttt{por}(\bot,{\textit{tt}}) = {\textit{tt}}=\texttt{por}({\textit{tt}},\bot)$ has no minimal producer. Aremarkable property of stable functions is that they allow to build anew model of PCF, where ${{{D}^{\sigma \to \tau}}}$ is the set ofstable functions on the domains that interpret the types $\sigma$and $\tau$, which are refinements of Scott domains calleddI-domains (Berry 1978). From our point of view, theimportant outcome of these definitions is the following adequacyresult (Gunter 1992: chap. 6):

Proposition 2.4. The interpretation of PCF terms aselements of dI-domains, where $D^{\sigma \to \tau}$ is the dI-domainof stable functions from $D^\sigma$ to $D^\tau$ with the stableorder, is a computationally adequate model of PCF.

This result completes the argument showing the failure of fullabstraction for the continuous model of PCF at the end ofSection 2.4, if the informal notion of sequentiality used there is formalized asstability. The stable model of PCF has recently been shown to be fullyabstract for an extension of PCF (Paolini 2006).

2.5.2 Sequential functions

The first definitions of sequentiality, due to Vuillemin (1974) andMilner (1977) stated that an $n$-ary functions $f$ over flatdomains issequential at argument ${\langle x_1,\ldots,x_n\rangle}$ if there is asequentiality index $i$ of$f$, depending on ${\langle x_1,\ldots,x_n \rangle}$, such thatevery increase in the output information must increase the informationat argument $i$. For example, the function $\texttt{cond} :{\mathbb{B}}_{\bot} \times {\mathbb{N}}_{\bot} \times{\mathbb{N}}_{\bot} \to {\mathbb{N}}_{\bot}$ is sequential in thissense at any input tuple. In fact, its sequentiality index at${\langle \bot,m,n \rangle}$ is 1; its sequentiality index at${\langle {\textit{tt}},m,n \rangle}$ is 2, and its sequentialityindex at ${\langle {\textit{ff}},m,n \rangle}$ is 3. There ishowever no sequentiality index for the function $\texttt{por} :{\mathbb{B}}_{\bot} \times {\mathbb{B}}_{\bot} \to{\mathbb{B}}_{\bot}$ at the input ${\langle \bot,\bot\rangle}$.

While all sequential functions (over flat domains) are stable,sequentiality is strictly stronger than stability. For example, thecontinuous function from ${\mathbb{B}}_\bot \times {\mathbb{B}}_\bot\times {\mathbb{B}}_\bot$ to ${\mathbb{B}}_\bot$ defined as thesmallest continuous extension of the three assignments \[{\langle {\textit{tt}},{\textit{ff}},\bot \rangle} \mapsto {\textit{tt}}, {\langle {\textit{ff}},\bot,{\textit{tt}}\rangle} \mapsto {\textit{tt}}, {\langle \bot,{\textit{tt}},{\textit{ff}}\rangle} \mapsto {\textit{tt}}.\]has no sequentiality index at the argument ${\langle \bot,\bot,\bot\rangle}$, but is stable because the arguments ${\langle{\textit{tt}},{\textit{ff}},\bot \rangle},{\langle{\textit{ff}},\bot,{\textit{tt}}\rangle},{\langle\bot,{\textit{tt}},{\textit{ff}}\rangle}$ are pairwiseinconsistent.

The following result adds support to the search for a semanticalcharacterizations of sequentiality:

Proposition 2.5. Let $f : D_1 \times \cdots \timesD_n \to D$ be a continuous function, where $D_i,D$ are either${\mathbb{N}}_\bot$ or ${\mathbb{B}}_\bot$. Then $f$ issequential if and only if it is definable in PCF.

2.5.3 Concrete data structures and sequential algorithms

If the domains needed for an adequate definition of sequentiality areto describe the causality relations among occurrences of computationalevents, then it is necessary to enrich our picture by consideringevents as located atplaces, generalizing the notion ofargument place in the definitions of Vuillemin and Milner whichdepends on how a function is presented. This led to a notion ofconcrete data structure (cds) (Kahn & Plotkin 1993) andto an axiomatization of the order-theoretic properties of domains offirst-order data. Kahn and Plotkin obtained a representation theoremfor the domains described by their axioms, theconcretedomains, in terms of thestates of a process ofexploration of a concrete data structure that consists in filling,given a state $x$, any cell enabled by sets of events that havealready happened in $x$, starting frominitial cellsenabled in the initial, empty state: this is similar to provingtheorems in an abstract deductive system whose rules are theenablings. As a motivating example, think of a linked list of, say,natural numbers. The initial cell may be filled at any time with anyvalue $n_1$. This event enables the second cell of the list, whichmay then (and only then) be filled with any value $n_2$, and so onfor all later cells.

Observe that the framework of concrete data structures gives thenecessary notions to reconstruct a semantical version ofsequentiality. Roughly, a monotonic function $f$ from states of$M$ to states of $M'$ issequential (at state $x$) if,for any output cell $c'$, there is an input cell $c$ that must befilled in any transition from $x$ to $y$ such that the transitionfrom $f(x)$ to $f(y)$ fills $c'$ (if such a $c'$ does exist)(Curien 1986: Def. 2.4.5). The cell $c$ is thesequentiality index for $f$ at $x$ for $c'$.

The category whose objects are the concrete data structures and whosemorphisms are the sequential functions just defined is, however, notcartesian closed, not unexpectedly. This observation (for a simpleproof, see Amadio & Curien 1998 (theorem 14.1.12)) prevents theuse of this category as a model of PCF. However, it is possible todefine for every two concrete data structures $M,M'$ a new one $M\to M'$ whose states representsequential algorithms andwhich is the exponential object of $M$ and $M'$ in a cartesianclosed category whose morphisms are sequential algorithms (Curien1986: sec. 2.5). The generalizations of the model theory of PCF tocategorical models allows us to obtain a model of PCF from this newcategory, even though its morphisms are not functions in the usualset-theoretic sense. It turns out that the sequential algorithm modelis not extensional, because there are distinct PCF terms that denotethe same continuous function yet represent distinct algorithms. As anexample, consider the following two terms, that denote the samefunction but different algorithms: \[\begin{aligned}\texttt{lror}(x,y) &= \texttt{if }x\texttt{ then }({\texttt{if }y\texttt{ then }\texttt{tt} \texttt{ else }x}) \\&\quad \texttt{ else }({\texttt{if }y\texttt{ then }\texttt{tt}\texttt{ else }\texttt{ff}}) \\\texttt{rlor}(x,y) &= \texttt{if }y\texttt{ then }({\texttt{if }x\texttt{ then }\texttt{tt}\texttt{ else }y})\\&\quad \texttt{ else }({\texttt{if } x\texttt{ then }\texttt{tt}\texttt{ else }\texttt{ff}}). \end{aligned}\] By suitablyintroducing error values $\textit{error}_1,\textit{error}_2$ in thesemantics, and enforcing an error-propagation property of theinterpretations of terms (thus enlarging the observables of thelanguage), thefunctions corresponding to the above terms canthen be distinguished: clearly, for the interpreting functions$\textit{lror}$ and $\textit{rlor}$ we have \[\begin{aligned} \textit{lror}(\textit{error}_1,\textit{error}_2) &= \textit{error}_1 &\textit{rlor}(\textit{error}_1,\textit{error}_2) &= \textit{error}_2\end{aligned}\] whichalso points to the possibility of proving full abstraction of this(non-standard) extensional model with respect to an extension of PCFwith control operators (Cartwright, Curien, & Felleisen 1994).

Before leaving this overview of the quest for an extensionalcharacterization of higher-order sequentiality, we should mentionBucciarelli & Ehrhard (1994) who introduced a refinement of thedI-domains of Berry supporting a notion ofstrongly stablefunction which allows them to build an extensional model of PCF,which is not fully abstract. The reason for the failure of fullabstraction in this case depends on the fact that PCF-definablefunctionals satisfy extensionality properties that fail when functionsare ordered by the stable order. This was also the reason thatmotivated the introduction ofbidomains (Berry 1978), wherethe stable and extensional (= pointwise) orderings of functionscoexist.

2.6 Historical notes and further readings

The problem of full abstraction has been anticipated in a large amountof work on the relations between the denotational and operationalinterpretations of programming languages. In particular, thepioneering work on the semantics of recursive programs carried out inStanford in the early 1970s by a group of people gathering aroundZohar Manna, and including Jean Marie Cadiou, Robin Milner and JeanVuillemin, also interacting with Gilles Kahn.

A related tradition was also quite influential on the background ofthe full abstraction problem, namely the characterizations ofsemantical notions like continuity and sequentiality inside syntacticmodels of the (untyped) $\lambda$-calculus based on Böhm trees(Barendregt 1984), mainly due to Lévy and Berry (see Berry etal. 1985 and Curien 1992) for accounts of the search for fullyabstract models of PCF along this line).

The basic papers on full abstraction for PCF are Milner 1977; Plotkin1977. They can be read together as giving a coherent picture of thesemantic analysis of this language. An independent approach to fullabstraction came from the Russian logician Vladimir Sazonov whocharacterized definability in PCF in terms of a certain class ofsequential computational strategies (Sazonov 1975, 1976). His work,however, had no direct influence on the bulk of research on the fullabstraction problem, and only recently there have been attempts torelate Sazonov’s characterization to the game theoreticapproaches (Sazonov 2007).

Another, completely different approach to full abstraction, exploitsspecial kinds oflogical relations in order to isolatequotients of the continuous model. The first use of logical relationsin the context of the problem of full abstraction is Mulmuley 1987,but the resulting construction of a fully abstract model is obtainedby brute force and therefore is not what the full abstraction problemsearches for. Later, Sieber (1992) and O’Hearn & Riecke(1995) have employed refinements of this technique to gain a betterinsight into the structure of the fully abstract models,characterizing the definable elements of the standard continuous modelby means of invariance under special logical relations cutting out thenon-sequential functions.

Detailed accounts of the full abstraction problem for PCF can be foundin Gunter 1992 (chaps 5,6), Streicher 2006, Ong 1995, Stoughton 1988and Amadio & Curien 1998 (chaps 6, 12, 14), in approximatelyincreasing order of technical complexity. The emphasis on therecursion-theoretic aspects of PCF and its full abstraction problemare dealt with in detail in the textbook (Longley & Normann 2015:chaps 6, 7); a shorter account can be found in Longley 2001 (sec.4).

3. Game semantics

3.1 Full completeness

Theorem 2.2 highlights the fundamental role of definability of finite elements inthe fully abstract model of PCF, an aspect that has been stressed inCurien 2007. As a smooth transition to the formalisms based on games,and partly following the historical development of the subject, wepause shortly to examine another aspect of definability that arises atthe border between computation and the proof theory of constructivelogical systems. It has been a remarkable discovery that the structureof natural deduction proofs for, say, the implicative fragment ofintuitionistic propositional calculus is completely described by termsof the simply typed $\lambda$-calculus, where a provablepropositional formula of the form $\sigma \to \tau$ is read as thetype of the terms representing its proofs. This is thepropositions-as-types correspondence, to be attributed toCurry, de Bruijn, Scott, Läuchli, Lawvere and Howard, whichextends to much richer formal systems (for a history of thiscorrespondence see Cardone & Hindley 2009: sec. 8.1.4).

The existence of this correspondence makes it possible to speak of asemantics of proofs, that extends to constructive formalproofs the denotational interpretations of typed $\lambda$-calculi,and in this context it also makes sense to ask whether an element$x$ of some $D^\sigma$ in a model of a typed $\lambda$-calculusis the interpretation of some proof of formula $\sigma$. A furtherquestion asks whetherevery element of $D^\sigma$satisfying a suitably chosen property is the interpretation of a proofof formula $\sigma$. Suitable properties may be for exampleinvariance under logical relations, suitably defined over each$D^\sigma$, like in several results of Plotkin, Statman and otherssummarized in Barendregt, Dekkers, & Statman 2013 (I.3, I.4). Wecan read the latter question as asking for a strong form ofcompleteness for that system calledfull completeness(Abramsky & Jagadeesan 1994), whose definition can be betterunderstood in a categorical semantics of systems of constructivelogic. It is common to interpret formulas $A$ of such systems asobjects ${\lll A \rll }$ of suitable categories $\mathbb{M}$, andproofs $p$ of sequents $A \vdash B$ as morphisms $\lll p \rll :\lll A \rll \longrightarrow \lll B \rll$. While ordinary completenessstates that for every valid sequent $A \vdash B$ the set$\mathbb{M}({\lll A \rll },{\lll B \rll })$ of morphisms is notempty, in the present setting full completeness expresses the strongerrequirement that every morphism $f: \lll A \rll \longrightarrow \lllB \rll$ in a semantical category $\mathbb{M}$ arises as theinterpretation of some proof, i.e., $f = {\lll p \rll }$ for someproof $p$ of the sequent $A \vdash B$. Full completeness resultshave been proved for several subsystems of linear logic Girard (1987),see Abramsky (2000) for a general framework. Furthermore, it has alsosuggested techniques for achieving the definition of models of PCFenjoying the strong definability property required by intensional fullabstraction.

3.2 Interaction

In our description of the refinements to the continuous model of PCFin order to guarantee the definability of finite elements at eachtype, we have progressively come closer to an interactive explanationof computation. For example, the action of a sequential algorithm $M\to M'$ (Curien 1986: sec. 3.4) exploits an external calling agentwhich triggers a cycle of requests and responses on input cellsleading (possibly) to the emission of an output value. Thatinteraction should be a central notion in the analysis of computation,especially in relation to full abstraction, is perhaps a naturaloutcome of the observational stance taken in the definition ofoperational equivalence. Our short account of game semantics startsprecisely from an analysis of a general notion ofinteractionas a motivation to a first formalization of games which is howeverrich enough to provide a universe for the interpretation of arestricted set of types and terms. Later we shall add to thisdefinition of game and strategies the features needed to express theconstraints that allow strategies to characterize preciselyhigher-order, sequential computations, which is the aim set fordenotational semantics by the full abstraction problem. The presentaccount of the conceptual background of game semantics owes much tothe work of Abramsky and Curien (Abramsky 1994, 1996, 1997; Curien2003a).

The relevant notion of interaction has been isolated as the result ofcontributions that come from widely different research areasintensively investigated only in relatively recent years, notablylinear logic (Girard 1987) and the theory of concurrent processes. Itis in these areas that a notion ofcomposition as interactionofmodules takes shape. We give here just a simple examplewhere the composition of modules in the form of “parallelcomposition + hiding” is found in nature, in order to connect itwith the origin of this idea in the semantics of concurrent processesdeveloped by Hoare (1985), and also to afford a first glimpse into asimplified game formalism.

Consider a module $S$ with four channels labeled$a_\textrm{in},a_\textrm{out},r_\textrm{in},r_\textrm{out}$. Themodule is intended to return on channel $a_\textrm{out}$ thesuccessor of the number $n$ incoming through channel$a_\textrm{in}$, therefore its behavior can be specified asfollows:

$S$ receives an input signal $\mathbf{?}_\textrm{in}$ onchannel $r_\textrm{in}$, then
emits a signal $\mathbf{?}_\textrm{out}$ on channel$r_\textrm{out}$, and
waits for a value $n$ on channel $a_\textrm{in}$ and then,after receiving it,
emits a value $n+1$ on channel $a_\textrm{out}$.

(This pattern of interaction is formally identical to thehandshake protocol which is used in hardware design tosynchronize components in order to avoid hazards caused byinterference of signals.) This behavior can be mapped on the channelsas follows:

[a rectangular box with the letter S inside, on the upper left a line ending in a white circle is labeled '?_in', on the lower left a line ending in a black circle is labeled 'n+1_out', on the upper right a lined ending in a black circle is labeled '?_out', and on the lower right a line ending in a white circle is labeled 'n_in']

Figure 1: A module for the successorfunction.

where $\circ$ means input or, more generally, apassiveinvolvement of the module in the corresponding action, whereas$\bullet$ means output, oractive involvement in theaction. We can describe the behavior of $S$ usingtraces(Hoare 1985), i.e., finite sequences of symbols from the infinitealphabet $ \alpha S = {\{\mathbf{?}_\textrm{in},\mathbf{?}_\textrm{out},n_\textrm{in},m_\textrm{out}\}}: $ \[\tau S = {\{ \varepsilon,\mathbf{?}_\textrm{in},\mathbf{?}_\textrm{in} \mathbf{?}_\textrm{out}, \mathbf{?}_\textrm{in} \mathbf{?}_\textrm{out} n_\textrm{in},\mathbf{?}_\textrm{in} \mathbf{?}_\textrm{out} n_\textrm{in} n+1_\textrm{out},\ldots \}}\] If we consider another instance $S'$ of $S$with alphabet $ \alpha S' = {\{\mathbf{?}_\textrm{in}',\mathbf{?}_\textrm{out}',n_\textrm{in}',m_\textrm{out}'\}} $ we can compose $S$ and $S'$ by identifying (= connecting)channels $r_\textrm{out},r_\textrm{in}'$, and $a_\textrm{in} ,a_\textrm{out}'$, and the signals passing through them, as shown:\[\begin{aligned}\mathbf{?}_\textrm{out} , \mathbf{?}_\textrm{in}' &\leadsto x\\n+1_\textrm{in} , n+1_\textrm{out}' &\leadsto y\end{aligned}\] This represents the parallel composition of the modules,$S \| S'$:

$[two rectangles, the one on the left containing 'S' and the one on the right 'S\prime'. The upper left of the left one has a line ending in a white circle labeled '?_in', on the lower left a line ending in a black circle labeled 'n+2_out'. The upper right of the right rectangle has a line ending in a black circle labeled '?\prime_out' and the lower right a line labeled 'n\prime_in'. The two rectangles are connected by two lines. The upper with a black circle on the left and a white circle on the right labeled 'x'. The lower with a white circle on the left and at black circle on the right labeled 'y'.]$

Figure 2

The behavior of the compound module is described by the set of traces\[{\{ \varepsilon,\mathbf{?}_\textrm{in},\mathbf{?}_\textrm{in} x, \mathbf{?}_\textrm{in} x \mathbf{?}_\textrm{out}',\mathbf{?}_\textrm{in} x \mathbf{?}_\textrm{out}' n_\textrm{in}',\mathbf{?}_\textrm{in} x \mathbf{?}_\textrm{out}' n_\textrm{in}' y, \mathbf{?}_\textrm{in} x \mathbf{?}_\textrm{out}' n_\textrm{in}' y n+2_\textrm{out}, \ldots \}}\] The symbols $x,y$ can now be hidden, representing thebehavior of the final system

$[two rectangles with dashed lines for sides, the one on the left containing 'S' and the one on the right 'S\prime'. The upper left of the left one has a line ending in a white circle labeled '?_in', on the lower left a line ending in a black circle labeled 'n+2_out'. The upper right of the right rectangle has a line ending in a black circle labeled '?\prime_out' and the lower right a line labeled 'n\prime_in'. The two rectangles are connected by two dashed lines. The upper with a black circle on the left and a white circle on the right and not labeled. The lower with a white circle on the left and at black circle on the right and not labeled. A larger rectangle with solid sides encloses the two rectangles so that the left side of the left rectangle and the right side of the right rectangle are on the left and right sides of the enclosing rectangle]$

Figure 3

whose traces have the required form \[{\{ \varepsilon,\mathbf{?}_\textrm{in},\mathbf{?}_\textrm{in} \mathbf{?}_\textrm{out}',\mathbf{?}_\textrm{in} \mathbf{?}_\textrm{out}' n_\textrm{in}',\mathbf{?}_\textrm{in} \mathbf{?}_\textrm{out}' n_\textrm{in}' n+2_\textrm{out}, \ldots \}}.\] This example containsmany of the ingredients on which game semantics is based. There is theidea of a System, whose behavior is triggered by an incoming requestfrom its Environment: in a game formalism these are the roles ofProponent and Opponent in a two-person game. The behavior of eachmodule is described as the trace of its possible interactions withother agents, and the behaviors can be composed by a peculiar changeof role whereby the module who plays as System (in the above example,$S$ emitting a request signal on channel $r_\textrm{out}$) is madeto behave as Environment with respect to $S'$ when this signal isreceived in input on channel $r_\textrm{in}'$. Let us see how thisexample can be generalized.

3.3 Games and strategies

We only give the definitions needed to understand the basicconstructions on games and to see how these form a category, followingAbramsky 1997 and Hyland 1997 that contain more formal details andproofs.

3.3.1 Games

Definition 3.1 Agame $G$ is specified bygiving a set ofmoves $M_G$, alabeling $\ell_G$of the moves as either moves of theProponent ($P$) or asmoves of theOpponent ($O$). Furthermore, there is a set ofpositions $P_G$ which is a set of sequences of moves where:(1) the two players alternate, starting with $O$; (2) if $s \inP_G$ then every prefix $s'$ of $s$ is also in $P_G$.

As an example, consider a game associated with the data-type ofBoolean values, $G_\texttt{bool}$. There are three possiblemoves,

an $O$-move $?_\texttt{bool}$ and
two $P$-moves $\textit{tt}, \textit{ff}$

(i.e., $\ell_\texttt{bool}(?_\texttt{bool}) = O,\ell_\texttt{bool}({\textit{tt}}) = \ell_\texttt{bool}({\textit{ff}})= P$). The positions in this game are \[?_{\texttt{bool}}, ?_{\texttt{bool}} \texttt{tt}, ?_{\texttt{bool}} \texttt{ff}:\] think of$?_\texttt{bool}$ as a cell (as in a concrete data structure) whichcan be filled by one of the two values ${\textit{tt}}$ and${\textit{ff}}$, or as a question by the Opponent that admits asanswers by the Proponent either ${\textit{tt}}$ or${\textit{ff}}$. Similarly we can describe a game $G_\texttt{num}$with an $O$-move $?_\texttt{num}$ and $P$-moves $n \in{\mathbb{N}}$.

3.3.2 Strategies and their composition

The players move in a game $G$ alternately, at each move reaching alegal position in $P_G$. Their behavior is best thought of asdescribing a strategy that prescribes deterministically what is$P$’s response to $O$ in a position where it is its turn tomove.

Definition 3.2. Astrategy $\sigma$ on agame $G$ is a prefix-closed set of even-length positions of $G$such that, each time $sab,sac \in \sigma$, we have $b=c$.

For example, the strategies on $G_\texttt{num}$ are $\varepsilon$and all sequences $?_\texttt{num}n$, corresponding respectively tothe elements $\bot$ and $n$ of the domain ${\mathbb{N}}_\bot$.

We would like to consider the behavior of the successor moduledescribed above as an element of a set $G_\texttt{num}\multimapG_\texttt{num}$ of strategies that compute functions over the naturalnumbers. If we consider only the sequences of interactions of $S$taking place either on the left or on the right side of the module ofFigure 1, we see that they describe positions of $G_\texttt{num}$, with aninversion of polarity (active/passive) depending on which side theinteractions take place: the module is initially passive, and becomesactive upon receiving a request from the environment. Such inversion,represented by the complementary labeling of the moves$\overline{\lambda_G}$, assigning to Proponent the moves of theOpponent in $G$ and conversely, is essential to the definition of agame $G \multimap H$:

Definition 3.3. Given any pair of games $G,H$, thegame $G \multimap H$ has moves $M_{G \multimap H}$ the disjointunion $M_G + M_H$ of the games $G$ and $H$, where \[\lambda_{G \multimap H} (m) = \begin{cases} \overline{\lambda_{G}} (m) = &\text{if $m \in M_G$,}\\ \lambda_{H} (m) = &\text{if $m \in M_H$.} \end{cases}\]and a position in $P_{G \multimap H}$ is any alternating sequence$s$ of moves (of $M_{G \multimap H}$) whose restrictions $s\upharpoonright M_G,s \upharpoonright M_H$ to the moves in $G$ and$H$, respectively, are positions of $G$ and $H$.

The strategy that interprets $\texttt{succ}:\texttt{num}\to\texttt{num}$ corresponds to the behavior of the module $S$ usedabove as a guiding example. The parallel composition + hiding approachused to compose two instances of the successor module can now bereinterpreted as composition of strategies, suggesting a generalpattern:

\[\begin{array}{ccc|c|cccc|c} G_\texttt{num}& \multimap &G_\texttt{num}&& & G_\texttt{num}& \multimap &G_\texttt{num}& \\ \hline & & && & & &\mathbf{?}_\textrm{in} & O\\ & &\mathbf{?}_\textrm{in}'&O& &\mathbf{?}_\textrm{out} && &P\\\mathbf{?}_\textrm{out}'& & &P& & & &&O\\ \vdots& & & \vdots && & &&\vdots \\ n_\textrm{in}'& & &O& & & && P\\ & & n+1_\textrm{out}' &P&&n+1_\textrm{in}& & &O \\ & & &O&& & &n+2_\textrm{out} &P \end{array}\]

Definition 3.4. The composition $\tau \circ \sigma$on $G \multimap K$ of strategies $\sigma$ on $G \multimap H$ and$\tau$ on $H \multimap K$ consists of the sequences of moves of$M_G + M_K$ obtained by hiding the moves of $M_H$ from thesequences $s$ of moves in $M_G + M_H + M_K$ such that $s\upharpoonright G,H$ is in $P_{G \multimap H}$ and $s\upharpoonright H,K$ is in $P_{H \multimap K}$.

There is one strategy that deserves a special name, because it is theidentity morphism in the category whose objects are games and whosemorphisms from $G$ to $H$ are the strategies on $G \multimap H$.Thecopy-cat strategy $\textsf{id}$ on $G \multimap G$ isdefined as the set of sequences of moves $s$ such that therestriction of $s$ to the left instance of $G$ coincides with itsrestriction to the right instance.

3.4 Special kinds of strategies

The game formalism just introduced is not detailed enough tocharacterize the kind of sequential computation at higher types neededto achieve definability. For this purpose, a richer structure on gamesis needed, making them closer todialogue games betweenProponent and Opponent exchangingquestions andanswers. This allows to formulate restrictions on plays bymatching answers with the corresponding questions in an appropriatemanner. The strategies for this refined game notion, that we studynext essentially through examples, will yield a richer notion ofmorphism between games, allowing to make finer distinctions of acomputational nature needed for intensionally fully abstract model ofPCF, following essentially the approach of Hyland & Ong (2000)drawing also material from Abramsky & McCusker (1999) and Curien(2006).

The moves of the refined game notion will be eitherquestionsoranswers played by Proponent or by the Opponent. We havethen four classes of moves each represented by a kind of (round orsquare) bracket: Proponent’s questions ‘(’;Opponent’s answers ‘)’; Opponent’s questions‘[’; and Proponent’s answer ‘]’. Thislabeling of the moves subsumes under the usual well-formednesscriterion for bracket sequences, at one time: the alternation betweenProponent and Opponent, the fact that Opponent is the first to moveand that each answer of a player answers a unique question of thepartner. This is not enough, however: a furtherjustificationstructure on questions and answers is needed to discipline the nestingof (sub)dialogues in the evaluation of higher-order functions,allowing to characterize thewell-bracketed strategies.Consider now the strategy in $(G^{11}_\texttt{bool}\toG^{12}_\texttt{bool}\to G^1_\texttt{bool}) \to G_\texttt{bool}$,described informally using a labeling of the copies of$G_\texttt{bool}$ as shown:

(1)Opponent asksquestion $?$ in $G_\texttt{bool}$;
(2)Proponent asksquestion $?_1$ in $G^1_\texttt{bool}$, justified by $?$, inorder to know about the output of the input value $f$;
(3.1)if Opponent asksquestion $?_{11}$, Proponent answers ${\textit{tt}}$ in$G_\texttt{bool}$: the computation examines first the first argumentof $f$;
(3.2)if Opponent asksquestion $?_{12}$, Proponent answers ${\textit{ff}}$ in$G_\texttt{bool}$: the computation examines first the secondargument of $f$;

Here, the Proponent’s moves at steps (3.$i$) answer thequestion asked by Opponent at step (1), not the questions asked by theOpponent at steps (3.1), (3.2) that are still pending. This violates a“no dangling question mark” condition on dialoguesintroduced under this name by Robin Gandy in his unpublished work onhigher-type computability (and well-known in the tradition of gamesemantics for intuitionistic logic initiated by Lorenzen (1961)).Strategies such as these interpret control operators that do not existin the fully abstract game model of PCF, but do exist, for example, inthe model based on sequential algorithms (Curien 1986: sec. 3.2.7,3.2.8). A different phenomenon occurs in a variation of the previousexample:

(1)Opponent asksquestion $?$ in $G_\texttt{bool}$;
(2)Proponent asksquestion $?_1$ in $G^1_\texttt{bool}$;
(3.1) ifOpponent asks question $?_{11}$,Proponent answers ${\textit{tt}}$ in$G^{11}_\texttt{bool}$;
(3.1.1) ifOpponent answers ${\textit{tt}}$ in$G^1_\texttt{bool}$, Proponent answers ${\textit{tt}}$ in$G_\texttt{bool}$;
(3.2) ifOpponent answers ${\textit{tt}}$ in$G^1_\texttt{bool}$, Proponent answers ${\textit{ff}}$ in$G_\texttt{bool}$

Here the strategy prescribes a response to the moves by Opponentdepending on the internal detail of the latter’s behavior. Theresponse prescribed to Proponent by the strategy to the initialquestion should not depend on what happens between theProponent’s question $?_1$ and the Opponent’s answer${\textit{tt}}$. This is the property ofinnocence, thatlimits the amount of detail that a strategy for $P$ can access. Forthis reason, failure of innocence allows strategies to model storagephenomena.

This gives us the necessary terminology to understand the statement ofthe intensional full abstraction theorem proved in Hyland & Ong2000 (th. 7.1), where the types of PCF are interpreted as gamesand terms as innocent and well-bracketed strategies, see also Abramskyet al. 2000 (th. 3.2), Curien 2006 (th. 5.1):

Theorem 3.1. For every PCF type $\sigma = \sigma_1\to \cdots \to \sigma_n \to \kappa$ with $\kappa = \texttt{num}$ or$\kappa = \texttt{bool}$, every (compact) innocent andwell-bracketed strategy corresponds to the denotation of a closedterm.

This closes our quick overview of game semantics applied to the fullabstraction problem for PCF, but opens a broad research area in theclassification of programming disciplines according to the possiblecombinations of restrictions (innocence, well-bracketing) on generalstrategies for games as defined above. An introductory picture (the“semantic square” by Abramsky and his students) of thislandscape, that we leave to the contemplation of the reader, can befound in Abramsky & McCusker 1999.

3.5 Historical notes and further readings

Games as a semantic framework have a longstanding tradition, fromancient logic onwards. Here we list of the main sources and furtherreadings pertaining to game semantics applied to programminglanguages.

The use of game semantic for dealing with the full abstraction problemfor PCF originates from Abramsky et al. 2000 and Hyland & Ong2000. Hanno Nickau (1994) proposed independently a game model similarto that of Hyland and Ong: their games are sometimes calledcollectively “H₂O games”.

As a background for game semantics, from intuitionistic logic we havethe very early Lorenzen (1961) on dialogue games, then from linearlogic Lafont and Streicher (1991) and Blass (1992) and fromCoquand’s game theoretical analysis of classical provability(Coquand 1995). From combinatorial game theory the categorical accountby Joyal (1977), “the first person to make a category of gamesand winning strategies” according to Abramsky & Jagadeesan(1994). A readable historical account of the first uses of games inthe interpretation of constructive logical formalisms, especiallylinear logic, is included in Abramsky & Jagadeesan 1994. It shouldbe observed that games for logic require winning strategies in orderto capture validity, an issue that we have not dealt with at all inthis entry.

Connections with concrete data structures were first noticed byLamarche (1992) and Curien (1994), see Curien 2003b. AntonioBucciarelli (1994) explains the connections between Kleene’sunimonotone functions and concrete data structures: the use ofdialogues in the former is mentioned in Hyland & Ong 2000 (sec.1.4).

Finally, among the introductions to game semantics for PCF and otherlanguages, we suggest Abramsky 1997; Abramsky & McCusker 1999. Thelatter also contains a description of the applications of gamesemantics to imperative languages, notably Idealized Algol. Otherexcellent introductions to game semantics are Hyland 1997 and Curien2006. A broad account of the use of games in the semantics ofprogramming languages with many pointers to Lorenzen games, andintended for a philosophical audience, is Jürjens 2002.

Bibliography

Abramsky, Samson, 1994, “Interaction Categories andCommunicating Sequential Processes”, in A. William Roscoe (ed.),A Classical Mind: Essays in Honour of C.A.R. Hoare, New York:Prentice Hall International, pp. 1–16.
–––, 1996, “Retracing Some Paths inProcess Algebra”, in U. Montanari & V. Sassone (eds.),CONCUR ’96: Concurrency Theory, 7th InternationalConference, Springer-Verlag, pp. 1–17. [Abramsky 1996 available online]
–––, 1997, “Semantics of Interaction: AnIntroduction to Game Semantics”, in P. Dybjer & A. Pitts(eds.),Proceedings of the 1996 CLiCS Summer School, Isaac NewtonInstitute, Cambridge University Press, pp. 1–31. [Abramsky 1997 available online]
–––, 2000, “Axioms for Definability andFull Completeness”, in G.D. Plotkin, C. Stirling, & M. Tofte(eds.),Proof, Language, and Interaction, Essays in Honour ofRobin Milner, The MIT Press, pp. 55–76. [Abramsky 2000 available online]
Abramsky, Samson & Radha Jagadeesan, 1994, “Games andFull Completeness for Multiplicative Linear Logic”,Journalof Symbolic Logic, 59: 543–574. [Abramsky and Jagadeesan 1994 available online]
Abramsky, Samson & Guy McCusker, 1999, “GameSemantics”, in H. Schwichtenberg & U. Berger (eds.),Computational Logic: Proceedings of the 1997 Marktoberdorf SummerSchool, Berlin: Springer-Verlag, pp. 1–56.
Abramsky, Samson, Radha Jagadeesan, & Pasquale Malacaria,2000, “Full Abstraction for PCF”,Information andComputation, 163(2): 409–470. [Abramsky, Jagadeesan, & Malacaria 2000 available online
Amadio, Roberto M. & Pierre-Louis Curien, 1998,Domainsand Lambda-Calculi (Cambridge Tracts in Theoretical ComputerScience, 46), Cambridge: Cambridge University Press.
Barendregt, Henk P., 1984,The Lambda Calculus, Its Syntax andSemantics, Amsterdam: North-Holland Co.
Barendregt, Henk P., Wil Dekkers, & Richard Statman, 2013,Lambda Calculus with Types (Perspectives in Logic),Cambridge: Cambridge University Press/Association for SymbolicLogic.
Berry, Gérard, 1976, “Bottom-Up Computation ofRecursive Programs”,RAIRO Informatique Théorique etApplications, 10: 47–82. [Berry 1976 available online]
–––, 1978, “Stable Models of Typed$\lambda$-Calculi”, in Giorgio Ausiello & CorradoBöhm (eds.),Automata, Languages and Programming, FifthColloquium (Lecture Notes in Computer Science, 62), Berlin:Springer-Verlag, pp. 72–89. doi:10.1007/3-540-08860-1_7
Berry, Gérard, Pierre-Louis Curien, & Jean-JacquesLévy, 1985, “ Full Abstraction for Sequential Languages:the State of the Art”, Maurice Nivat & John C. Reynolds(eds.),Algebraic Methods in Semantics, Cambridge: CambridgeUniversity Press, pp. 89–131. [Berry, Curien, & Lévy 1985 available online
Blass, Andreas, 1992, “A Game Semantics for LinearLogic”,Annals of Pure and Applied Logic,56(1–3): 183–220. doi:10.1016/0168-0072(92)90073-9
Bucciarelli, Antonio, 1994, “Another Approach toSequentiality: Kleene’s Unimonotone Functions”, in StephenD. Brookes, Michael G. Main, Austin Melton, Michael W. Mislove, &David A. Schmidt (eds.),Mathematical Foundations of ProgrammingSemantics, Proceedings of the 9th International Conference, NewOrleans, LA, USA, April 7–10, 1993, (Lecture Notes inComputer Science, 802), Berlin: Springer, pp. 333–358.doi:10.1007/3-540-58027-1_17
Bucciarelli, Antonio & Thomas Ehrhard, 1994,“Sequentiality in An Extensional Framework”,Information and Computation, 110(2): 265–296.doi:10.1006/inco.1994.1033
Cardone, Felice & J. Roger Hindley, 2009, “History ofLambda-Calculus and Combinators in the 20th Century”, in Dov M.Gabbay & John Woods (eds.),Handbook of the History of Logic.Volume 5. Logic from Russell to Church, Amsterdam: Elsevier, pp.723–817.
Cartwright, Robert, Pierre-Louis Curien, & Matthias Felleisen,1994, “Fully Abstract Semantics for Observably SequentialLanguages”,Information and Computation, 111(2):297–401. doi:10.1006/inco.1994.1047
Coquand, Thierry, 1995, “A Semantics of Evidence forClassical Arithmetic”,Journal of Symbolic Logic,60(1): 325–337. doi:10.2307/2275524
Curien, Pierre-Louis, 1986,Categorical Combinators,Sequential Algorithms and Functional Programming, London: Pitman;New York: Wiley.
–––, 1992, “Sequentiality and FullAbstraction”, in Fourman, Johnstone, & Pitts 1992:66–94. doi:10.1017/CBO9780511525902.005
–––, 1994, “On the Symmetry ofSequentiality”, in Stephen Brookes, Michael Main, Austin Melton,Michael Mislove, & David Schmidt (eds.),MathematicalFoundations of Programming Semantics, 9th InternationalConference (Lecture Notes in Computer Science, 802), Berlin:Springer-Verlag, pp. 29–71. doi:10.1007/3-540-58027-1_2
–––, 2003a, “Symmetry and Interactivity inProgramming”,Bulletin of Symbolic Logic, 9(2):169–180. [Curien 2003a available online]
–––, 2003b, “Playful, StreamlikeComputation”, in Guo-Qiang Zhang, J. Lawson, Ying Ming Liu, M.K.Luo (eds.),Domain Theory, Logic and Computation, Proceedings ofthe 2nd International Symposium on Domain Theory, Sichuan, China,October 2001 (Semantic Structures in Computation, 3), Dordrecht:Springer Netherlands, pp. 1–24. doi:10.1007/978-94-017-1291-0_1 [Curien 2003b available online]
–––, 2007, “Definability and FullAbstraction”,Electronic Notes in Theoretical ComputerScience, 172(1): 301–310.doi:10.1016/j.entcs.2007.02.011
Fourman, M.P., P.T. Johnstone, & A.M. Pitts (eds.), 1992,Applications of Categories in Computer Science: Proceedings of theLondon Mathematical Society Symposium, Durham 1991 (LondonMathematical Society Lecture Note Series, 177), Cambridge: CambridgeUniversity Press.
Girard, Jean-Yves, 1987, “Linear logic”,Theoretical Computer Science, 50(1): 1–102.doi:10.1016/0304-3975(87)90045-4
Gunter, Carl A., 1992,Semantics of Programming Languages.Structures and Techniques, Cambridge, MA: MIT Press.
Hoare, C.A.R., 1985,Communicating Sequential Processes,Englewood Cliffs, NJ: Prentice-Hall.
Hodges, Wilfrid, 2001, “Formal Features ofCompositionality”,Journal of Logic, Language andInformation, 10(1): 7–28. doi:10.1023/A:1026502210492
Hyland, J. Martin E., 1997, “Game Semantics”, in P.Dybjer & A. Pitts (eds.),Proceedings of the 1996 CLiCS SummerSchool, Isaac Newton Institute, Cambridge: Cambridge UniversityPress, pp. 131–184.
Hyland, J.M.E. & C.-H.L. Ong, 2000, “On Full Abstractionfor PCF: I., Models, Observables and the Full Abstraction Problem, II.Dialogue Games and Innocent Strategies, III. a Fully Abstract andUniversal Game Model”,Information and Computation,163(2): 285–408. doi:10.1006/inco.2000.2917
Janssen, Theo M.V., 2001, “Frege, Contextuality andCompositionality”,Journal of Logic, Language andInformation, 10(1): 115–136.doi:10.1023/A:1026542332224
Joyal, André, 1977, “Remarques sur la Théoriedes Jeux à Deux Personnes”,Gazette des SciencesMathématiques du Quebec, 1(4): 46–52.
Jung, Achim & Allen Stoughton, 1993, “Studying the FullyAbstract Model of PCF Within Its Continuous Function Model”, inMarc Bezem & Jjan Friso Groote (eds.),Typed Lambda Calculiand Applications, Proceedings of the International Conference on TypedLambda Calculi and Applications, TLCA ’93, Utrecht, theNetherlands, March 16–18, 1993, (Lecture Notes on ComputerScience, 664), Berlin: Springer-Verlag, pp. 230–244.doi:10.1007/BFb0037109
Jürjens, Jan, 2002, “Games in the Semantics ofProgramming Languages—An Elementary Introduction”,Synthese, 133(1–2): 131–158.doi:10.1023/A:1020883810034
Kahn, G. & G.D. Plotkin, 1993, “Concrete Domains”,Theoretical Computer Science, 121(1–2): 187–277.doi:10.1016/0304-3975(93)90090-G
Kleene, Stephen Cole, 1952,Introduction toMetamathematics, New York: Van Nostrand.
Lafont, Yves & Thomas Streicher, 1991, “Games Semanticsfor Linear Logic”, inProceedings Sixth Annual IEEESymposium on Logic in Computer Science, IEEE Computer Society,Los Alamitos, CA, pp. 43–50. doi:10.1109/LICS.1991.151629
Loader, Ralph, 2001, “Finitary PCF is Not Decidable”,Theoretical Computer Science, 266(1–2): 341–364.doi:10.1016/S0304-3975(00)00194-8
Longley, John, 2001, “Notions of Computability at HigherTypes, I”, in René Cori, Alexander Razborov, StevoTodorcevic, & Carol Wood (eds.),Logic Colloquium 2000(Lecture Notes in Logic, 19), Wellesley, MA: A.K. Peters, pp.32–142. [Longley 2001 available online]
Longley, John & Dag Normann, 2015,Higher-OrderComputability, Heidelberg: Springer.
Lorenzen, P., 1961, “Ein DialogischesKonstructivitätskriterium”, inInfinitistic Methods,Proceedings of the Symposium on Foundations of Mathematics (1959 :Warsaw, Poland), New York: Pergamon Press, pp.193–200.
Milner, Robin, 1973,Models for LCF, Technical report,STAN-CS-73-332, Computer Science Department, Stanford University. [Milner 1973 available online]
–––, 1975, “Processes: a MathematicalModel of Computing Agents”, in H.E. Rose & J.C. Shepherdson(eds.),Logic Colloquium ’73 (Studies in the Logic andthe Foundations of Mathematics, 80), Amsterdam: North-Holland, pp.157–174. doi:10.1016/S0049-237X(08)71948-7
–––, 1977, “Fully Abstract Models of Typed$\lambda$-Calculi”,Theoretical Computer Science, 4:1–22. doi:10.1016/0304-3975(77)90053-6
–––, 1980,A Calculus of CommunicatingSystems (Lecture Notes in Computer Science, 92), Berlin, NewYork: Springer-Verlag. doi:10.1007/3-540-10235-3
Mitchell, John C., 1993, “On Abstraction and the ExpressivePower of Programming Languages”,Science of ComputerProgramming, 21(2): 141–163.doi:10.1016/0167-6423(93)90004-9
Mulmuley, Ketan, 1987,Full Abstraction and SemanticEquivalence, Cambridge, MA: MIT Press.
Nickau, Hanno, 1994, “Hereditarily SequentialFunctionals”, in Anil Nerode & Yu V. Matiyasevich (eds.),Logical Foundations of Computer Science: Proceedings of the ThirdInternational Symposium, LFCS 1994 St. Petersburg, Russia, July11–14, 1994 (Lecture Notes in Computer Science, 813),Berlin: Springer-Verlag, pp. 253–264.doi:10.1007/3-540-58140-5_25
Ong, C.-H.L., 1995, “Correspondence Between Operational andDenotational Semantics”, in Samson Abramsky, Dov M. Gabbay,& T.S.E. Maibaum (eds.),Handbook of Logic in ComputerScience, vol. 4, Oxford: Oxford University Press, pp.269–356.
O’Hearn, Peter W. & Jon G. Riecke, 1995, “KripkeLogical Relations and PCF”,Information andComputation, 120(1): 107–116.doi:10.1006/inco.1995.1103
Paolini, Luca, 2006, “A Stable Programming Language”,Information and Computation, 204(3): 339–375.doi:10.1016/j.ic.2005.11.002
Plotkin, G.D., 1977, “LCF Considered as a ProgrammingLanguage”,Theoretical Computer Science, 5(3):223–257. doi:10.1016/0304-3975(77)90044-5
Reynolds, John C., 1981, “The Essence of Algol”, inJ.W. de Bakker & J.C. van Vliet (eds.),Algorithmic Languages:Proceedings of the International Symposium on AlgorithmicLanguages, Amsterdam: North Holland, pp. 345–372.
Riecke, Jon G., 1993, “Fully Abstract Translations BetweenFunctional Languages”,Mathematical Structures in ComputerScience, 3(4): 387–415. doi:10.1017/S0960129500000293
Sazonov, Vladimir Yu., 1975, “Sequentially and ParallellyComputable Functionals”, in Corrado Böhm (ed.),$\lambda$-Calculus and Computer Science Theory, Proceedings ofthe Symposium Held in Rome, March 25–27, 1975 (LectureNotes in Computer Science, 37), Berlin: Springer-Verlag, pp.312–318.
–––, 1976, “Degrees of Parallelism inComputations”, in A.W. Mazurkiewicz (ed.),MathematicalFoundations of Computer Science 1976, Proceedings of the 5thSymposium, Gdansk, Poland, September 6–10, 1976, (LectureNotes in Computer Science, 45), New York: Springer, pp.517–523.
–––, 2007, “Inductive Definition andDomain Theoretic Properties of Fully Abstract Models for PCF andPCF+”,Logical Methods in Computer Science, 3(3): paper7. doi:10.2168/LMCS-3(3:7)2007
Scott, Dana S., 1969, “A Type-Theoretical Alternative toISWIM, CUCH, OWHY”, Informally distributed. Revised and printed1993,Theoretical Computer Science, 121: 411–440.doi:10.1016/0304-3975(93)90095-B
–––, 1970, “Outline of a MathematicalTheory of Computation”, inProceedings of the Fourth AnnualPrinceton Conference on Information Sciences and Systems, Dept.of Electrical Engineering, Princeton University, pp. 169–176. [Scott 1970 available online]
–––, 1982, “Domains for DenotationalSemantics”, in M. Nielsen & E. Schmidt (eds.),Automata,Languages and Programming, Ninth International Colloquium(Lecture Notes in Computer Science, 140), Berlin: Springer-Verlag, pp.577–613. doi:10.1007/BFb0012801
Scott, Dana S. & Christopher Strachey, 1971, “Toward aMathematical Semantics for Computer Languages”, in Jerome Fox(ed.),Proceedings of the Symposium on Computers and Automata Heldin New York, 13–15 April 1971, New York: PolytechnicInstitute of Brooklyn Press, pp. 19–46. [Scott and Strachey 1971 available online]
Sieber, Kurt, 1992, “Reasoning About Sequential Functionsvia Logical Relations”, in Fourman, Johnstone, & Pitts 1992:258–269. doi:10.1017/CBO9780511525902.015
Stoughton, Allen, 1988,Fully Abstract Models of ProgrammingLanguages, London: Pitman; New York: Wiley.
Stoy, Joseph E., 1977,Denotational Semantics: theScott-Strachey Approach to Programming Language Theory,Cambridge, MA: MIT Press.
Strachey, Christopher, 1966, “Towards a FormalSemantics”, in Thomas B. Steel, Jr. (ed.),Formal LanguageDescription Languages for Computer Programming, Amsterdam:North-Holland, pp. 198–220.
–––, 1967, “Fundamental Concepts inProgramming Languages”, International Summer School in ComputerProgramming, Copenhagen. Revised and reprinted 2000,Higher-Orderand Symbolic Computation, 13(1–2): 11–49.doi:10.1023/A:1010000313106
Streicher, Thomas, 2006,Domain-Theoretic Foundations ofFunctional Programming, Singapore: World Scientific.
Szabó, Zoltán Gendler, 2013,“Compositionality”, in Edward N. Zalta (ed.),TheStanford Encyclopedia of Philosophy (Fall 2013.). URL = <https://plato.stanford.edu/archives/fall2013/entries/compositionality/>
Turner, Raymond, 2016, “The Philosophy of ComputerScience”, in Edward N. Zalta (ed.),The StanfordEncyclopedia of Philosophy (Spring 2016.). URL = <https://plato.stanford.edu/archives/spr2016/entries/computer-science/>
Vuillemin, Jean, 1974, “Correct and Optimal Implementationsof Recursion in a Simple Programming Language”,Journal ofComputer and System Science, 9(3): 332–354.doi:10.1016/S0022-0000(74)80048-6
White, Graham, 2004, “The Philosophy of ComputerLanguages”, in Luciano Floridi (ed.),The Blackwell Guide tothe Philosophy of Computing and Information, Malden, MA:Blackwell, pp. 237–247. doi:10.1002/9780470757017.ch18

Academic Tools

How to cite this entry.
Preview the PDF version of this entry at theFriends of the SEP Society.
Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

Curien, Pierre-Louis, 2006, “Notes on Game Semantics”, course notes
Lamarche, François, 1992, “Sequentiality, Games and Linear Logic”, from a lecture to the CLiCS Symposium Aarhus University, March23–27, 1992.
Plotkin, Gordon, 1978, “The Category of Complete PartialOrders: a Tool for Making Meanings”, Lectures, summer school,Dipartimento di Informatica, Università di Pisa, Italy.Reprinted inDomains (1983)
Translation of Joyal, André (1977) “Remarks on the Theory of Two-Player Games,” translated by Robin Houston, see theposted note about this translation.

Acknowledgments

I am grateful to Ray Turner for advice and encouragement, and to LucaPaolini for comments on an early draft of this entry.

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free

Browse

About

Support SEP

Mirror Sites

View this site from another server:

USA (Main Site)Philosophy, Stanford University

Info about mirror sites

Library of Congress Catalog Data: ISSN 1095-5054

Movatterモバイル変換