Authors: Ghilezan, Silvia 
Ivetić, Jelena
Kašterović, Simona
Ognjanović, Zoran 
Savić, Nenad
Title: Towards Probabilistic reasoning about simply typed lambda terms
First page: 11
Last page: 12
Conference: Sedma nacionalna konferencija “Verovatnosne logike i njihove primene” ; Beograd, Srbija, 8. novembar 2017
Issue Date: Nov-2017
We present a formal model PΛ→ for probabilitic reasoning about simply typed lambda terms, which is a combination of lambda calculus [1] and probabilistic logic [3]. We propose its syntax, Kripke-style semantics and an infinitary axiomatization. We use simple type assignment which is sound and complete ([2]) with respect to the simple semantics (based on the concept of a term model). We define two sets of formulas basic formulas and probabilistic formulas. Basic formulas, denoted by For B, are lambda statements and Boolean combinations of lambda statements. Basic probabilistic formula is any formula of the form P≥sα, such thatα ∈ ForB and s ∈[0,1 ]∩ Q. The set of all probabilistic formulas, denoted by For P, is the smallest set containing all basic probabilistic formulas which is closed under Boolean connectives. The language of PΛ→ consist of both basic formulas and probabilistic formula For PΛ→=For B ∪ For P. Neither mixing of basic formulas and probabilistic formulas, nor nested probability operators is allowed. The following two expressions are not (well defined) formulas of the logic PΛ→: α∧P≥12β, P≥13P≥12α. An axiomatic system for the logic PΛ→ is introduced. It consists of axioms chemes and two groups of inference rules, such that rules from the first group can be applied only on lambda statements. The semantics for PΛ→ is a Kripke-style semantics based on the possible-world approach. The main results are soundness and strong completeness of PΛ→ with respect to the proposed model. We proved strong completeness using the fact that simple type assignment is sound and complete with respect to the simple semantics and property that every consistent set can be extended to a maximal consistent set. The crucial part in the proof of strong completenes is the construction of the canonical model using a maximal consistent set.
Keywords: simply typed lambda calculus | probabilistic logic | soundness | strong completeness
Publisher: Mathematical Institute of the SASA
Project: Development of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education 
Representations of logical structures and formal languages and their application in computing 

Show full item record

Page view(s)

checked on May 9, 2024

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.