Abstract
In game semantics, one expresses the higher-order value passing mechanisms of the λ-calculus as sequences of atomic actions exchanged by a Player and its Opponent in the course of time. This is reminiscent of trace semantics in concurrency theory, in which a process is identified to the sequences of requests it generates. We take as working hypothesis that game semantics is, indeed, the trace semantics of the λ-calculus. This brings us to a notion of asynchronous game, inspired by Mazurkiewicz traces, which generalizes the usual notion of arena game. We then extract the true concurrency semantics of λ-terms from their interleaving semantics formulated as innocent strategies. This reveals that innocent strategies are positional strategies regulated by forward and backward interactive confluence properties. We conclude by defining a non uniform variant of the λ-calculus, whose game semantics is formulated as a trace semantics.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions (1997)
Abramsky, S.: Sequentiality vs. concurrency in games and logic. Report Research Report RR-01-08, Oxford University, Programming Research Group (April 2001)
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation 163(2), 409–470 (2000)
Abramsky, S., McCusker, G.: Game Semantics. Springer, Heidelberg (1999)
Abramsky, S., Melliès, P.-A.: Concurrent games and full completeness. In: Logic in Computer Science 1999, Trento, July 1999, pp. 431–442. IEEE Computer Society Press, Los Alamitos (1999)
Baillot, P., Danos, V., Ehrhard, T., Regnier, L.: Timeless games. In: Nielsen, M., Thomas, W. (eds.) CSL 1997. LNCS, vol. 1414, pp. 56–77. Springer, Heidelberg (1998)
Danos, V., Herbelin, H., Regnier, L.: Games semantics and abstract machines. In: Proceedings of the 11th Symposium on Logic in Computer Science, New Brunswick, pp. 394–405. IEEE Computer Society Press, Los Alamitos (1996)
Ehrhard, T.: Hypercoherences: a strongly stable model of linear logic. Mathematical Structures in Computer Science 3(4), 365–385 (1993)
Ehrhard, T.: A relative definability result for strongly stable functions and some corollaries. Information and Computation (1997)
Goubault, E.: Geometry and concurrency: A user’s guide. Mathematical Structures in Computer Science 10(4) (August 2000)
Harmer, R.: Games and full abstraction for nondeterministic languages. Phd thesis, University of London (2000)
Hyland, M.: Game Semantics, Publications of the Newton Institute. Cambridge University Press, Cambridge (1997)
Hyland, M., Ong, L.: On full abstraction for PCF: I, II and III. Information and Computation 163(2), 285–408 (2000)
Kuske, D.: Non deterministic automata with concurrency relations and domains. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, Springer, Heidelberg (1994)
Hyland, M., Schalk, A.: Games on graphs and sequentially realizable functionals. In: Logic in Computer Science 2002, Kopenhavn, July 2002, pp. 257–264. IEEE Computer Society Press, Los Alamitos (2002)
Laird, J.: Full abstraction for functional languages with control. In: Logic in Computer Science, pp. 58–67 (1997)
Laurent, O.: Polarized games (extended abstract). In: Proceedings of the seventeenth annual symposium on Logic In Computer Science, Copenhagen, July 2002, pp. 265–274. IEEE Computer Society Press, Los Alamitos (2002)
Mazurkiewicz, A.: Concurrent program schemes and their interpretations. Technical Report DAIMI PB 78, Aarhus University (1977)
Mazurkiewicz, A.: The book of traces, chapter Introduction to trace theory. World Scientific Publishing, Singapore (1995)
Melliès, P.-A.: Axiomatic rewriting 4: a stability theorem in rewriting theory. In: Logic in Computer Science 1998, July 1998, IEEE Computer Society Press, Los Alamitos (1998)
Melliès, P.-A.: Asynchronous games 1: a group-theoretic formulation of uniformity. Prépublication électronique PPS//04/06//n°31 (pp), Equipe Preuves, Programmes et Systèmes (April 2003)
Melliès, P.-A.: Sequential algorithms and strongly stable functions. Prépublication électronique PPS//03/09//n°23 (pp), Equipe Preuves, Programmes et Systèmes, The special issue ”Game Theory Meets Theoretical Computer Science” of Theoretical Computer Science (April 2003) (to appear)
Milner, R.: Fully abstract models of typed lambda-calculi. Theoretical Computer Science 4, 1–22 (1977)
Nickau, H.: Hereditarily sequential functionals. In: Matiyasevich, Y.V., Nerode, A. (eds.) LFCS 1994. LNCS, vol. 813, pp. 253–264. Springer, Heidelberg (1994)
Stark, E.W., Panangaden, P., Shanbhogue, V.: Stability and sequentiality in data flow networks. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 253–264. Springer, Heidelberg (1990)
Pratt, V.: Modeling concurrency with geometry. In: Proceedings of the eighteenth annual symposium on Principles Of Programming Languages, January 1991, pp. 311–322. IEEE Computer Society Press, Los Alamitos (1991)
Winskel, G., Nielsen, M.: Models for concurrency. In: Abramsky, S., Gabbay, D., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 4. Oxford University Press, Oxford (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Melliès, PA. (2004). Asynchronous Games 2: The True Concurrency of Innocence. In: Gardner, P., Yoshida, N. (eds) CONCUR 2004 - Concurrency Theory. CONCUR 2004. Lecture Notes in Computer Science, vol 3170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-28644-8_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-28644-8_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22940-7
Online ISBN: 978-3-540-28644-8
eBook Packages: Springer Book Archive