Skip to main content
SpringerLink
Log in
Book cover

Correct System Design pp 65–82Cite as

On Applicative Similarity, Sequentiality, and Full Abstraction

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9360))

Abstract

We study how applicative bisimilarity behaves when instantiated on a call-by-value probabilistic \(\lambda \)-calculus, endowed with Plotkin’s parallel disjunction operator. We prove that congruence and coincidence with the corresponding context relation hold for both bisimilarity and similarity, the latter known to be impossible in sequential languages.

The authors are partially supported by the ANR project 12IS02001 PACE.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abramsky, S.: The lazy \(\lambda \)-Calculus. In: Turner, D. (ed.) Research Topics in Functional Programming, pp. 65–117. Addison Wesley (1990)

    Google Scholar 

  2. Abramsky, S., Ong, C.-H.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159–267 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  3. Comaniciu, D., Ramesh, V., Meer, P.: Kernel-based object tracking. IEEE Trans. on Pattern Analysis and Machine Intelligence 25(5), 564–577 (2003)

    Article  Google Scholar 

  4. Crubillé, R., Dal Lago, U.: On probabilistic applicative bisimulation and call-by-value \(\lambda \)-calculi (long version). CoRR, abs/1401.3766 (2014)

    Google Scholar 

  5. Dal Lago, U., Sangiorgi, D., Alberti, M.: On coinductive equivalences for higher-order probabilistic functional programs (long version). CoRR, abs/1311.1722 (2013)

    Google Scholar 

  6. Dal Lago, U., Sangiorgi, D., Alberti, M.: On coinductive equivalences for higher-order probabilistic functional programs. In: POPL, pp. 297–308 (2014)

    Google Scholar 

  7. Dal Lago, U., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO - Theor. Inf. and Applic. 46(3), 413–450 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  8. Danos, V., Harmer, R.: Probabilistic game semantics. ACM Trans. Comput. Log. 3(3), 359–382 (2002)

    Article  MathSciNet  Google Scholar 

  9. Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179(2), 163–193 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  10. Ehrhard, T., Tasson, C., Pagani, M.: Probabilistic coherence spaces are fully abstract for probabilistic PCF. In: POPL, pp 309–320 (2014)

    Google Scholar 

  11. Goldwasser, S., Micali, S.: Probabilistic encryption. J. Comput. Syst. Sci. 28(2), 270–299 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  12. Goodman, N.D.: The principles and practice of probabilistic programming. In: POPL, pp. 399–402 (2013)

    Google Scholar 

  13. Jones, C., Plotkin, G.D.: A probabilistic powerdomain of evaluations. In: LICS, pp. 186–195 (1989)

    Google Scholar 

  14. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  15. Lassen, S.B.: Relational Reasoning about Functions and Nondeterminism. PhD thesis, University of Aarhus (1998)

    Google Scholar 

  16. Manning, C.D., Schütze, H.: Foundations of statistical natural language processing, vol. 999. MIT Press (1999)

    Google Scholar 

  17. Ong, C.-H.L.: Non-determinism in a functional setting. In: LICS, pp. 275–286 (1993)

    Google Scholar 

  18. Park, S., Pfenning, F., Thrun, S.: A probabilistic language based on sampling functions. ACM Trans. Program. Lang. Syst. 31(1) (2008)

    Google Scholar 

  19. Pearl, J.: Probabilistic reasoning in intelligent systems: networks of plausible inference. Morgan Kaufmann (1988)

    Google Scholar 

  20. Pfeffer, A.: IBAL: A probabilistic rational programming language. In: IJCAI, pp. 733–740. Morgan Kaufmann (2001)

    Google Scholar 

  21. Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223–255 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  22. Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: POPL, pp. 154–165 (2002)

    Google Scholar 

  23. Thrun, S.: Robotic mapping: A survey. Exploring Artificial Intelligence in the New Millennium, pp. 1–35 (2002)

    Google Scholar 

  24. van Breugel, F., Mislove, M.W., Ouaknine, J., Worrell, J.: Domain theory, testing and simulation for labelled markov processes. Theor. Comput. Sci. 333(1–2), 171–197 (2005)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ENS-Lyon, Lyon, France

    Raphaëlle Crubillé

  2. Universitá di Bologna and INRIA, Bologna, Italy

    Ugo Dal Lago, Davide Sangiorgi & Valeria Vignudelli

Authors
  1. Raphaëlle Crubillé
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ugo Dal Lago
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Davide Sangiorgi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Valeria Vignudelli
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Davide Sangiorgi .

Editor information

Editors and Affiliations

  1. University of Kaiserslautern, Kaiserslautern, Germany

    Roland Meyer

  2. Computer Science, Carnegie Mellon U, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA

    André Platzer

  3. University of Paderborn, Paderborn, Germany

    Heike Wehrheim

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Crubillé, R., Dal Lago, U., Sangiorgi, D., Vignudelli, V. (2015). On Applicative Similarity, Sequentiality, and Full Abstraction. In: Meyer, R., Platzer, A., Wehrheim, H. (eds) Correct System Design. Lecture Notes in Computer Science(), vol 9360. Springer, Cham. https://doi.org/10.1007/978-3-319-23506-6_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23506-6_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23505-9

  • Online ISBN: 978-3-319-23506-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation