L'algèbre universelle et la logique équationnelle sont des outils bien établis pour raisonner sur les programmes et les équivalences de programmes. Les algèbres quantitatives et la logique équationnelle quantitative ont été introduites en 2016 comme une extension naturelle de ces outils pour raisonner sur les distances entre programmes. Dans cette thèse, nous étendons cette ligne de travail pour traiter des notions généralisées de distances.
Nous montrons que certaines propriétés du cadre original sont toujours valables dans notre version généralisée. Nous montrons comment certains résultats provenant d'autres endroits de la littérature (par exemple, les algèbres ordonnées) sont recouvrés dans notre cadre plus général. Nous prouvons un nouveau résultat qui rend l'application du raisonnement algébrique quantitatif plus accessible. Nous fournissons de nouveaux exemples et revisitons des exemples connus de telles applications à l'aide de ce résultat.
English version
Universal algebra and equational logic stand as well-established tools for reasoning about programs and program equivalences. Quantitative algebras and quantitative equational logic were introduced in 2016 as a natural extension of these to reason about program distances. In this thesis, we further extend this line of work to handle generalised notions of distances.
We show some properties of the original framework still hold in our generalised version.
We show how some results from other places in the literature (e.g. ordered algebras) are recovered within our more general framework. We prove a new result that makes applying quantitative algebraic reasoning more accessible. We provide new examples and revisit known examples of such applications with the help of this result.
Gratuit
Disciplines