The ANR PPS meeting took place online from Feb 16 to Feb 18, 2021 and was joined with the 4th edition of the PIHOC workshop series initiated by Ugo Dal Lago in 2018 and with a Dal Lago's DIAPASoN ERC project meeting.
The meeting was organised by the Institut de Recherche en Informatique Fondamentale and by Dal Lago's DIAPASoN ERC project.
The meeting was on Zoom. The video recordings provided on this web page are available until Feb 15, 2022.
(last update: Feb 16, 2021)
(GMT+1 (Bologna-Paris time))
Tuesday 16 February
Video recording. Password: Q%L5MdY.zb
Session 1 (chair Ugo Dal Lago)
break
Session 2 (chair Thomas Ehrhard)
A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculus where the probabilistic operator is decomposed into two syntactic constructs: a generator, which represents a probabilistic event; and a consumer, which acts on the term depending on a given event. The resulting calculus, the Probabilistic Event Lambda-Calculus, is confluent, and interprets the call-by-name and call-by-value strategies through different interpretations of the probabilistic operator into our generator and consumer constructs. We present two notions of reduction, one via fine-grained local rewrite steps, and one by generation and consumption of probabilistic events. Simple types for the calculus are essentially standard, and they convey strong normalization. We demonstrate how we can encode call-by-name and call-by-value probabilistic evaluation.
Wednesday 17 February
Session 3 (chair Ugo Dal Lago)
Video recording. Password: #J33&ha82H
Furthermore, we present a weakest precondition calculus for quantitative reasoning about probabilistic pointer programs in QSL. This calculus is a conservative extension of both Ishtiaq's, O'Hearn's and Reynolds' separation logic for heap-manipulating programs and Kozen's / McIver and Morgan's weakest preexpectations for probabilistic programs. Our calculus preserves O'Hearn's frame rule, which enables local reasoning - a key principle of separation logic.
Finally, we briefly touch upon open questions regarding lower bounds on weakest preexpectations and intensional completeness of our calculus.
break
Session 4 (chair Thomas Ehrhard)
Video recording. Password: #J33&ha82H
break
Session 5 (chair Michele Pagani)
Video recording. Password: #J33&ha82H
Motivated by the study of effectful programming languages and computations, we introduce the novel theory of monadic rewriting systems. The latter are rewriting systems whose notion of reduction is effectful, where effects are modelled as monads. Such systems are to effectful computations and programming languages what traditional rewriting systems are to pure computations and programming languages. Contrary to what happens in the ordinary operational semantics of monadic programming languages, defining mathematically and operationally meaningful notions of monadic rewriting turns out to be simply not possible for several monads, including the distribution, powerset, reader, and global state monad. This raises the question of when monadic rewriting is possible. We answer that question by identifying a class of monads, known as weakly cartesian monads, that guarantee monadic rewriting to be well-behaved. As a further evidence of that, we prove a number of proof techniques that allow us to reason about monadic rewriting systems. In case monads are given as equational theories, as it is the case for algebraic effects, we give a sufficient condition on the shape of the theory for having a well-behaved notion of monadic rewriting. Such a condition dates back to an old theory by Guatam and requires equations to be linear. Finally, we apply the abstract theory of monadic rewriting systems to the call-by-value $\lambda$-calculus with algebraic effects, this way obtaining the extension of the well-known confluence and standardisation theorems to an effectful setting. Remarkably, the latter holds for all algebraic effects, whereas the former for the commutative ones only.
Thursday 18 February
Video recording. Password: pNu!dLMc03
Session 6 (chair Michele Pagani)
(Joint work with Wonyeol Lee, Hangyeol Yu, and Hongseok Yang, KAIST)
Probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been explored intensely, which led to the development of so called deep probabilistic programming languages, such as Pyro, Edward and ProbTorch. At the core of this development lie inference engines based on stochastic variational inference algorithms. When asked to find information about the posterior distribution of a model written in such a language, these algorithms convert this posterior-inference query into an optimisation problem and solve it approximately by a form of gradient ascent or descent.
In this talk, we analyse one of the most fundamental and versatile variational inference algorithms, called score estimator or REINFORCE, using tools from denotational semantics and program analysis. We formally express what this algorithm does on models denoted by programs, and expose implicit assumptions made by the algorithm on the models. The violation of these assumptions may lead to an undefined optimisation objective or the loss of convergence guarantee of the optimisation process. We then describe rules for proving these assumptions, which can be automated by static program analyses. Some of our rules use nontrivial facts from continuous mathematics, and let us replace requirements about integrals in the assumptions, such as integrability of functions defined in terms of programs' denotations, by conditions involving differentiation or boundedness, which are much easier to prove automatically (and manually). Following our general methodology, we have developed a static program analysis for the Pyro programming language that aims at discharging the assumption about what we call model-guide support match. Our analysis is applied to the eight representative model-guide pairs from the Pyro webpage, which include sophisticated neural network models such as AIR. It finds a bug in one of these cases, reveals a non-standard use of an inference engine in another, and shows that the assumptions are met in the remaining six cases.
break
Session 7 (chair Ugo Dal Lago)
Video recording. Password: pNu!dLMc03
Organizers: Ugo Dal Lago and Michele Pagani