Loading...
Please wait, while we are loading the content...
Similar Documents
Dialogue Games and Innocent Strategies: An Approach to (Intensional) Full Abstraction for PCF
| Content Provider | Semantic Scholar |
|---|---|
| Author | Ong, Luke Hyland, Martin |
| Copyright Year | 1993 |
| Abstract | This note is (intended to be) released in conjunction with a preliminary announcement of Abram-sky, Jagadeesan and Malacaria entitled Games and Full Abstraction of PCF. Like Abramsky et al. (but independently), we have found an intensionally fully abstract model for pcf Plo77]. Our model is a Cartesian closed category of Scott domains all of whose compact elements are deenable in pcf. Using Stoughton's Theorem Sto88], the model can be extensionally collapsed by means of a continuous ho-momorphism to the least xpoint, order-extensional, fully abstract model which is shown to be unique by Milner Mil77]. It is unclear at this stage how our model relates to that of Abramsky et al. Our model of computation is based on a kind of game in which each play consists of a dialogue of questions and answers between two players. This approach is very concrete and in nature goes back to Kleene Kle78] and Gandy in one tradition, and to Kahn and Plotkin KP78], and Berry and Curien BC82] in another. This work has also been informed by the game semantical paradigm of AJ92]. We analyze pcf-style computations directly in terms of partial strategies based on the information available to each player when he is about to move. Hence our games are not history-sensitive; but they are not history-free either. Rather each player selects only that part of the \history" that interests him currently: he has a view of current concerns. These dialogue games have two important features: No question may be answered until all subsidiary questions are answered. This is a version of Gandy's \no dangling question marks" condition. Also our players are required to play an \innocent" strategy: they play on the basis of their current views which are continually updated as the play unfolds. They give expression to what seems to us to be the nub of pcf-style sequentiality. A simple computational arena consists of the following data: A partially order set of questions such that the upper set of each question is a nite linear order. So the questions form an upside down forest (of trees), the root of each tree being a maximal element in the ordering. An association to each question of a set of possible answers. Any such answer is said to match the question. Questions of depth 0, 2, 4, etc. are associated with Opponent (O), and those of depth 1, 3, 5, etc. are associated … |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.di.uminho.pt/ftp/pub/DI/Fundamentos/Papers/mirror-ImperialCollege/AbramskyS/clics/clics.HO.dgis.ps.gz |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
