Towards Probabilistic reasoning about simply typed lambda terms

Abstract

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.