Full Abstraction for Functional Languages with Control
James Laird LFCS, Department of Computer Science University of Edinburgh
This paper considers the consequences of relaxing the bracketing condition on ‘dialogue games’, showing that this leads to a category of games which can be ‘factorized’ into a well-bracketed substructure, and a set of classically typed morphisms. These are shown to be sound denotations for control operators, allowing the factorization to be used to extend the de?nability result for PCF to one for PCF with control operators at atomic types. Thus we de?ne a fully abstract and effectively presentable model of a functional language with non-local control as part of a modular approach to modelling non-functional features using games.
tial computation, as well as a toy ‘functional language with control’. The extent to which control operators alter the sorts of programs which can be written is underlined by their types, which are derivable in classical but not intuitionistic logic. This extension to the Curry-Howard correspondence between proofs and programs has been formalised elsewhere , ; here it suggests that the same basic games model will give a semantics to PCF with a simple escape mechanism, (which can be extended to the higher order control operators) and to proofs of classical logic. The fact that features of classical reasoning can be identi?ed in games, and are the same elements which model jumps in the ?ow of control also gives a way of understanding the computational content of classical reasoning: a similar distinction is used in  to extend a games semantics for intuitionistic arithmetic to the classical case by allowing backtracking. The prototypical language PCF has provided a framework in which to study the essential features of functional languages. So a reasonable place to examine the functional/non-functional boundary is in a version of PCF incremented with a simple non-functional feature. The power of game semantics to describe the intensional features of functional languages and calculi has already been established in providing a fully abstract semantics for PCF. Full abstraction provides a formal test of the level of detail at which a semantics describes the dynamics of a language. But the de?nition of a semantics which passes this formal test is necessarily preceded by a detailed intuitive correspondence between aspects of functional behaviour and the conditions imposed upon games to model it. This correspondence can be exploited when adding non-functional features to PCF by relaxing precisely the restrictions which exclude this behaviour to get a fully abstract semantics. It can also be formalized, as a ‘factorization’ of the denotations in the model as the composition of a morphism from the PCF model and one from a restricted set with essentially nonfunctional behaviour. Provided these are de?nable (they are the denotations of appropriately typed control operators), a full abstraction theorem for the extended model is a simple consequence of the PCF de?nability of its functional sub1
The simultaneous elegance and inef?ciency of pure functional languages is manifest in the fact that whilst many practical languages are described as ‘functional’, they contain so-called ‘imperative features’. The object of this approach is to exploit the nice structural properties of functional programs, whilst avoiding, at least, the obvious inef?ciencies which they impose. However, the addition of imperative features is a radical alteration to the previously pure functional idiom, as an increase in expressive power testi?es. If it is to be possible to describe such a language as ‘essentially functional with imperative features’, it will be necessary to have a clear perspective on the extent of its non-functional behaviour. One way to do so is to give a semantics in which the functional and non-functional elements of the model are clearly and naturally delineated. The object of this paper is to study the effects of adding operators which give access to the ?ow of control to call-byname functional languages using games semantics. Control operators allow programs to use intensional information about their arguments, and PCF augmented with such operators is (arguably) a basis for a notion of sequen-
structure. Abramsky has suggested (by analogy with Barendegt’s -cube), that this intensional hierarchy can be seen as a ‘Games’ cube, with a category of dialogue games at each vertex, partially ordered according to the presence or absence of the three constraints which jointly give purely functional behaviour: innocence, well-bracketing and determinacy. A vertex of this cube, at which innocence is lost, allowing Idealized Algol (‘PCF with State’) to be modelled, is studied in , and the fact that a similar methodology is used there to prove full abstraction (factorization through a morphism which records a history of the play), suggests that this is a fruitful paradigm for intensional semantics. However, this is not the ?rst fully abstract semantics to be given to PCF with control operators. Before the emergence of the fully abstract games models of PCF, Cartwright, Curien and Felleisen  had used the fact that such operators allow one to distinguish between, for instance, +l and +r , to achieve this result using Sequential Algorithms. These represent morphisms intensionally as trees, with obvious parallels with various categories of games . However, it was not apparent how the Sequential Algorithms model could be restricted to re?ect pure functional behaviour, and hence yield a fully abstract model of PCF itself. Dialogue (and AJM) games represent a move towards a more detailed intensional description of computation, by incorporating a notion corresponding to stack discipline, (the bracketing condition), which can be weakened, allowing operators which pop the stack to be modelled. The possibility of mixing and matching the conditions corresponding to the non-functional features - not available in the sequential algorithms model, supports this view, and the claim that dropping the bracketing condition gives more than ‘just another fully abstract model for sPCF’. Extensions of dialogue games to model the -calculus have been considered elsewhere: Ong  adds a notion of state, whilst Herbelin  suggests the adaptation to the Hyland-Ong framework which is used here: i.e. the relaxation of the bracketing condition, although in the context of a more syntax-oriented study, in contrast to the present work which aims to place these models in context.
in , in which most of these de?nitions are more comprehensively studied. A game A is a speci?cation of a set of possible plays, i.e. sequences of moves MA , which are alternately made by Opponent and Player, and can be either questions or answers. Thus the speci?cation consists of: a labelling function A : MA ! fP; Og fQ; Ag, which indicates the nature of each move (who made it, and whether it is a question or an answer). PO and A QA denote the composition of A with the ?rst and A second projections, respectively. a pre?x-closed set of legal sequences of moves, or ‘plays’: PA MA .
a justi?cation relation; `A MA MA associating to each move a set of ‘justifying’ moves. ( ‘a justi?es b’ is denoted a ` b.) If this set is empty, then the move is initial (this fact is denoted ` a; if it is non-empty then one of the justifying moves must appear before it in any play. Justi?cation also satis?es the following properties:
– If a ` b then PO (a) = PO (b): i.e. Opponent’s moves are justi?ed by Player, and vice-versa. (Where P = O, and vice-versa.) – No move is justi?ed by an answer: If a ` b then QA (a) = Q. – Initial moves are Opponent questions: If ` a then (a) = hO; Qi.
For any play s 2 PA there is a function ( s : jsj ! N ) such that s (n) n, giving for each non-initial nth move sn of s, the index s(n) of the unique move justifying sn . As each answer is non-initial, and justi?ed by a unique question, it is reasonable to say that it answers that question. Plays are subject to these general conditions: P1 Moves are made alternately by Player and Opponent:
sab 2 PA ) QA (a) = QA (b): A A
2. Weakly bracketed games
The framework proposed here is a variant of the ‘dialogue games and innocent strategies’ setting, which gives fully abstract models of the simply-typed -calculus and PCF; namely, ‘weakly-well-bracketed’ games and innocent strategies. Hence it is easily accommodated within a setting which has been well described elsewhere, particularly
P2 Plays satisfy the ‘visibility condition’: for every non-initial move a, if sa 2 PA then the unique move in s justifying a is in the view of s (de?ned below). De?nition 2.1 (Player and Opponent views.) Notions of Player and Opponent view psq and xsy can be de?ned on any justi?ed sequence s of moves, independently of the question/answer distinction, and,
in particular, any bracketing condition :
p q= p q=p q p q= p q=p q
sm s m; if m is a P-move. sm m; if ` m. smtn s mn; if n is an O-move justi?ed by m. : sm s m; if m is an O-move. smtn s mn; if n is a P-move justi?ed by m.
x y= x y=x y x y=x y
it. Imposing the original bracketing condition corresponds to rigidly maintaining stack discipline; only the question at the top of the stack can be popped. Relaxation to the weak bracketing condition allows for the stack to be popped to an earlier point, causing every question pushed onto the stack since that point to be lost.
3. Innocent strategies
A (deterministic) strategy over a game A is a speci?cation of Player’s responses to (some of) the plays of A in which she is to move, and is therefore generally even expressed as a even-pre?x-closed subset PA , such that sa; sb 2 ) a = b. Thus a strategy is determined by a partial function from odd length sequences of moves in PA (situations with player to move) to legal moves. It is innocent if its moves are only determined by the view of the game even PA , such so far: i.e. it is a pre?x closed subset that
In the absence of an explicit bracketing condition, imposing the visibility condition entails that plays satisfy a weaker condition (provided that that answers cannot justify any moves), because all moves between a question and answer disappear from view. Lemma 2.2 The Player view of any play Player is to move is well-bracketed.
s in which
Proof: - by induction on the length of s The view of a single move is trivially well-bracketed. Suppose s = s0 mtn, where m justi?es n (as Player is to move, n is an O-move) then psmtnq = psqmn. By inductive hypothesis, psq is well-bracketed, and as m justi?es another move (n), it cannot be an answer move. However the only move which n can answer is its justifying move m, so psmtnq is also wellbracketed. Dually, unanswered questions disappear from Opponent’s view as soon as a question asked earlier is answered by either participant. Consequently the following ‘Weak Bracketing condition’ holds: – Only open questions may be answered: a question is open if it is unanswered, and no questions asked before it have been answered since it was asked:
sa; tb 2 ^ psq = ptq ) a = b:
Hence it is determined by a partial function from Player views to legal moves. The representations of a strategy as a tree and as an ‘innocent function’ will frequently be interchanged. In order to characterise the substructure of this games model which is restricted to purely functional behaviour (i.e. ‘the well-bracketed part’), it is necessary to describe the strategies which correspond to functions without control operators. These will be the strategies which do obey the last-asked-?rst-answer condition; the question is, how do these strategies correspond to strategies on well-bracketed games, given that the latter only have responses to well-bracketed plays? As views are well-bracketed, there is a simple answer. De?nition 3.1 A well-bracketed strategy is an innocent strategy which always answers the most recently asked open question, (which is always visible). A well-bracketed strategy may contain plays which are not well-bracketed, but the lemma below shows that these are just the plays which are forced to be there by innocence. Lemma 3.2 Every well-bracketed strategy corresponds to a unique strategy on well-bracketed games with the same innocent function.
smtn 2 PA ^ QA (m) = QA (n) = A ) A A smtn(n) smtn(m):
This contrasts with the ‘well-bracketing condition’ applied in , , which requires that only the most recently asked open question can be answered. In weakly bracketed games, answering a question closes all of the more recently asked questions as well. This is in accord with the intuition that we can keep track of dialogues between Player and Opponent (and hence compute the result of a composition of strategies) by keeping unanswered questions in a ‘stack’. Moves can be characterized either as the pushing of a new question onto the top of the stack, or as the popping of a question from the stack by answering
Proof: Suppose is a well-bracketed strategy. Then it is necessary to show that for every play sa 2 , there is a well-bracketed play s0 a 2 , such that psq = ps0 q. (From this fact it follows immediately that the innocent function representation of is an innocent function in the weakly bracketed setting.) Proof is by induction on the length of sa: - the base case is trivial, so we prove the inductive step. As s ends with an opponent move, psq = ptqbc, for some pre?x t of s, and moves b and c such that b justi?es c. But by inductive hypothesis, there is a well bracketed play t0 b 2 such that ptq = pt0q. Then psq = pt0bcq, and t0bc is well-bracketed, as move b is made by a wellbracketed strategy, and if c is an answer, it is justi?ed by b anyway. The functor which embeds the category of wellbracketed games in the category of weakly-bracketed games (described below) by taking the ‘innocent closure’ of each strategy is therefore faithful.
P A = fs 2 M A j if m 2 MA is initial then the subsequence of s hereditarily justi?ed by m is in PA g
` A = `A
For each object A, the identity morphism idA : A ! A is the copycat strategy, which copies Opponent moves on either side of the arrow as Player moves on the other side. Composition of morphisms is interaction of strategies: Given : A ! B and : B ! C ; = ( k )=B = fs A,C : s 2 k g, where k = fs 2 (MA + MB + MC ) js A; B 2 ^ s B; C 2 g. It is necessary to check that if and are innocent, then ; is too. The proof of this fact for wellbracketed games appears in , but carries through directly to the weakly-bracketed case. If both and are well-bracketed, then so is k , and hence also ; .
4. A symmetric monoidal closed category of games
Like well-bracketed games and innocent strategies, the non-well-bracketed games form an af?ne autonomous category G , in which the objects are games, and morphisms are strategies for the exponential. Given games A and B : the game A ( B is de?ned: – – – –
Now de?ne the cartesian closed category C of weakly bracketed games to be the the co-Kleisli construction of the comonad ! on the autonomous category G . The canonical morphisms for a CCC are then various forms of copycat strategy. De?ne an atomic game to be the game consisting of a single (Opponent) question and a set of answers, f]a : a 2 g. These correspond to the ?at domains which interpret ground types in PCF. If S is any collection of such atomic games, CS denotes the CCC of weakly bracketed games freely generated from S . For each object A 2 CS , let At(A) denote the set of atomic subgames of A. Example 4.1 (Peirce’s Law)
MA(B = MA + MB . A(B = A ; B ] PA(B = fs 2 MA(B js MA 2 PA , s MB 2 PB g. 8b 2 MB , m `A(B b iff m `B b for a initial in A, m `A(B a iff m is initial in B. 8a(non-initial)2 MA m `A(B a iff m `A a.
The game A B is de?ned as for A ( B , except that A B = A ; B ]. It has a unit, the game with no moves (which is also a terminal object as this is an af?ne category). For any strategy :A, the strategy p q : 1 ( A, the ‘name of sigma’ has the same graph as , allowing the systematic confusion between them adopted here. The game !A is de?ned: – –
(( ! ) ! ) ! (Peirce’s law), is the simplest type which can be given to control operators but not (generally) to functions; it is also the simplest example of a classical tautology which is not provable in minimal intuitionistic logic. This translates to the games semantics framework: this is the simplest construction from atomic games and upon which there is a weakly bracketed strategy, independent of and which is total (in the obvious sense), but no total well-bracketed strategy. Moreover, this strategy is (in a sense made formal by the factorization theorem) a canonical example of a non-well-bracketed strategy, and will be the denotation of the call=cc-like control operators which will be added to PCF.
M A = MA
[α (α [β [β [β [β (α
α) α) α)
simply typed -calculus as well. Individual violations of the bracketing condition can be speci?ed according to the type of the most recently asked question to be prematurely closed, and the type of the answer closing it. All such violations with respect to the types and can then be factored out by forcing Opponent to ‘pop the stack of questions’ ?rst, by shifting play to a premise of type (( ! ) ! ) ! , where Player plays as Opponent and can copy moves from the rest of the play. Composing with Peirce returns the original strategy. Thus all bracketing violations in a strategy on a game over ?nitely many atomic types can be systematically factored out. Theorem 5.1 (Factorization Theorem:) Let S be any collection of atomic games. Then for any game A 2 CS and strategy :A, there is a well-bracketed strategy,
Figure 1. Peirce
! )! )!
) ) ) ) ) ) ?! A
Peirce ); 0 = :
such that This is the strategy depicted in Figure 1. (Where square brackets denote Opponent questions and their answers, and round brackets denote Player questions and their answers.) It copies the initial -question in the second component, and copies back any answer. If none is forthcoming, it copies the -question again in response to the beta question, until it receives an -answer, which it copies as an answer to the initial question, closing the game.
Proof: For any ; 2 S , de?ne the property WB ; (wellbracketing in with respect to ) over strategies in CS : De?nition 5.2 WB ; ( ) if and only if never gives an answer of type which is not justi?ed by the last asked (open) question of type .
5. Translating to well-bracketed strategies
Factorizing weakly bracketed strategies as a composition of a well-bracketed strategy and ?nitely many of the strategies Peirce allows the de?nability results for PCF and the simply typed lambda-calculus to be extended to the weakly bracketed case by adding terms to denote Peirce (which will be control operators). This approach is similar to that of , where de?nability of non-innocent (‘knowing’) strategies is proved for a version of PCF with state, by factorizing them as the composition of an innocent strategy and a strategy with the sole function of recording a history of the play. Although the factorizations differ in that factorizing knowing strategies requires an encoding of moves to record the history of play, whereas removing violations of the bracketing condition is achieved simply by copying moves- thus it can be done in the case of the
: B is well-bracketed if and only if
8 ; 2 At(B )WB ; ( )
Thus we can get a well-bracketed strategy of the right type by factorizing through Peirce , for each pair of types ; 2 AT (A), by repeated application of the following Lemma 5.3 For any atomic types , , and weakly bracketed strategy : B , there is a strategy 0 : ((( ) ) ) ) ) ) ! B such that – – –
WB ; ( 0). Peirce ; 0 = 8 ; 2 At(B ) : WB ; ( ) ) WB ; ( 0 ).
! )! )!
[α (β [α
the premise (( ! ) ! ) ! , and each Player answer of type may be preceded by up to four moves in the premise. Corollary 5.4 If
: A is compact then so is 0 .
Proof: At(A) At(A) is ?nite, therefore the lemma need only be applied ?nitely many times, each yielding a compact strategy, to factorize .
6. Augmenting PCF with control operators
Figure 2. Elimination of a violation of the bracketing condition. Now the Factorization Theorem can be applied to prove that the games and innocent well-bracketed strategies model for call-by-name PCF extends to a fully-abstract model of PCF with control operators call=cc of type (( ! ) ! ) ! , for ; 2 fo; g by dropping the bracketing condition. However, to maintain a concise account, I will consider a version of PCF with only the ground-type , allowing call=cc to be abbreviated to call=cc. (This is described as ‘call with current downward continuation’ in , although a less expressive ‘linear’ version is de?ned there.) Hyland and Ong proved that the well-bracketed model is fully abstract with respect to a call-by-name operational semantics for PCF in terms of a Martin-L¨ f style o evaluation relation : this can be naturally extended to include call=cc using the notion of evaluation context . De?nition 6.1 (Evaluation contexts.)
– If is compact (its innocent function has a ?nite graph) then so is 0 . Proof: De?ne 0 as described by Figure 2. i.e. play as , but jump into the premise (( ! ) ! ) ! as soon as an question is asked by Opponent, and copy it as the initial question. Then jump back and play as until a point where would close a -question prematurely by answering the -question. Instead 0 returns to the premise, and copies the -question, forcing Opponent to answer a question ?rst, providing either a -answer to copy, or closing all questions back to the original question, allowing it to be answered. (The translation from to 0 can be described in a more formal but less perspicuous way by de?ning the innocent function f :)
First note that 0 is a well de?ned innocent strategy, i.e. 0 is pre?x closed, as its restrictions to the premise (( ! ) ! ) ! and to the conclusion B both are. Plays according to 0 obey the visibility condition, as if 0 is able to close an question then the play succeeding in in the premise is visible to 0 , and elsewhere 0 plays as It remains to verify the following claims: will not give an -answer when the last-asked question is of type . – Peirce ; 0 = : if Opponent plays according to Peirce in the premise (( ! ) ! ) ! , then for any s 2 0 , s B 2 is played according to the same Opponent strategy in B . – 8 ; 2 At(B ) : WB ; ( ) ) WB ; ( 0): 0 only changes the order in which answers are given in the case where the last asked question is of type , and the answer closing it is of type . – If is compact then so is 0: 0 is de?ned on the same views as , except that each visible Opponent -question is now followed by two moves in –
E ] ::= ] j E ]M j IFOE ]MN j call=cc f:E ] j constE ]
where const is any constant of PCF. Evaluation contexts serve to pick out subterms which must be evaluated in any reduction sequence for the whole term, a fact expressed by the Unique Evaluation Contexts lemma : Any application of PCF + call=cc can be uniquely represented as E t], where t is a variable or , and E ] is an evaluation context. Assuming + is the evaluation relation for PCF, extend it with the following reductions (and allowing evaluation inside a call=cc), where E ranges over applicative contexts:
WB ; (
t+n call=cc f:t + n
call=cc f:t + n call=cc f:E ft] + n
The denotational semantics for PCF given in  can be extended to PCF + call=cc using the faithful embedding of the category of well-bracketed games and innocent strategies into the category of weakly bracketed games and innocent strategies given by mapping strategies to their well-bracketed counterparts, and letting call=cc denote Peirce , which is abbreviated to Peirce. ( ] is an atomic game as required, with a single question N and the answers f]njn 2 N g, whilst n : denotes the strategy f N ]ng). Informally, it is clear that call=cc should denote the strategy Peirce, as call=cc f:M returns the ?rst argument to f that is encountered whilst evaluating M, or if f:M is non-strict, it returns the value of M . Theorem 6.2 (Adequacy) : The proposed denotational semantics is computationally adequate with respect to the operational semantics; i.e. for all closed terms s of type , s + n if and only if s] = n. Proof: C is a ‘standard model’ for PCF , (just using the well-bracketed substructure). To extend this adequacy result to PCF + call=cc, it is suf?cient to extend the reducibility style proof of the adequacy of standard models , to the interpretation of call=cc as Peirce in C : i.e. to show, in the absence of the combinator, that call=cc f:M + m , f:M ] ; Peirce = m:
(using the lemma). To establish completeness, suppose that call=cc f:M ] = n, where M is in head-normal form. As it is of ground type it must be an application or a value. Applying the Unique Evaluation Contexts Lemma, M = E t], where t = f , or t = n0 or t = , and E ] is an evaluation context. By soundness, in the ?rst two cases, t + n, whilst the latter contradicts the assumption that call=cc f:M ] = n] . The proof can be extended to PCF including the combinator, as described in , by replacing it in all terminating programs by a ?nite approximant.
Now the factorization of strategies, and the de?nability of well-bracketed strategies by PCF terms can be exploited to give an easy proof of: Theorem 6.4 (De?nability lemma:) Any compact innocent strategy : A is the denotation of a term of PCF + call/cc. Proof: By the factorization theorem, there is a well-bracketed compact strategy 0 : ((( ! ) ! ) ! ) ! A such that Peirce ; ; 0 = . By the de?nability theorem for PCF , there is a term s of PCF denoting 0, and thus the term s ( x.call/cc x) denotes . To get a fully abstract model it is now necessary to quotient by the intrinsic preorder, ., as in , . Note, however, that intrinsic equivalence is no longer extensional equivalence, as we can de?ne the strategies catchk , of  which distinguish between different sequentializations of the same function. De?nition 6.5
Lemma 6.3 (Evaluation contexts) : Let evaluation context such that
E ] be any
() 8 : A ! N ( ; = n) ) ( ; = n): A () .A ^ .A :
? ` f:E ft] : (
The strategy responds to Opponent’s initial question by asking the initial question in ! . Proof is by a structural induction over the de?nition of evaluation context. Proof of Adequacy: In the direction of soundness it is suf?cient to note that: – –
! )! : ? ` f:E ft]]] : ?]] ! ( ! ) !
The semantics of PCF + call=cc can be fully and faithfully translated to C / , which is poset-enriched by . (). De?ne the relation of observational approximation, vOBS , between type-compatible terms of PCF + call=cc thus:
svOBS t () C s] + v ) C t] + v
where C ranges over all type compatible program contexts. Then a denotational model for PCF + call=cc is fully abstract if for all type-compatible pairs of terms s, t:
call=cc f:n] = f:n] ; Peirce = n] call=cc f:E ft]]] = f:E ft]]]; Peirce = call=cc f:t] :
s] . t] () svOBS t
Theorem 6.6 (Full abstraction:) stract model for PCF + call=cc.
C /. is a
Soundness: if s 6vOBS t, then as the denotational semantics is adequate, there is some n 2 N and type-compatible context C ], such that C s] + n, but C t] 6+ n. Then if = x:C x] (where x is free in C[x]: ; s] = n, but ; t] 6= n, and hence s] 6. t] . Completeness: suppose s] 6. t] . Then there is a strategy , and number n such that s] ; = n and t] ; 6= n. As s] ; returns a result in N, the uncovering of this play with respect to s] and is ?nite, consequently, has a ?nite approximant 0 such that s] ; 0 = n and t] ; 0 6= n. By the de?nability lemma, there is a closed term r denoting 0 , thus rs] = n and rt] 6= n so (rs) + n and (rt) 6+ n by adequacy. So s 6vOBS t as required.
Proof: It is suf?cient to prove soundness and completeness for closed terms, as given any terms s and t with free variables x1 : A1 ; x2 : A2 ; :::; xn : An , then s] . t] if and only if x:s] . x:t] . Whilst svOBS t if x:svOBS x:t, as if C is any type-compatible program context, then C s] + v () D x:s] + v, where D = C[( x)].
Essentially this is because in the absence of the bracketing condition, any intensional differences between two strategies can be exposed by supplying the same inputs and making a sharp exit as soon as they make different moves provided that this does not violate innocence. De?nition 7.1 An innocent play according to an (innocent) strategy is a ?nite play s 2 such that Opponent also plays innocently: i.e. 8s0 ; t0 veven s; xs0 y = xt0y ^s0a v s =) t0a v s. Given s 2 Innocent plays( ), O ? strategy(s) is the innocent function from Opponent views to moves which is manifested in s. Proposition 7.2 For any strategies and only if
in C ,
8s 2 Innocent plays( ); 8t 2 Innocent plays( ) O ? strategy( ) O ? strategy( ) ) xsy = xt0 y for some t0 v t.
: A ! N such that ; = n and ; 6= n. Then
, i.e. there is some (innocent)
7. Effective presentability
An interesting question concerns the effective presentability of the extensionally fully abstract domain C = : The sequential algorithms model of sPCF does not require quotienting (the intensional preorder is just the subset relation on strategies) - consequently ‘the fully abstract model of sPCF’ is effectively presentable. This contrasts with the extensionally fully abstract model of PCF, which is known not to be effectively presentable, as ?nitary PCF is undecidable . Adding control operators allows intensionally distinct versions of extensionally equal functions to be distinguished - one of the reasons for introducing them in sPCF . Not all of the strategies in the games model can be distinguished (partly a consequence of the greater intensional precision with which it models the process of computation - there is no operational distinction between e.g. x:IF x = x then x else 0 : N ! N and x:x, although it is reasonable to allow them to represent different computations). However the intrinsic preorder for compact strategies is decidable, and thus the quotiented model is effectively presentable as required.
let s be the uncovering of (the sequence consisting of) N , with respect to ; , and let t be the uncovering of N , with respect to ; . Let s0 be the maximal innocent pre?x of s A such that O ? strategy(s0 ) O ? strategy(t). Then s0 ; t A are even-length innocent plays, but xs0 y 6= xt0y for any t0 v t, as Opponent plays according to in both s and t, and O ? strategy(s0 ) O ? strategy(t) and xsy 6= xty. To show the converse, suppose that there is some s 2 Innocent plays( ) and t 2 Innocent plays( ), such that O ? strategy(s) O ? strategy(t) but xsy 6= xt0 y. De?ne the following strategy on A ! N : Then is innocent, as s is an innocent play (so the last move does not violate innocence as there is no pre?x of N s with the same P-view). And ; = 0, but ; is unde?ned, so 6. . Another characterization of the intrinsic preorder is to consider it as being induced by mapping to the sequential algorithm which denotes the same term in sPCF. The intrinsic preorder on compact strategies is decidable, because we can give a bound (of 2jdom(f )j) for the length of the innocent plays which can differentiate from by the above criterion.
= Pref even( N s] g)
8. Further directions and conclusions
– The version of call=cc de?ned here at atomic types is a natural choice of control operator with which to increment PCF: it denotes the morphism used in the factorization theorem, it can be typed with PCF types, and it has no additional variable bindings to deal with. However, as noted in , adding double negation elimination, (or, equivalently Peirce’s law) at atomic types to intuitionistic natural deduction is suf?cient to derive classical laws for all arrow types. (The factorization theorem is really just a semantic version of this bit of elementary proof theory.) Moreover, the derived higher-order classical terms behave appropriately, extending Curry-Howard: the derived term of type (((A ! ?) ! ?) ! A) obeys the equalities for the operator C , for instance. This offers the possibility of using the well/weakly bracketed distinction to investigate proof theory semantically, in particular using factorizations to extract computational content from classical proofs in a more direct and ef?cient fashion than by using existing methods of double negation translation. – The construction corresponding to the factorization theorem appears to be quite general, and to have some nice properties, such as commuting with composition, posing the the question: what is its categorical characterization, and can it be expressed more generally, for instance in terms of the Geometry of Interaction? – As already noted, the Sequential Algorithms model of sPCF is isomorphic to the quotient of the dialogue games model. The requirement of innocence in the latter corresponds to the characterization of plays in the sequential data structure !A as non-repetitive sequences of plays in A. A semantic characterisation of the isomorphism would clarify this distinction between sharing and copying of information. – Control operators are better understood in the context of call-by-value languages. Games semantics for such languages are currently under investigation, and it appears that innocent, wellbracketed, strategies yield fully abstract models of purely functional languages, and that violating the bracketing condition corresponds to the use of control operators, and that such violations can be factored out, as described here. – In the call-by-name and call-by-value settings one can combine the bracketing factorization
with the factorization of knowing strategies described in  to get a de?nability result for PCF with state and control mechanisms - seemingly a foundation for a broad notion of sequential nonfunctional computation.
I am indebted to Samson Abramsky, and others in the Edinburgh interaction group, particularly Paul-Andr? e Mellies and Juliusz Chroboczek, for valuable discussions and suggestions. Graham Clark suggested many corrections to the layout and clari?cations of the language which I have adopted. Thanks are also due to Pierre-Louis Curien for a different perspective on control operators, and to suggestions made in reports on an initial version of this paper. Financial support in the form of an EPSRC studentship is also gratefully acknowledged.
 S. Abramsky and G. McCusker. Linearity Sharing and state: a fully abstract game semantics for idealized algol with active expressions (extended abstract). Elsevier Electronic notes in Theoretical Computer Science, (3), 1996.  S. Abramsky, R. Jagadeesan and P. Malacaria. Full abstraction for PCF. Submitted for publication.  G. Berry, P.-L. Curien, J.-J. L? vy. Full abstraction for e sequential languages: The state of the art. In J. Reynolds, editor, Algebraic methods in Semantics. Cambridge university press, 1985.  R. Cartwright, P.-L. Curien and M. Felleisen. Fully abstract semantics for observably sequential languages. Information and Computation, 1994.  C.Murthy. Extracting constructive content from classical proofs. PhD thesis, Cornell University, 1992.  T. Coquand. A semantics of evidence for classical arithmetic. Journal of Symbolic Logic, 1995.  P.-L. Curien. On the symmetry of sequentiality. In Mathematical Foundations of Computer Science, number 802 in LNCS. Springer, 1993.  M. Felleisen, D. P. Friedman, E. Kohlbecker and B. Duba. A syntactic theory of sequential control. In LICS 1986, pages 131 – 141. IEEE Computer Society Press, 1986.  H. Herbelin. Games and weak-head reduction for classical logic. Manuscript, 1996.  J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. to appear, 1995.  R. Loader. Finitary PCF is undecidable. Manuscript, 1996.  G. McCusker. Games and full abstraction for a functional metalanguage with recursive types. PhD thesis, Imperial College London, 1996.
 C.-H. L. Ong. A semantic view of classical proofs: type-theoretic, categorical and denotational characterizations. In LICS 96. IEEE Computer Society Press, 1996.  C.-H. L. Ong and C. A. Stewart. A Curry-Howard foundation for functional computation with control. to appear in proceedings POPL, 1997.  G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223 – 255, 1977.  D. Prawitz. Natural Deduction. Number 3 in Stockholm studies in Philosophy. Almqvist and Wiksell, 1965.