DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2025.15

On the Metric Nature of (Differential) Logical Relations

Authors: Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract

Differential logical relations are a method to measure distances between higher-order programs. They differ from standard methods based on program metrics in that differences between functional programs are themselves functions, relating errors in input with errors in output, this way providing a more fine grained, contextual, information. The aim of this paper is to clarify the metric nature of differential logical relations. While previous work has shown that these do not give rise, in general, to (quasi-)metric spaces nor to partial metric spaces, we show that the distance functions arising from such relations, that we call quasi-quasi-metrics, can be related to both quasi-metrics and partial metrics, the latter being also captured by suitable relational definitions. Moreover, we exploit such connections to deduce some new compositional reasoning principles for program differences.

Cite as

Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Metric Nature of (Differential) Logical Relations. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.FSCD.2025.15,
  author =	{Dal Lago, Ugo and Hoshino, Naohiko and Pistone, Paolo},
  title =	{{On the Metric Nature of (Differential) Logical Relations}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{15:1--15:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.15},
  URN =		{urn:nbn:de:0030-drops-236300},
  doi =		{10.4230/LIPIcs.FSCD.2025.15},
  annote =	{Keywords: Differential Logical Relations, Quantales, Quasi-Metrics, Partial Metrics}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2023.20

On the Lattice of Program Metrics

Authors: Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract

In this paper we are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalizations of program equivalences. Some of the metrics we are interested in are well-known, such as those based on the interpretation of terms in metric spaces and those obtained by generalizing observational equivalence. We also introduce a new one, called the interactive metric, built by applying the well-known Int-Construction to the category of metric complete partial orders. Our aim is then to understand how these metrics relate to each other, i.e., whether and in which cases one such metric refines another, in analogy with corresponding well-studied problems about program equivalences. The results we obtain are twofold. We first show that the metrics of semantic origin, i.e., the denotational and interactive ones, lie in between the observational and equational metrics and that in some cases, these inclusions are strict. Then, we give a result about the relationship between the denotational and interactive metrics, revealing that the former is less discriminating than the latter. All our results are given for a linear lambda-calculus, and some of them can be generalized to calculi with graded comonads, in the style of Fuzz.

Cite as

Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Lattice of Program Metrics. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.FSCD.2023.20,
  author =	{Dal Lago, Ugo and Hoshino, Naohiko and Pistone, Paolo},
  title =	{{On the Lattice of Program Metrics}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.20},
  URN =		{urn:nbn:de:0030-drops-180049},
  doi =		{10.4230/LIPIcs.FSCD.2023.20},
  annote =	{Keywords: Metrics, Lambda Calculus, Linear Types}
}

Search Results

Documents authored by Hoshino, Naohiko

On the Metric Nature of (Differential) Logical Relations

Abstract

Cite as

On the Lattice of Program Metrics

Abstract

Cite as

Thanks for your feedback!

Could not send message