Towards Probabilistic Reasoning in Type Theory - The Intersection Type Case
| Autor: | Zoran Ognjanović, Jelena Ivetić, Simona Kašterović, Silvia Ghilezan, Nenad Savić |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Soundness
050101 languages & linguistics Theoretical computer science Computer science Semantics (computer science) 05 social sciences Probabilistic logic 02 engineering and technology Possible world Operator (computer programming) Type theory TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 510 Mathematics Intersection TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Lambda calculus computer 000 Computer science knowledge & systems computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030399504 FoIKS |
| DOI: | 10.7892/boris.140892 |
| Popis: | The development of different probabilistic models of uncertainty has been inspired by the rapid progress in various fields, e.g. in AI, probabilistic programming, etc. Lambda calculus is a universal model of computation suitable to express programming languages concepts. Hence, different methods for probabilistic reasoning in lambda calculus have been investigated. In this paper, we develop a formal model for probabilistic reasoning about lambda terms with intersection types, which is a combination of lambda calculus and probabilistic logic. The language of lambda calculus with intersection types is endowed with a probabilistic operator. We propose a semantics based on the possible world approach. An infinitary axiomatization is given for this system and it is proved to be sound with respect to the proposed semantics. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|