On the Metric Nature of (Differential) Logical Relations

1. Problématique

L'équivalence de programmes est un concept fondamental en sémantique des programmes, garantissant que deux implémentations produisent les mêmes résultats. Cependant, dans de nombreux cas pratiques (optimisation, refactoring, calcul incrémental), les programmes ne sont pas strictement équivalents mais proches. La mesure quantitative de la distance entre des programmes non équivalents est donc cruciale.

Les relations logiques différentielles (Differential Logical Relations - DLR) ont été introduites pour mesurer ces distances dans les langages d'ordre supérieur. Contrairement aux métriques classiques qui attribuent un nombre unique à la distance entre deux fonctions, les DLR utilisent des fonctions pour mesurer la distance. Une distance entre deux fonctions $f$ et $g$ est une fonction $d$ qui, pour une erreur d'entrée donnée, borne l'erreur de sortie.

Cependant, la nature mathématique précise de ces distances reste floue dans la littérature :

• Les DLR ne satisfont pas la réflexivité standard ($d(x,x)=0$) : la distance d'une fonction à elle-même n'est pas toujours nulle (elle dépend de la fonction elle-même).
• Elles ne satisfont pas toujours la symétrie.
• La question centrale est : Les distances générées par les relations logiques différentielles constituent-elles une forme de métrique quantale-valued bien définie ? Si oui, quelles propriétés de réflexivité et de transitivité satisfont-elles ?

2. Méthodologie

Les auteurs adoptent une approche catégorielle et algébrique pour clarifier la structure métrique des DLR :

1. Introduction des "Quasi-Quasi-Métriques" (Quasi-Quasi-Metrics) :

   • Ils définissent une nouvelle classe de métriques à valeurs dans un quantale (une structure algébrique généralisant les distances).
   • Le nom "Quasi-Quasi" reflète deux affaiblissements par rapport aux métriques standards :
     • Quasi-réflexivité (premier "Quasi") : Au lieu de $d(x,x)=0$, on a $d(x,x) \le d(x,y)$ (ou une condition similaire dépendant du contexte). Cela permet de modéliser le fait qu'une fonction peut avoir une "distance à elle-même" non nulle (liée à sa variation).
     • Absence de symétrie (deuxième "Quasi") : $d(x,y)$ n'est pas nécessairement égal à $d(y,x)$.
   • Ils introduisent également une condition de transitivité forte gauche (Left Strong Transitivity), une variante de la transitivité forte des métriques partielles, adaptée au contexte quantale.

2. Construction Catégorielle :

   • Ils définissent la catégorie $\mathbf{Qqm}$ des espaces quasi-quasi-métriques.
   • Ils démontrent que cette catégorie est cartésienne close. Cette propriété est essentielle car elle correspond structurellement à la construction des types fonctionnels dans les langages d'ordre supérieur.
   • Ils montrent que la structure cartésienne close de $\mathbf{Qqm}$ reflète exactement la construction des relations logiques différentielles.

3. Sémantique du Calcul Lambda Typé ($\Lambda_{Real}$) :

   • Ils interprètent un calcul lambda simplement typé avec des réels dans la catégorie $\mathbf{Qqm}$.
   • Ils dérivent un Lemme Fondamental (Fundamental Lemma) directement de la structure catégorielle, établissant que l'interprétation de tout terme bien typé préserve les relations quasi-quasi-métriques.

4. Étude des Relations Prélogiques Différentielles :

   • Ils définissent les relations prélogiques différentielles comme des familles indexées par les types de quasi-quasi-métriques satisfaisant le lemme fondamental.
   • Ils analysent la structure d'ordre de l'ensemble de ces relations (poset) pour déterminer l'existence d'une métrique "la plus fine" (équationnelle) et d'une métrique "la plus grossière" (contextuelle).

3. Contributions Clés

• Définition formelle des Quasi-Quasi-Métriques : Une nouvelle notion unifiant les concepts de métriques partielles et de relations logiques différentielles, caractérisée par la quasi-réflexivité et la transitivité forte gauche.
• Modèle Catégoriel : Preuve que la catégorie $\mathbf{Qqm}$ est cartésienne close, fournissant un cadre mathématique rigoureux pour les DLR.
• Lemme Fondamental Categorical : Démonstration que le lemme fondamental pour les programmes n'est pas une propriété ad hoc, mais une conséquence directe de la structure cartésienne close de l'espace des métriques.
• Propriétés des Modèles de Types : Preuve que les espaces métriques issus de l'interprétation des types satisfont non seulement la transitivité forte gauche, mais aussi une forme faible de symétrie et une propriété d'indistinction (self-indistancy).
• Résultat Négatif sur la Métrique Contextuelle : Analyse de l'ensemble des relations prélogiques différentielles montrant l'absence d'un élément maximal (greatest element).

4. Résultats Principaux

1. Correspondance Structurelle : La construction des relations logiques différentielles préserve la structure des quasi-quasi-métriques. Les distances entre programmes ne sont pas de simples nombres, mais des fonctions monotones qui respectent la transitivité forte gauche.
2. Le Lemme Fondamental : Pour tout terme $t$ de type $A \to B$, il existe une "dérivée" $t^\bullet$ telle que si l'entrée varie de $a$, la sortie varie d'au plus $t^\bullet(a)$. Ce résultat découle naturellement de l'interprétation catégorielle.
3. Absence de Métrique Contextuelle :
   • L'ensemble des relations prélogiques différentielles forme un poset qui possède un élément minimal (la métrique la plus fine), qui correspond à la théorie équationnelle quantitative.
   • Cependant, ce poset n'a pas d'élément maximal (la métrique la plus grossière).
   • Signification : Contrairement aux équivalences de programmes (où l'équivalence contextuelle est l'équivalence la plus grossière), il n'existe pas de notion naturelle de "métrique contextuelle" pour les programmes d'ordre supérieur dans ce cadre. L'obstacle réside dans le fait que le lemme fondamental ne garantit qu'une approximation inférieure de la distance, rendant impossible la définition d'une métrique contextuelle unique qui capturerait toutes les distinctions possibles.

5. Signification et Impact

• Clarification Théorique : Cet article résout une ambiguïté majeure dans la littérature sur les DLR en les ancrant dans la théorie des métriques quantales-valued (quasi-quasi-métriques).
• Outils pour l'Analyse : La structure catégorielle offre un cadre puissant pour raisonner de manière compositionnelle sur les erreurs et les distances dans les programmes d'ordre supérieur, y compris ceux avec effets (monades) et récursivité.
• Limites de l'Approche Quantitative : La découverte de l'absence de métrique contextuelle maximale est un résultat profond. Elle suggère que la notion de "distance contextuelle" (similaire à l'équivalence contextuelle) est intrinsèquement plus complexe, voire impossible à définir de manière unique dans les langages d'ordre supérieur non linéaires, en raison de la dépendance circulaire entre les distances des termes et celles des contextes.
• Perspectives : Ce travail ouvre la voie à l'application de techniques topologiques et de limites (issues de la théorie des métriques quantales) à la sémantique des langages de programmation, tout en identifiant les limites fondamentales de la quantification des distances programmatiques.

En résumé, l'article établit que les relations logiques différentielles sont naturellement modélisées par des quasi-quasi-métriques, offrant un cadre robuste pour l'analyse quantitative des programmes, tout en révélant une limitation fondamentale concernant l'existence d'une métrique contextuelle universelle.