💻 computer science

When Equality Fails as a Rewrite Principle: Provenance and Definedness for Measurement-Bearing Expressions

Cet article présente une sémantique unifiée pour les expressions portant des mesures, qui intègre la provenance et la définissabilité pour établir des règles de réécriture sûres et formellement vérifiées en Lean 4, démontrant que l'égalité algébrique classique est insuffisante pour garantir l'interchangeabilité de ces expressions.

Auteurs originaux : David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Publié 2026-04-10

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous êtes un chef cuisinier très méticuleux qui prépare une recette scientifique. Dans votre cuisine, chaque ingrédient n'est pas juste une quantité (comme "200 grammes de farine"), mais un ingrédient réel avec une histoire : il vient d'un sac précis, pesé à un moment précis, avec une petite marge d'erreur.

Ce papier de recherche explique pourquoi, dans ce monde de la cuisine scientifique, on ne peut pas simplement appliquer les règles de l'algèbre de l'école primaire (comme dire que $x - x = 0$ ) sans faire très attention.

Voici l'explication simple, avec des analogies :

1. Le Problème : Pourquoi $x - x$ n'est pas toujours égal à 0 ?

En mathématiques classiques, si vous avez une variable $x$ , alors $x - x$ est toujours 0. C'est comme si vous aviez un seul sac de farine et que vous enleviez ce même sac de la balance : il ne reste rien.

Mais dans la science, il y a deux pièges :

Piège n°1 : L'Origine (La "Provenance")
Imaginez que vous avez deux sacs de farine.
- Cas A : Vous prenez le même sac, vous le posez sur la balance, vous le notez, puis vous le retirez. ( $x - x$ ). Résultat : 0. C'est sûr.
- Cas B : Vous prenez un premier sac, vous le pesez, puis vous prenez un deuxième sac (qui vient d'un autre endroit, même si les deux sont marqués "200g"). Vous faites la soustraction. ( $x_1 - x_2$ ).
- Le problème : Même si les deux sacs sont étiquetés pareil, ils ne pèsent peut-être pas exactement la même chose à cause de petites erreurs de fabrication. Le résultat n'est pas forcément 0 !
- L'analogie : C'est comme si vous disiez : "J'ai deux jumeaux qui se ressemblent exactement, donc ils sont la même personne." Non, ce sont deux personnes différentes ! Le papier dit qu'il faut garder une étiquette (un "jeton" ou token) pour savoir si on parle du même objet ou de deux objets jumeaux.
Piège n°2 : Le "Zéro Interdit" (La "Définition")
Imaginez que vous divisez une quantité par elle-même : $x / x$ .
- Si $x$ est 5, le résultat est 1.
- Si $x$ est 100, le résultat est 1.
- Mais que se passe-t-il si $x$ est 0 ? En mathématiques, on ne peut pas diviser par zéro. C'est interdit.
- Le problème : L'expression "1" est toujours valable. Mais l'expression " $x/x$ " devient dangereuse si $x$ peut être zéro. Si vous remplacez " $x/x$ " par "1" dans une formule, vous risquez d'introduire un accident (une division par zéro) là où il n'y en avait pas avant.
- L'analogie : C'est comme dire : "Cette route est toujours ouverte." C'est vrai pour la route principale. Mais si vous dites : "Cette route est toujours ouverte, sauf si un pont est effondré", vous ne pouvez pas simplement effacer la mention du pont. Si vous simplifiez la route en disant "c'est toujours ouvert", vous oubliez le danger du pont.

2. La Solution du Papier : Un Nouveau Système de Sécurité

Les auteurs disent : "Arrêtez de faire confiance aveuglément aux règles d'algèbre !". Ils proposent un nouveau système de cuisine (une "sémantique") qui vérifie deux choses avant de laisser un cuisinier simplifier une recette :

Qui est l'ingrédient ? (Est-ce le même sac de farine ou deux sacs différents ?) -> On appelle ça la Provenance.
Est-ce que c'est sûr de le faire ? (Est-ce qu'on risque de tomber dans le trou du zéro ?) -> On appelle ça le Domaine Admissible.

3. Les Règles du Jeu (Les Analogies)

Le papier établit des règles strictes pour savoir quand on peut remplacer une formule par une autre :

La Règle de l'Allumage (Simplification à sens unique) :
Parfois, on peut simplifier une recette pour la rendre plus sûre, mais on ne peut pas faire l'inverse.
- Exemple : Si vous avez une recette qui dit "Divisez par $x$ ", et que vous savez que $x$ est toujours positif (jamais zéro), vous pouvez simplifier en disant "C'est égal à 1". C'est sûr.
- Mais si vous avez "1" et que vous voulez le transformer en " $x/x$ ", vous ne pouvez pas le faire si $x$ pourrait être zéro. Vous auriez créé un danger. C'est comme enlever un garde-corps : c'est facile, mais le remettre en place quand le sol est glissant est interdit.
La Règle de l'Échange Interdit :
Parfois, deux recettes semblent donner le même résultat partout où elles fonctionnent, mais on ne peut pas les échanger.
- Exemple : Imaginez deux ponts. Le Pont A s'effondre si vous pesez 0 kg. Le Pont B s'effondre si vous pesez 100 kg. Sur tous les autres poids, les deux ponts sont identiques.
- Si vous remplacez le Pont A par le Pont B dans votre itinéraire, vous risquez de vous effondrer à 100 kg. Même si les deux sont "pareils" la plupart du temps, ils ne sont pas interchangeables car leurs zones de danger sont différentes.

