Top

Published in:

2020 | OriginalPaper | Chapter

A Type Theory for Probabilistic \(\lambda \)–calculus

Author : Alessandra Di Pierro

Published in: From Lambda Calculus to Cybersecurity Through Program Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We present a theory of types where formulas may contain a choice constructor. This constructor allows for the selection of a particular type among a finite set of options, each corresponding to a given probabilistic term. We show that this theory induces a type assignment system for the probabilistic \(\lambda \)–calculus introduced in an earlier work by Chris Hankin, Herbert Wiklicky and the author, where probabilistic terms represent probability distributions on classical terms of the simply typed \(\lambda \)–calculus. We prove the soundness of the type assignment with respect to a probabilistic term reduction and a normalization property of the latter.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Cathoristic Logic

next chapter Galois Connections for Recursive Types

Having in mind a model in which a type is a vector space, it is natural to consider its subspaces as its subtypes.

In fact, probabilities are used at the semantical level only to estimate the likelihood that a certain value is actually otained after the reduction process.

Abramsky, S., Hankin, C. (eds.): Abstract Interpretation of Declarative Languages. Halsted Press, Sydney (1987)

Abramsky, S., Jensen, T.P.: A relational approach to strictness analysis for higher-order polymorphic functions. In: Proceedings of ACM Symposium on Principles of Programming Languages, pp. 49–54 (1991)

Barbanera, F., Dezani-Ciancaglini, M., de’Liguoro, U.: Intersection and union types: syntax and semantics. Inf. Comput. 119(2), 202–230 (1995). https://doi.org/10.1006/inco.1995.1086. https://dx.doi.org/10.1006/inco.1995.1086MathSciNetCrossRefMATH

Barendregt, H.P.: The Lambda Calculus, Studies in Logic and the Foundations of Mathematics, vol. 103, revised edn. North-Holland (1991)

Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, S.E. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 117–309. Oxford University Press Inc., New York (1992), http://dl.acm.org/citation.cfm?id=162552.162561

Barendregt, H.: The Lambda Calculus, Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103. Elsevier (1984)

Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17(4), 471–523 (1985). https://doi.org/10.1145/6041.6042CrossRef

Castagna, G., Ghelli, G., Longo, G.: A calculus for overloaded functions with subtyping. Inform. Comput. 117(1), 115–135 (1995). https://doi.org/10.1006/inco.1995.1033MathSciNetCrossRefMATH

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

10.

Dezani, M.: Logical semantics for concurrent lambda calculus, ph.D. Thesis, Radboud University Nijmegen (1996)

11.

Di Pierro, A., Hankin, C., Wiklicky, H.: Probabilistic lambda-calculus and quantitative program analysis. J. Logic Comput. 15(2), 159–179 (2005)MathSciNetCrossRef

12.

Di Pierro, A., Wiklicky, H.: Measuring the precision of abstract interpretations. LOPSTR 2000. LNCS, vol. 2042, pp. 147–164. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45142-0_9CrossRef

13.

Draheim, D.: Semantics of the Probabilistic Typed Lambda Calculus - Markov Chain Semantics, Termination Behavior, and Denotational Semantics. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-642-55198-7CrossRefMATH

14.

Girard, J.Y.: Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In: Proceedings of the 2nd Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 63–92. North-Holland (1971)

15.

Gunter, C.A.: Foundations of Computing. MIT Press, Cambridge (1992)

16.

Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Functional characters of solvable terms. Math. Logic Q. 27(2–6), 45–58 (1981)MathSciNetCrossRef

17.

Park, S.: A calculus for probabilistic languages. In: Proceedings of the ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 38–49. ACM (2003)

18.

Park, S., Pfenning, F., Thrun, S.: A monadic probabilistic language (2003). manuscript. http://www.cs.cmu.edu/~fp/papers/prob03.pdf

19.

Park, S., Pfenning, F., Thrun, S.: A probabilistic language based on sampling functions. ACM Trans. Program. Lang. Syst. 31(1), 4:1–4:46 (2008). https://doi.org/10.1145/1452044.1452048. https://doi.acm.org/10.1145/1452044.1452048CrossRefMATH

20.

Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)MATH

21.

Plotkin, G.D.: Call-by-name, call-by-value and the \(\lambda \)-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)MathSciNetCrossRef

22.

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

23.

Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: Proceedings of ACM Symposium on Principles of Programming Languages, pp. 154–165. ACM Press (2002)

24.

Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19, pp. 408–425. Springer, Heidelberg (1974). https://doi.org/10.1007/3-540-06859-7_148CrossRef

25.

Roman, S.: Advanced Linear Algebra. Graduate Texts in Mathematics 135. Springer, New York (2008). https://doi.org/10.1007/978-0-387-72831-5CrossRef

Title: A Type Theory for Probabilistic –calculus
Author: Alessandra Di Pierro
Publisher: Springer International Publishing
Book: From Lambda Calculus to Cybersecurity Through Program Analysis
Print ISBN: 978-3-030-41102-2

Electronic ISBN: 978-3-030-41103-9

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-41103-9_3

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"