Hostname: page-component-8448b6f56d-gtxcr Total loading time: 0 Render date: 2024-04-24T21:37:10.871Z Has data issue: false hasContentIssue false

Full abstraction for expressiveness: history, myths and facts

Published online by Cambridge University Press:  13 November 2014

DANIELE GORLA
Affiliation:
Dip. di Informatica, ‘Sapienza’ Università di Roma. Via Salaria 113, 00198 Roma, Italy Email: gorla@di.uniroma1.it
UWE NESTMANN
Affiliation:
Technische Universitat Berlin. Ernst-Reuter-Platz 7, 10587 Berlin, Germany Email: uwe.nestmann@tu-berlin.de

Abstract

What does it mean that an encoding is fully abstract? What does it not mean? In this position paper, we want to help the reader to evaluate the real benefits of using such a notion when studying the expressiveness of programming languages. Several examples and counterexamples are given. In some cases, we work at a very abstract level; in other cases, we give concrete samples taken from the field of process calculi, where the theory of expressiveness has been mostly developed in the last years.

Type
Paper
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

Supported by the Deutsche Forschungsgemeinschaft, grant NE-1505/2-1.

References

Amadio, R. M. (2000) On modelling mobility. Theoretical Computer Science 240 147176.CrossRefGoogle Scholar
Amadio, R. M., Castellani, I. and Sangiorgi, D. (1998) On bisimulations for the asynchronous pi-calculus. Theoretical Computer Science 195 (2) 291324.CrossRefGoogle Scholar
Beauxis, R., Palamidessi, C. and Valencia, F. D. (2008) On the asynchronous nature of the asynchronous pi-calculus. In: Concurrency, Graphs and Models. Springer Lecture Notes in Computer Science 5065 473492.CrossRefGoogle Scholar
Boreale, M. (1998) On the expressiveness of internal mobility in name-passing calculi. Theoreatical Computer Science 195 (2) 205226.CrossRefGoogle Scholar
Boudol, G. (1992) Asynchrony and the π-calculus (note). Rapport de Recherche 1702, INRIA Sophia-Antipolis.Google Scholar
Cacciagrano, D., Corradini, F. and Palamidessi, C. (2007) Separation of synchronous and asynchronous communication via testing. Theoretical Computer Science 386 (3) 218235.CrossRefGoogle Scholar
Carbone, M. and Maffeis, S. (2003) On the expressive power of polyadic synchronisation in π-calculus. Nordic Journal of Computing 10 (2) 7098.Google Scholar
Chandra, A. K. and Manna, Z. (1976) On the power of programming features. Computer Languages 1 (3) 219232.CrossRefGoogle Scholar
de Boer, F. S. and Palamidessi, C. (1994) Embedding as a tool for language comparison. Information and Computation 108 (1) 128157.CrossRefGoogle Scholar
De Nicola, R. and Hennessy, M. (1984) Testing equivalences for processes. Theoretical Computer Science 34 83133.CrossRefGoogle Scholar
Felleisen, M. (1991) On the expressive power of programming languages. Science of Computer Programming 17 (1–3) 3575.CrossRefGoogle Scholar
Fournet, C. and Gonthier, G. (1996) The reflexive chemical abstract machine and the join-calculus. In: Proceedings of Principles of Programming Languages (POPL), ACM 372–385.Google Scholar
Fu, Y. and Lu, H. (2010) On the expressiveness of interaction. Theoretical Computer Science 411 (11–13) 13871451.CrossRefGoogle Scholar
Gorla, D. (2008) Comparing communication primitives via their relative expressive power. Information and Computation 206 (8) 931952.CrossRefGoogle Scholar
Gorla, D. (2010a). A taxonomy of process calculi for distribution and mobility. Distributed Computing 23 (4) 273299.CrossRefGoogle Scholar
Gorla, D. (2010b) Towards a unified approach to encodability and separation results for process calculi. Information and Computation 208 (9) 10311053.CrossRefGoogle Scholar
Haagensen, B., Maffeis, S. and Phillips, I. (2008) Matching systems for concurrent calculi. In: Proceedings of International Workshop on Expressiveness of Concurrency (EXPRESS). Electronic Notes in Theoretical Computer Science 194 (2) 8599.CrossRefGoogle Scholar
Herlihy, M. (1991) Wait-free synchronization. ACM Transactions on Programming Languages and Systems 13 (1) 124149.CrossRefGoogle Scholar
Honda, K. and Tokoro, M. (1991) An object calculus for asynchronous communication. In: Proceedings of European Conference on Object-Oriented Programming (ECOOP'91). Springer Lecture Notes in Computer Science 512 133147.CrossRefGoogle Scholar
Kleene, S. C. (1952) Introduction to Metamathematics, Van Nostrand, New York.Google Scholar
Landin, P. J. (1966) The next 700 programming languages. Communications of the ACM 9 157166.CrossRefGoogle Scholar
Lipton, R. J. (1975) Reduction: A new method of proving properties of systems of processes. In: Proceedings of Principles of Programming Languages (POPL), ACM 78–86.CrossRefGoogle Scholar
Lipton, R. J., Snyder, L. and Zalcstein, Y. (1974) A comparative study of models of parallel computation. In: 15th Annual Symposium on Switching and Automata Theory, IEEE 145–155.CrossRefGoogle Scholar
Merro, M. (1998) On the expressiveness of Chi, update, and fusion calculi. In: Palamidessi, C. and Castellani, I. (eds.) Proceedings of International Workshop on Expressiveness of Concurrency (EXPRESS '98). Electronic Notes in Theoretical Computer Science 16 (2), Elsevier Science Publishers 133144.CrossRefGoogle Scholar
Merro, M. (2000) Locality and polyadicity in asynchronous name-passing calculi In: Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS). Springer Lecture Notes in Computer Science 1784 238251.CrossRefGoogle Scholar
Merro, M. and Sangiorgi, D. (2004) On asynchrony in name-passing calculi. Mathematical Structures in Computer Science 14 (5) 715767.CrossRefGoogle Scholar
Milner, R. (1989) Communication and Concurrency, Prentice Hall.Google Scholar
Milner, R. (1993) The polyadic π-calculus: A tutorial. In: Logic and Algebra of Specification, Series F: Computer and System Sciences, volume 94, Springer.Google Scholar
Milner, R. (1999) Communicating and Mobile Systems: The π-Calculus, Cambridge University Press.Google Scholar
Milner, R. and Sangiorgi, D. (1992) Barbed bisimulation In: Proceedings of International Colloquium on Automata, Languages and Programming (ICALP). Springer Lecture Notes in Computer Science 623 685695.CrossRefGoogle Scholar
Mitchell, J. (1993) On abstraction and the expressive power of programming languages. Science of Computer Programming 21 (2) 141163.CrossRefGoogle Scholar
Nestmann, U. (2006) Welcome to the jungle: A subjective guide to mobile process calculi In: Proceedings of International Conference on Concurrency Theory (CONCUR). Springer Lecture Notes in Computer Science 4137 5263.CrossRefGoogle Scholar
Nestmann, U. and Pierce, B. C. (2000) Decoding choice encodings. Information and Computation 163 (1) 159.CrossRefGoogle Scholar
Palamidessi, C. (2003) Comparing the expressive power of the synchronous and asynchronous Pi-calculi. Mathematical Structures in Computer Science 13 (5) 685719.CrossRefGoogle Scholar
Palamidessi, C., Saraswat, V. A., Valencia, F. D. and Victor, B. (2006) On the expressiveness of linearity vs persistence in the asychronous Pi-calculus. In: Proceedings of Logic in Computer Science (LICS), IEEE Computer Society 59–68.CrossRefGoogle Scholar
Parrow, J. (2008) Expressiveness of process algebras. Electronic Notes in Theoretical Computer Science 209 173186.CrossRefGoogle Scholar
Parrow, J. (2014) General conditions for full abstraction. In this issue of Mathematical Structures in Computer Science.CrossRefGoogle Scholar
Paterson, M. S. and Hewitt, C. E. (1970) Comparative schematology. In: Conference on Concurrent Systems and Parallel Computation, ACM 119–127.Google Scholar
Perez, J. A. (2009) Higher-Order Concurrency: Expressiveness and Decidability Results, Ph.D. thesis, University of Bologna.Google Scholar
Peters, K. and Nestmann, U. (2012) Is it a ‘good’ encoding of mixed choice? In: Birkedal, L. (ed.) Foundations of Software Science and Computation Structures (FoSSaCS). Springer Lecture Notes in Computer Science 7213 210224.CrossRefGoogle Scholar
Peters, K., Nestmann, U. and Goltz, U. (2013) On distributability in process calculi. In: Felleisen, M. and Gardner, P. (eds.) European Symposium on Programming (ESOP). Springer Lecture Notes in Computer Science 7792 310329.CrossRefGoogle Scholar
Plotkin, G. D. (1977) LCF considered as a programming language. Theoretical Computer Science 5 (3) 223255.CrossRefGoogle Scholar
Quaglia, P. and Walker, D. (2000) On synchronous and asynchronous mobile processes. In: Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS). Springer Lecture Notes in Computer Science 1784 283296.CrossRefGoogle Scholar
Quaglia, P. and Walker, D. (2005) Types and full abstraction for polyadic π-calculus. Information and Computation 200 (2) 215246.CrossRefGoogle Scholar
Reynolds, J. C. (1970) GEDANKEN – a simple typeless language based on the principle of completeness and the reference concept. Communications of the ACM 13 308319.CrossRefGoogle Scholar
Reynolds, J. C. (1981) The Essence of ALGOL, North Holland 345372.Google Scholar
Riecke, J. G. (1991) Fully abstract translations between functional languages. In: Proceedings of Principles of Programming Languages (POPL), ACM 245–254.CrossRefGoogle Scholar
Sangiorgi, D. (1993) Expressing Mobility in Process Algebras: First-Order and Higher-Order Para-digms, Ph.D. thesis, Laboratory for Foundations of Computer Science, University of Edinburgh. CST-99-93 (also published as ECS-LFCS-93-266).Google Scholar
Sangiorgi, D. and Walker, D. (2001) The π-Calculus: A Theory of Mobile Processes, Cambridge University Press.Google Scholar
Shapiro, E. Y. (1991) Separating concurrent languages with categories of language embeddings (extended abstract). In: Proceedings of Symposium on Theory of Computing (STOC), ACM 198–208.Google Scholar
Steele, G. L. and Sussman, G. J. (1976) Lambda: The ultimate imperative. AI Lab Memo AIM-353, MIT AI Lab.Google Scholar
van Glabbeek, R. (2012) Musing on encodings and expressiveness. In: Proceedings of EXPRESS/SOS. Electronic Proceedings in Theoretical Computer Science 89 8198.CrossRefGoogle Scholar
van Glabbeek, R. J. (1990) The linear time-branching time spectrum (extended abstract) In: Proceedings of International Conference on Concurrency Theory (CONCUR). Springer Lecture Notes in Computer Science 458 278297.CrossRefGoogle Scholar
van Glabbeek, R. J. (1993) The linear time - branching time spectrum ii. In: Proceedings of International Conference on Concurrency Theory (CONCUR). Springer Lecture Notes in Computer Science 715 6681.CrossRefGoogle Scholar
Victor, B. and Parrow, J. (1996) Constraints as processes In: Montanari, U. and Sassone, V. (eds.) Proceedings of International Conference on Concurrency Theory (CONCUR '96). Springer-Verlag Lecture Notes in Computer Science 119 389405.CrossRefGoogle Scholar
Yoshida, N. (1996) Graph types for monadic mobile processes. In: Proceedings of Foundations of Software Technology and Theoretical Computer Science (FSTTCS). Springer Lecture Notes in Computer Science 1180 371386.CrossRefGoogle Scholar