4. Pourquoi c'est important ?

Les ordinateurs actuels (les "simplificateurs symboliques") essaient souvent de nettoyer les formules scientifiques en appliquant des règles mathématiques simples. Ce papier montre que c'est dangereux.

Si un ordinateur simplifie une formule de physique ou de chimie en oublant l'origine des mesures ou en oubliant les risques de division par zéro, il peut produire un résultat qui semble correct mais qui est en fait faux ou dangereux.

En résumé :
Ce papier dit aux mathématiciens et aux informaticiens : "Pour faire de la science avec des formules, il ne suffit pas de regarder les chiffres. Il faut regarder d'où viennent les chiffres (provenance) et où ils sont autorisés à aller (définition). Sans ces deux garde-fous, l'égalité mathématique classique échoue."

Ils ont même écrit tout cela dans un langage informatique très rigoureux (Lean 4) pour prouver qu'ils ont raison, sans aucune erreur possible. C'est comme avoir un manuel de sécurité infaillible pour les cuisiniers scientifiques.

1. Le Problème

L'article aborde une limitation fondamentale dans la manipulation symbolique des expressions scientifiques et de mesure : l'égalité algébrique standard n'est pas un principe de réécriture sûr pour les expressions contenant des mesures.

Deux modes d'échec principaux rendent la substitution d'une expression par une autre non triviale et souvent dangereuse :

La Provenance (Origine de la donnée) : Une même observation physique produit une valeur exacte unique. Si une variable $x$ représente une seule mesure réutilisée deux fois (ex: $x - x$ ), le résultat est exactement 0. Cependant, si deux mesures distinctes $x_1$ et $x_2$ sont prises avec le même instrument et les mêmes bornes d'incertitude, elles ne correspondent pas nécessairement à la même valeur exacte sous-jacente. Les formalismes classiques (analyse dimensionnelle, arithmétique des intervalles) sont "aveugles à la provenance" et ne distinguent pas la réutilisation d'un même token de l'utilisation de deux mesures similaires mais indépendantes.
La Définissabilité (Singularités) : La division introduit des singularités. Deux expressions peuvent être algébriquement égales là où elles sont définies, mais différer par leurs domaines de définition. Par exemple, remplacer la constante $1$ par $x/x$ introduit une singularité en $x=0$ . L'inverse (supprimer une singularité) est sûr, mais l'introduction d'une singularité ne l'est pas. De plus, deux expressions peuvent avoir des structures de singularités incomparables, bloquant toute réécriture dans les deux sens.

Les simplificateurs symboliques actuels échouent souvent car ils traitent ces deux problèmes séparément ou ignorent l'un des deux.

2. Méthodologie

Les auteurs proposent un cadre sémantique unifié formalisé en Lean 4 (sans sorry, c'est-à-dire entièrement prouvé) qui intègre simultanément la provenance et la définissabilité.

Langage d'expression : Un langage minimal contenant des constantes rationnelles exactes et des feuilles mesurées Meas(t, I, d), où $t$ est un token opaque (identifiant de l'événement d'observation), $I$ est un intervalle rationnel, et $d$ est une dimension.
Sémantique à base de Tokens (Enclosure) :
- Un environnement $\sigma$ assigne une valeur rationnelle exacte à chaque token.
- La provenance est gérée par le fait que deux occurrences du même token $t$ dans une expression partagent la même valeur $\sigma(t)$ .
- L'enclos garanti ($Encl(e)$) est l'ensemble des valeurs réalisables par tous les environnements cohérents avec les tokens de $e$ .
Domaines Admissibles (Definedness) :
- Une expression est bien définie ($WellDefined$) si aucun sous-terme de division n'a un dénominateur nul dans l'environnement donné.
- Le domaine admissible ($AdmDom(e)$) restreint l'évaluation aux environnements où l'expression est bien définie.
- L'enclos défini ($DefinedEncl(e)$) est l'ensemble des valeurs réalisables uniquement sur le domaine admissible.
Judgments de Réécriture :
- Niveau Enclos (Provenance uniquement) : $e \leadsto e'$ si $Encl(e') \subseteq Encl(e)$ .
- Niveau Sensible au Domaine : $e \leadsto_d e'$ si (i) le domaine admissible de $e'$ contient celui de $e$ , et (ii) les valeurs de $e'$ sur le domaine de $e$ sont dans l'enclos défini de $e$ .
- Niveau Relatif au Support : Permet de raisonner sur des sous-ensembles d'environnements (ex: intervalles strictement positifs) pour récupérer des résultats locaux.

