Probabilistic Reasoning About Typed Programs: Towards Compactness

Reasoning with uncertainty has gained an important role in various fields of computer science, artificial intelligence and cognitive science, while it is underdeveloped in typed calculi. For this reason, we have investigated different approaches used to introduce probability into typed calculi. In this paper, we develop P CL logic, which is a formal model for probabilistic reasoning about typed programs. The semantics of P CL is based on the possible world approach. Allowing the range of probability functions to be infinite results in non-compactness of the logic. As a consequence, a finite axiomatization of the logic cannot be sound and strongly complete. We propose the simplest method for resolving the non-compactness phenomenon of the logic P CL.