nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Metric Reasoning About \(\lambda \)-Terms: The General Case

verfasst von : Raphaëlle Crubillé, Ugo Dal Lago

Erschienen in: Programming Languages and Systems

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

In any setting in which observable properties have a quantitative flavor, it is natural to compare computational objects by way of metrics rather than equivalences or partial orders. This holds, in particular, for probabilistic higher-order programs. A natural notion of comparison, then, becomes context distance, the metric analogue of Morris’ context equivalence. In this paper, we analyze the main properties of the context distance in fully-fledged probabilistic \(\lambda \)-calculi, this way going beyond the state of the art, in which only affine calculi were considered. We first of all study to which extent the context distance trivializes, giving a sufficient condition for trivialization. We then characterize context distance by way of a coinductively-defined, tuple-based notion of distance in one of those calculi, called \(\varLambda ^\oplus _!\). We finally derive pseudometrics for call-by-name and call-by-value probabilistic \(\lambda \)-calculi, and prove them fully-abstract.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel ML and Extended Branching VASS

Nächstes Kapitel Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring

Barendregt, H.P.: The Lambda Calculus - Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1984)MATH

Barendregt, H.P., Dekkers, W., Statman, R.: Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, Cambridge (2013)CrossRef

Bizjak, A., Birkedal, L.: Step-indexed logical relations for probability. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 279–294. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46678-0_18CrossRef

Cappai, A., Dal Lago, U.: On equivalences, metrics, and polynomial time. In: Kosowski, A., Walukiewicz, I. (eds.) FCT 2015. LNCS, vol. 9210, pp. 311–323. Springer, Cham (2015). doi:10.1007/978-3-319-22177-9_24CrossRef

Crubillé, R., Dal Lago, U.: On probabilistic applicative bisimulation and call-by-value \(\lambda \)-calculi. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 209–228. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54833-8_12CrossRefMATH

Crubillé, R., Dal Lago, U.: Metric reasoning about \(\lambda \)-terms: the affine case. In: Proceedings of LICS, pp. 633–644 (2015)

Crubillé, R., Dal Lago, U.: Metric reasoning about \(\lambda \)-terms: the general case (long version) (2016). http://arxiv.org/abs/1701.05521

Crubillé, R., Dal Lago, U., Sangiorgi, D., Vignudelli, V.: On applicative similarity, sequentiality, and full abstraction. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 65–82. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23506-6_7CrossRef

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

10.

Dal Lago, U., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO Theor. Inform. Appl. 46(3), 413–450 (2012)MathSciNetCrossRef

11.

Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labeled Markov systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 258–273. Springer, Heidelberg (1999). doi:10.1007/3-540-48320-9_19CrossRef

12.

Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: Proceedings of LICS, pp. 413–422 (2002)

13.

Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: logic, simulation and games. In: Proceedings of QEST, pp. 264–273 (2008)

14.

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

15.

Escardo, M.: A metric model of PCF. In: Proceedings of the Workshop on Realizability Semantics and Applications (1999). http://www.cs.bham.ac.uk/~mhe/papers/metricpcf.pdf

16.

Gebler, D., Larsen, K.G., Tini, S.: Compositional metric reasoning with probabilistic process calculi. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 230–245. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46678-0_15CrossRef

17.

Gebler, D., Tini, S.: SOS specifications of probabilistic systems by uniformly continuous operators. In: Proceedings of CONCUR, pp. 155–168 (2015)

18.

Giacalone, A., Jou, C.C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of IFIP TC2, pp. 443–458. North-Holland (1990)

19.

Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)MathSciNetCrossRef

20.

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

21.

Goodman, N.D., Mansinghka, V.K., Roy, D.M., Bonawitz, K., Tenenbaum, J.B.: Church: a language for generative models. In: UAI 2008, pp. 220–229 (2008)

22.

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

23.

Jung, A., Tix, R.: The troublesome probabilistic powerdomain. Electron. Notes Theor. Comput. Sci. 13, 70–91 (1998)MathSciNetCrossRef

24.

Manning, C.D., Schütze, H.: Foundations of Statistical Natural Language Processing, vol. 999. MIT Press, Cambridge (1999)MATH

25.

Mardare, R.: Logical foundations of metric behavioural theory for Markov processes. Doctoral thesis (2016, in preparation)

26.

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

27.

Pearl, J.: Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference. Morgan Kaufmann, San Francisco (1988)MATH

28.

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

29.

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

30.

Saheb-Djahromi, N.: Probabilistic LCF. In: Winkowski, J. (ed.) MFCS 1978. LNCS, vol. 64, pp. 442–451. Springer, Heidelberg (1978). doi:10.1007/3-540-08921-7_92CrossRef

31.

Sangiorgi, D.: On the bisimulation proof method. Math. Struct. Comput. Sci. 8, 447–479 (1998)MathSciNetCrossRef

32.

Sangiorgi, D., Vignudelli, V.: Environmental bisimulations for probabilistic higher-order languages. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20–22 January 2016, pp. 595–607 (2016)

33.

Simpson, A.: Reduction in a linear lambda-calculus with applications to operational semantics. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 219–234. Springer, Heidelberg (2005). doi:10.1007/978-3-540-32033-3_17CrossRefMATH

34.

Thrun, S.: Robotic mapping: a survey. Explor. Artif. Intell. New Millenn. 1, 1–35 (2002)

35.

van Breugel, F.: An introduction to metric semantics: operational and denotational models for programming and specification languages. Theor. Comput. Sci. 258(1–2), 1–98 (2001)MathSciNetCrossRef

36.

van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331(1), 115–142 (2005)MathSciNetCrossRef

Titel: Metric Reasoning About -Terms: The General Case
verfasst von: Raphaëlle Crubillé
Ugo Dal Lago
Verlag: Springer Berlin Heidelberg
Buch: Programming Languages and Systems
Print ISBN: 978-3-662-54433-4

Electronic ISBN: 978-3-662-54434-1

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-662-54434-1_13

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"