Advanced Semantics for Non-deterministic and Probabilistic Programming

Declarative programming is the idea that a program should describe what it does, which problem it is solving, not how it does so. In this fashion, declarative programming focuses on the complexity that is inherent in the problem, not the accidental complexity that originates from solving the problem on a computer. By reducing accidental complexity, declarative programming eliminates a common source of bugs. This thesis contributes towards declarative programming in three distinct, but partly overlapping paradigms: logic programming, functional programming and probabilistic programming. The first part of this thesis studies tabling, which is a powerful resolution mechanism for logic programming that ensures termination of a larger class of programs. Extensions of this technique, such as mode-directed tabling and answer subsumption allow efficient tabling for optimisation problems. While much attention has been devoted to the expressivity and efficiency of these approaches, soundness has not been considered. This thesis shows that the different implementations indeed fail to produce the correct answer for some programs. To remedy this situation, the thesis provides a formal framework that generalises the existing approaches and establishes a correctness criterion that explains when the approach is sound. Then, tabling is adapted for non-determinism in the functional programming language Haskell. Non-determinism is a technique that allows expressing a wide range of problems in a concise and declarative manner. Essentially, non- determinism means that programs can return zero or more answers as opposed to a single deterministic one. However, Haskell's default recursion mechanism is not the right one for non-deterministic programs, and causes non-termination. Instead, the correct semantics is a set-based least fixed point semantics, which is implemented via tabling as a monad. The set-based least fixed point semantics is then generalised to arbitrary complete lattices, enabling tabling for optimisation problems. The second part of this thesis presents PλωNK, a probabilistic programming language for modelling networks. Unlike the earlier modelling language Probabilistic NetKAT (PNK), PλωNK provides higher-order functions, to make programming much more convenient and declarative. The formalisation of PλωNK is challenging for two reasons: Firstly, network programming introduces multiple side effects (in particular, non-determinism and probabilistic choice) which need to be carefully controlled in a functional setting. For this purpose, the system uses an explicit syntax for functions and sequencing which makes the interplay of these effects explicit. Secondly, measure theory, the standard domain for formalisation of probabilistic languages does not admit higher-order functions. We address this by leveraging ω-Quasi Borel Spaces, a recent advancement in the domain theory of probabilistic programming. This work is not only useful for bringing abstraction to PNK. The meta-theory for PλωNK which combines advanced features like higher-order functions, iteration and parallelism, may also inform similar meta-theoretic efforts.

Jaar van publicatie:2020

Toegankelijkheid:Open