Niels Voorneveld: Quantitative Logics for Equivalence of Effectful Programs

Abstract: Two terms of a programming language are behaviourally equivalent if they satisfy the same behavioural properties. In this talk, we consider specifying such behavioural properties using a quantitative logic. These logics contain formulas which can for instance express probabilities that, or sets of correct starting states for which, a program satisfies a property. Given such quantitative formulas, we say that two terms are behaviourally equivalent if they satisfy the same formulas to the same degree.

This work is a generalisation of previous work by the speaker and Alex Simpson, in which Boolean logics are considered. Fundamental to the design of these logics are the quantitative modalities, predicate liftings which determine the behavioural aspects of the effects under consideration. If these quantitative modalties satisfy certain properties, we can prove that the behavioural equivalence is compatible, hence a congruence. We investigate these results in the context of Levy's call-by-push-value with general recursion and algebraic effects. We will look at some examples of effects to which the results apply. These include nondeterminism, probability, global store, error, cost, and certain combinations thereof. We will also briefly look at other notions of program equivalence for effectful languages. Most notably, we will see that each behavioural equivalence coincides with a notions of Abramsky's applicative bisimilarity, which allows us to prove the aforementioned compatibility of the behavioural equivalence.