3. Contributions Clés

L'article présente six contributions majeures :

Sémantique d'enclos sensible aux tokens : Une sémantique dénotationnelle qui attribue à chaque expression son enclos garanti, distinguant explicitement la réutilisation d'un même token de l'utilisation de tokens distincts.
Judgments de réécriture sensibles au domaine : Introduction d'un jugement de réécriture sûr ( $\leadsto_d$ ) qui exige que la cible soit admissible partout où la source l'est. Cela rend la réécriture directionnelle (non symétrique) et non transitive en général.
Théorèmes de réduction et de récupération :
- Sur les fragments universellement admissibles (pas de division ou dénominateurs non nuls), la théorie unifiée se réduit à la théorie basée sur la provenance.
- Des théorèmes de récupération internalisent des règles classiques (cancellation, soustraction de fond, division auto sur intervalles positifs) dans la couche relative au support.
Résultats de stricte directionnalité : Démonstration que la présence de singularités accessibles rend la simplification strictement unidirectionnelle. La réécriture sûre n'est pas transitive : une chaîne de simplifications sûres localement peut échouer globalement si les domaines ne sont pas vérifiés à chaque étape.
Théorème d'insuffisance : Preuve formelle que ni la provenance seule, ni la définissabilité seule ne suffisent. Effacer l'identité des tokens (provenance) ou ignorer les singularités (définissabilité) effondre des distinctions de classes de réécriture cruciales.
Mécanisation Lean 4 : L'ensemble de la théorie (143 théorèmes, 45 définitions, ~2700 lignes de code) est formalisé et vérifié sans aucune hypothèse non prouvée (sorry-free).

4. Résultats Principaux

Échec de l'égalité commune : Deux expressions peuvent être égales sur leur domaine commun ($DomainEqual$) sans être interchangeables. Par exemple, $x/x$ et $(x-1)/(x-1)$ sont tous deux égaux à 1 là où ils sont définis, mais leurs domaines de définition sont disjoints (l'un exclut 0, l'autre 1). Aucune ne peut remplacer l'autre de manière sûre.
Non-transitivité : La réécriture sûre n'est pas transitive. Un exemple concret montre que $A \leadsto_d B$ et $B \leadsto_d C$ ne garantissent pas $A \leadsto_d C$ , car le domaine de $A$ peut être trop petit pour contrôler le comportement de $C$ sur les points critiques introduits par $B$ .
Classification Positive :
- Annulation (Cancellation) : $Meas(t) - Meas(t) \to 0$ est une équivalence complète. $Meas(t_1) - Meas(t_2) \to 0$ n'est qu'une réécriture unidirectionnelle (sûre seulement dans un sens).
- Soustraction de fond : $(s + b) - b \to s$ n'est valide que si $b$ est le même token.
- Division auto : $Meas(t)/Meas(t) \to 1$ n'est une équivalence que si l'intervalle de mesure est strictement positif (excluant 0). Si l'intervalle inclut 0, la réécriture est unidirectionnelle (simplification sûre, mais l'inverse introduit une singularité).
Insuffisance des approches partielles : Un comparateur aveugle aux tokens (qui ne voit que les intervalles) ne peut pas distinguer entre des paires interchangeables et des paires non interchangeables, même avec une analyse de domaine.

5. Signification et Impact

Ce travail établit que la réécriture sûre pour les expressions de mesure nécessite une approche binaire combinant :

La provenance (suivi de l'identité des observations).
La définissabilité (suivi des singularités et des domaines de validité).

L'article démontre qu'aucune sémantique basée uniquement sur les valeurs, uniquement sur la provenance, ou uniquement sur l'accord des domaines communs ne peut supporter une classification de réécriture sûre.

Implications pratiques :

Les optimiseurs symboliques pour les pipelines scientifiques ne peuvent pas appliquer d'algèbre standard aveuglément. Ils doivent annoter les expressions avec des tokens et vérifier les conditions de domaine à chaque étape.
La théorie fournit une base formelle pour construire des simplificateurs certifiés qui évitent les erreurs subtiles liées à la réutilisation de données ou à l'introduction de singularités.
La formalisation complète en Lean 4 offre une référence de vérité pour les futurs travaux sur l'arithmétique des intervalles, l'analyse dimensionnelle et la vérification formelle de code scientifique.

En résumé, l'article remplace l'intuition algébrique par une théorie rigoureuse où "l'égalité" est remplacée par des relations de réécriture conditionnelles, garantissant que les transformations mathématiques restent valides dans le contexte physique des mesures.

1. Le Problème : Pourquoi x−xx - xx−x n'est pas toujours égal à 0 ?