Probabilistic Reasoning About Simply Typed Lambda Terms

  • Silvia Ghilezan
  • Jelena Ivetić
  • Simona Kašterović
  • Zoran Ognjanović
  • Nenad SavićEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


Reasoning with uncertainty has gained an important role in computer science, artificial intelligence and cognitive science. These applications urge for development of formal models which capture reasoning of probabilistic features. We propose a formal model for reasoning about probabilities of simply typed lambda terms. We present its syntax, Kripke-style semantics and axiomatic system. The main results are the corresponding soundness and strong completeness, which rely on two key facts: the completeness of simple type assignment and the existence of a maximal consistent extension of a consistent set.


Simply typed lambda calculus Probabilistic logic Soundness Strong completeness 



This work was supported by the SNSF project 200021_165549 Justifications and non-classical reasoning, and by the Serbian Ministry of Education, Science and Technological Development through projects ON174026, III 044006 and ON174008.


  1. 1.
    Abadi, M., Halpern, J.Y.: Decidability and expressiveness for first-order logics of probability. Inf. Comput. 112(1), 1–36 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568–589 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North Holland, New York (1984)Google Scholar
  4. 4.
    Barendregt, H.P., Dekkers, W., Statman, R.: Lambda Calculus with Types (Perspectives in logic). Cambridge University Press, Cambridge (2013)CrossRefzbMATHGoogle Scholar
  5. 5.
    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). CrossRefGoogle Scholar
  6. 6.
    Cooper, R., Dobnik, S., Lappin, S., Larsson, S.: A probabilistic rich type theory for semantic interpretation. In: Proceedings of the EACL 2014 Workshop on Type Theory and Natural Language Semantics (TTNLS), pp. 72–79 (2014)Google Scholar
  7. 7.
    Doder, D., Grant, J., Ognjanović, Z.: Probabilistic logics for objects located in space and time. J. Logic Comput. 23(3), 487–515 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Ehrhard, T., Pagani, M., Tasson, C.: The computational meaning of probabilistic coherence spaces. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, pp. 87–96 (2011)Google Scholar
  9. 9.
    Fagin, R., Halpern, J.Y., Megiddo, N.: A logic for reasoning about probabilities. Inf. Comput. 87(1/2), 78–128 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Fattorosi-Barnaba, M., Amati, G.: Modal operators with probabilistic interpretations. I. Studia Logica 46(4), 383–393 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Ghilezan, S., Likavec, S.: Computational interpretations of logics. Zbornik radova, Special Issue Logic and Computer Science, Matematički institut 12(20), 159–215 (2009)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Goodman, N.D.: The principles and practice of probabilistic programming. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 399–402 (2013)Google Scholar
  13. 13.
    Hindley, J.R.: The completeness theorem for typing lambda-terms. Theor. Comput. Sci. 22, 1–17 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Hindley, J.R.: Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science 42. Cambridge University Press, Cambridge (1997)CrossRefzbMATHGoogle Scholar
  15. 15.
    Hindley, J.R., Longo, G.: Lambda-calculus models and extesionality. Math. Logic Q. 26, 289–310 (1980)CrossRefzbMATHGoogle Scholar
  16. 16.
    Ikodinović, N., Ognjanović, Z., Rašković, M., Marković, Z.: First-order probabilistic logics and their applications. Zbornik radova, Subseries Logic in Computer Science, Matematički institut 18(26), 37–78 (2015)MathSciNetGoogle Scholar
  17. 17.
    Kokkinis, I., Maksimović, P., Ognjanović, Z., Studer, T.: First steps towards probabilistic justification logic. Logic J. IGPL 23(4), 662–687 (2015)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Kokkinis, I., Ognjanović, Z., Studer, T.: Probabilistic justification logic. In: Artemov, S., Nerode, A. (eds.) LFCS 2016. LNCS, vol. 9537, pp. 174–186. Springer, Cham (2016). CrossRefGoogle Scholar
  19. 19.
    Lago, U.D., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO Theor. Inform. Appl. 46(3), 413–450 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Marković, Z., Ognjanović, Z., Rašković, M.: A probabilistic extension of intuitionistic logic. Math. Logic Q. 49(4), 415–424 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Milnikel, R.S.: The logic of uncertain justifications. Ann. Pure Appl. Logic 165(1), 305–315 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Nilsson, N.J.: Probabilistic logic. Artif. Intell. 28(1), 71–87 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Ognjanović, Z.: Discrete linear-time probabilistic logics: completeness, decidability and complexity. J. Logic Comput. 16(2), 257–285 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Ognjanović, Z., Rašković, M., Marković, Z.: Probability logics. Zborik radova, Subseries Logic in Computer Science, Matematički institut 12(20), 35–111 (2009)MathSciNetzbMATHGoogle Scholar
  25. 25.
    Ognjanović, Z., Rašković, M., Marković, Z.: Probability Logics: Probability-Based Formalization of Uncertain Reasoning. Springer, Cham (2016)Google Scholar
  26. 26.
    Savić, N., Doder, D., Ognjanović, Z.: Logics with lower and upper probability operators. Int. J. Approx. Reason. 88, 148–168 (2017)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  • Silvia Ghilezan
    • 1
    • 2
  • Jelena Ivetić
    • 1
  • Simona Kašterović
    • 1
  • Zoran Ognjanović
    • 2
  • Nenad Savić
    • 3
    Email author
  1. 1.Faculty of Technical SciencesUniversity of Novi SadNovi SadSerbia
  2. 2.Mathematical Institute SANUBelgradeSerbia
  3. 3.Institute of Computer ScienceUniversity of BernBernSwitzerland

Personalised recommendations