Skip to Main content Skip to Navigation
Theses

Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects

Francesco Gavazzo 1, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : This dissertation investigates notions of program equivalence and metric for higher-order sequential languages with algebraic effects. Computational effects are those aspects of computation that involve forms of interaction with the environment. Due to such an interactive behaviour, reasoning about effectful programs is well-known to be hard. This is especially true for higher-order effectful languages, where programs can be passed as input to, and returned as output by other programs, as well as perform side-effects. Additionally, when dealing with effectful languages, program equivalence is oftentimes too coarse, not allowing, for instance, to quantify the observable differences between programs. A natural way to overcome this problem is to refine the notion of a program equivalence into the one of a program distance or program metric, this way allowing for a finer, quantitative analysis of program behaviour. A proper account of program distance, however, requires a more sophisticated theory than program equivalence, both conceptually and mathematically. This often makes the study of program distance way more difficult than the corresponding study of program equivalence. Algebraic effects provide a powerful formalism to structure effectful higher-order (sequential) computations. Accordingly, effectful computations are produced by means of effect-triggering operations which act as sources of the side effects of interest. Such operations are algebraic, in the sense that their (operational) semantics is independent of their continuation, and thus effects act independently of the evaluation context in which they are executed. Algebraic effects can be used to model several computational effects, proving formal models for higher-order languages with nondeterministic, probabilistic, and imperative features, as well as combinations thereof. In fact, contrary to other theories of computational effects, algebraic effects naturally support operations to combine algebraic theories, and thus allow for the combination of effects with one another.These features make reasoning about program equivalence for languages with algebraic effects challenging, as the operational behaviour of a program may be determined by complex interactions between the program and the environment. The first part of this dissertation studies bisimulation-based notions of equivalence and refinement for $\lambda$-calculi enriched with algebraic effects. In particular, notions of effectful applicative and normal form (bi)similarity are defined for both call-by-name and call-by-value $\lambda$-calculi, as well as a notion of monadic applicative (bi)similarity for call-by-name calculi only. For all these notions, congruence and precongruence theorems are proved, which directly lead to soundness results with respect to an extension of Morris' contextual equivalence to effectful calculi. In order to design the aforementioned notions of equivalence and refinement, an abstract relational framework is developed, which is based on the notions of a monad and of a relator, the latter being an abstract construction axiomatising relation lifting operations. The second part of this dissertation is devoted to the study of program distances for languages with algebraic effects. Following Lawvere analysis of metric spaces as enriched categories, the abstract relational framework developed in the first part of the dissertation, is extended to relations taking values over quantales, the latter being algebraic structures whose elements represent `abstract quantities'. Using such a framework, the notion of an effectful applicative bisimulation distance is defined, and its main properties are studied. Due to the so-called distance trivialisation, however, the notion of an effectful applicative bisimulation distance is defined for a calculus supporting program sensitivity. The latter is the law describing how much operational differences in output are affected by operational differences in input. Relying on the notion of program sensitivity, an abstract (pre)congruence theorem for effectful applicative (bi)similarity distance is proved, which states that the latter behaves as a Lipschitz-continuous metric-like function, this way enabling compositional reasoning about program distance.
Document type :
Theses
Complete list of metadata

Cited literature [177 references]  Display  Hide  Download

https://hal.inria.fr/tel-02386201
Contributor : Francesco Gavazzo <>
Submitted on : Friday, November 29, 2019 - 11:18:14 AM
Last modification on : Friday, October 30, 2020 - 12:04:04 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-02386201, version 1

Collections

Citation

Francesco Gavazzo. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Programming Languages [cs.PL]. Alma Mater Studiorum Università di Bologna, 2019. English. ⟨tel-02386201⟩

Share

Metrics

Record views

76

Files downloads

157