Probabilistic Reasoning about Typed Combinatory Logic

Abstract

In [6, 7] we have introduced a Logic of Combinatory Logic (LCL), a for- mal system for reasoning about simply typed combinatory terms. The LCL is obtained by extending the simply typed combinatory logic with classical propo- sitional connectives, and corresponding axioms and rules. In [7] we have pre- sented the syntax, axiomatization and semantics of LCL. The language of the logic LCL is generated by the following syntax α, β := M : σ | ¬α | α ∧ β where M : σ is type assignment statement typable from some basis Γ in simply typed combinatory logic, M is a combinatory term and σ is a simple type. The axiomatic system of LCL is obtained by combining the axiomatic system for classical propositional logic and type assignment system for simply typed combinatory logic. The semantics for LCL, inspired by Kripke-style semantics for lambda calculus with types introduced in [8, 5], is based on an extensional applicative structure containing special elements that correspond to primitive combinators. We have proved that the given axiomatization is sound and complete with respect to the proposed semantics. Further, we proved that the logic LCL is a conservative extension of the simply typed combinatory logic. Our goal is to use the logic LCL to develop a formal system for probabilistic reasoning about typed combinatory terms. The idea of formal system for rea- soning about simply typed lambda terms and lambda terms with intersection types is presented in [2, 3]. These models are based on the well-known models of lambda calculus, i.e. terms models ([4]) and filter models ([1]). However, these models have shown not to be suitable for propositional reasoning about typed terms. For this reason, we have developed the logic LCL. We define PCL, a probabilistic system for simply typed combinatory terms, as a probabilistic logic over LCL. Formulas of PCL are layered into two sets: basic formulas and probabilistic formulas. Basic formulas are LCL-formulas. The set of probabilistic formulas is generated by the following syntax φ, ψ := P≥aα | ¬φ | φ ∧ ψ where α is an LCL-formula and s ∈ Q ∩ [0, 1]. The semantics of PCL are defined as Kripke-style semantics where each world represents one LCL model. The axiomatic system for PCL is obtained from the axiomatic system for probability logic and axiomatic system for LCL. For future work, we plan to prove that the given axiomatization of PCL is sound and complete with respect to the proposed semantics of PCL. Further, we plan to investigate probabilistic extensions of other typed calculi.