💻 computer science

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

Dieses Papier stellt eine formale Semantik vor, die sowohl die Herkunft als auch die Definiertheit von Messausdrücken verfolgt, um zu zeigen, dass die gewöhnliche algebraische Gleichheit kein sicheres Umformungsprinzip ist, und liefert damit eine fundierte Basis für ein- und zweiseitige Umformungsregeln, die in Lean 4 vollständig formalisiert wurde.

Ursprüngliche Autoren: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Veröffentlicht 2026-04-10

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Wenn Gleichheit nicht mehr reicht: Warum bei Messungen „A ist B" manchmal falsch ist

Stellen Sie sich vor, Sie sind ein Koch, der ein Rezept für einen perfekten Kuchen schreibt. In der normalen Mathematik (der „Algebra") gilt: Wenn Sie zwei gleiche Zutaten haben, können Sie sie austauschen, ohne dass sich das Ergebnis ändert. $x - x$ ist immer $0$. $x / x$ ist immer $1$.

Aber in der realen Welt der Messungen (z. B. in der Wissenschaft oder Technik) funktioniert das nicht so einfach. Dieses Papier erklärt, warum wir vorsichtiger sein müssen, wenn wir Formeln mit Messwerten vereinfachen. Es gibt zwei Hauptgründe, warum das einfache „Austausch-Prinzip" hier scheitert:

1. Das Problem der „Herkunft" (Provenance)

Stellen Sie sich vor, Sie wiegen eine Kartoffel.

Szenario A: Sie wiegen dieselbe Kartoffel zweimal. Wenn Sie dann die beiden Gewichte voneinander abziehen ($Gewicht - Gewicht$), erhalten Sie exakt $0$. Das ist logisch, denn es ist dieselbe Kartoffel.
Szenario B: Sie nehmen zwei verschiedene Kartoffeln, die zufällig auf der Waage fast das gleiche Gewicht anzeigen (z. B. beide zwischen 100g und 102g). Wenn Sie diese beiden Werte voneinander abziehen, ist das Ergebnis nicht garantiert $0$. Die eine könnte 100g sein, die andere 102g. Das Ergebnis wäre 2g.

Die Metapher:
In der Mathematik sind Variablen wie leere Behälter. In der Wissenschaft sind Messwerte wie Fingerabdrücke.

Wenn Sie in einer Formel denselben Fingerabdruck zweimal sehen, wissen Sie: Es ist dieselbe Person.
Wenn Sie zwei Fingerabdrücke sehen, die fast identisch aussehen (gleiche Maße, gleiche Unsicherheit), aber unterschiedliche Finger sind, sind es zwei verschiedene Personen.
Das Papier sagt: Ein Computer darf nicht einfach $x - x$ zu $0$ vereinfachen, wenn er nicht weiß, ob das $x$ aus derselben Messung stammt oder aus zwei fast gleichen, aber getrennten Messungen. Es braucht eine Art „Etikett" (einen Token), um zu verfolgen, woher die Zahl kommt.

2. Das Problem der „Definition" (Definedness)

Stellen Sie sich vor, Sie teilen eine Torte.

Wenn Sie eine Torte durch sich selbst teilen ($Torte / Torte$), erhalten Sie 1.
Aber was passiert, wenn die Torte leer ist (Größe 0)? Dann können Sie nicht teilen. Das Ergebnis ist undefiniert.

In der reinen Mathematik sagen wir oft: „ $x/x$ ist 1". Aber in der Physik ist das nur wahr, solange $x$ nicht 0 ist. Wenn Sie die Formel $1$ durch $x/x$ ersetzen, fügen Sie plötzlich eine „Falle" ein: Die Formel funktioniert plötzlich nicht mehr, wenn $x$ 0 ist.

Die Metapher:
Stellen Sie sich eine Brücke vor.

Die Formel „1" ist wie eine breite, stabile Autobahn. Sie führt überall hin.
Die Formel „ $x/x$ " ist wie eine schmale Hängebrücke, die nur dann sicher ist, wenn kein Wasser (kein 0) unter ihr steht.
Wenn Sie die Autobahn durch die Hängebrücke ersetzen, haben Sie das Problem, dass die Brücke bei Hochwasser (wenn $x=0$ ) einstürzt. Das Papier zeigt: Man darf eine sichere Formel nicht durch eine unsichere ersetzen, nur weil sie im „normalen" Fall das Gleiche tun.

Die Lösung: Ein neuer Sicherheitsgurt

Die Autoren haben ein neues System entwickelt, das wie ein zweischichtiges Sicherheitsnetz funktioniert:

Die Spur-Verfolgung (Token-Sensitive):
Das System schaut sich jeden Messwert genau an und klebt ein unsichtbares Etikett darauf. Wenn zwei Werte dasselbe Etikett tragen, weiß das System: „Aha, das ist dieselbe Messung!" Dann darf es vereinfachen. Haben sie verschiedene Etiketten, bleibt das System skeptisch und vereinfacht nicht blind.
Der Sicherheits-Check (Admissible Domains):
Bevor das System eine Formel vereinfacht, prüft es: „Gibt es eine Situation (z. B. wenn ein Wert 0 ist), in der die neue Formel kaputtgeht, die alte aber nicht?" Wenn ja, ist der Austausch verboten.

Was bringt das alles?

Das Papier ist wie ein Regelwerk für einen sehr vorsichtigen Übersetzer.

Früher: Ein Übersetzer sagte: „ $x - x$ ist 0." (Und ignorierte, ob es dieselbe Kartoffel war).
Jetzt: Der Übersetzer sagt: „Ich darf $x - x$ nur dann zu 0 machen, wenn ich weiß, dass es dieselbe Kartoffel ist. Und ich darf $x/x$ nur dann zu 1 machen, wenn ich sicher bin, dass die Kartoffel nicht leer ist."

Das Wichtigste in einem Satz:
Man kann mathematische Formeln in der Wissenschaft nicht einfach nach den Regeln der Algebra umschreiben, ohne zu wissen, woher die Zahlen kommen und wo sie funktionieren. Wenn man diese beiden Dinge ignoriert, kann man zu falschen oder unsicheren Ergebnissen kommen.

Die Autoren haben diesen ganzen Prozess in einer Programmiersprache namens Lean 4 bewiesen, sodass kein einziger Schritt auf Vermutungen beruht – alles ist mathematisch wasserdicht. Sie zeigen uns, dass „Gleichheit" in der Welt der Messungen oft eine Illusion ist, und dass wir genau hinsehen müssen, um sicher zu bleiben.

Titel: Wenn die Gleichheit als Umformungsprinzip versagt: Herkunft und Definiiertheit für messwerttragende Ausdrücke

Autoren: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz
Formalisierung: Vollständig in Lean 4 (ohne sorry)

1. Problemstellung

Das Papier adressiert ein fundamentales Problem bei der symbolischen Vereinfachung von wissenschaftlichen Formeln, die Messwerte enthalten: Die herkömmliche algebraische Gleichheit ist kein sicheres Prinzip für Umformungen (Rewriting). Zwei spezifische Fehlermodi machen die Frage, wann ein Ausdruck durch einen anderen ersetzt werden darf, nicht-trivial:

Herkunft (Provenance): Ein konkreter Beobachtungsvorgang erzeugt einen Wert mit einer Spur seiner Herkunft. Wenn derselbe Messwert in einer Formel zweimal verwendet wird (z. B. $x - x$ ), beziehen sich beide Vorkommen auf denselben verborgenen exakten Wert. Werden jedoch zwei separate Messungen mit identischen Instrumenten und Unsicherheitsgrenzen verwendet (z. B. $x_1 - x_2$ ), müssen die zugrunde liegenden exakten Werte nicht übereinstimmen. Herkömmliche Methoden wie Dimensionsanalyse oder klassische Intervallarithmetik sind „herkunftsblind" und können diese Unterscheidung nicht treffen.
Definiiertheit (Definedness): Division führt zu Singularitäten. Algebraisch äquivalente Formen können sich darin unterscheiden, wo sie definiert sind. Zum Beispiel ist $x/x$ überall dort definiert, wo $x \neq 0$ , und ergibt 1. Die Konstante 1 ist überall definiert. Das Ersetzen von 1 durch $x/x$ führt also zu einer neuen Singularität. Die Richtung der Vereinfachung ist entscheidend: Das Entfernen einer Singularität ist sicher, das Einführen einer neuen ist es nicht.

Ein symbolischer Vereinfacher für wissenschaftliche Formeln muss beide Fehlermodi gleichzeitig berücksichtigen. Das Papier zeigt, dass weder Herkunfts- noch Definiiertheitsinformationen allein ausreichen, um sichere Umformungen zu klassifizieren.

2. Methodik und Semantischer Rahmen

Die Autoren entwickeln einen einheitlichen semantischen Rahmen, der sowohl die Herkunft (Token-Identität) als auch die Definiiertheit (Admissibilität) integriert.

Ausdrucksprache: Eine minimale Sprache mit Blättern, die entweder exakte rationale Konstanten oder gemessene Größen (Meas(t, I, d)) sind. Ein gemessenes Blatt enthält einen undurchsichtigen Token $t$ (für die Beobachtungsereignis-Identität), ein rationales Intervall $I$ (Schranken für den wahren Wert) und eine Dimension $d$ .
Token-sensitive Einschließungs-Semantik (Enclosure Semantics):
- Eine Token-Umgebung $\sigma$ weist jedem Token einen exakten rationalen Wert zu.
- Die gewährleistete Einschließung ($Encl(e)$) ist die Menge aller Werte, die durch token-konsistente Umgebungen realisierbar sind. Dies macht die Wiederverwendung desselben Tokens (gleicher verborgener Wert) vs. separate Tokens (unterschiedliche Werte) semantisch sichtbar.
Admissible Domains (Zulässige Bereiche):
- Ein Ausdruck ist an einer Umgebung $\sigma$ wohldefiniert, wenn keine Division durch Null auftritt.
- Der zulässige Bereich ($AdmDom(e)$) ist die Menge aller Umgebungen, die sowohl token-konsistent sind als auch keine Division durch Null verursachen.
- Die definierte Einschließung ($DefinedEncl(e)$) beschränkt die Auswertung auf diesen zulässigen Bereich.
Vergleichsbasis (Forgetful View): Um die Notwendigkeit von Token-Informationen zu beweisen, wird eine „herkunftsblinde" Semantik definiert, bei der Token-Informationen gelöscht werden. Dies dient als Kontrastmittel für die Unzulänglichkeits-Theoreme.

3. Umformungs-Urteile (Rewrite Judgments)

Auf Basis dieses Rahmens werden drei Ebenen von Umformungs-Urteilen definiert:

Einschließungsbasiert (Provenance-Ebene):
- $e \leadsto e'$ : Die Einschließung von $e'$ ist in der von $e$ enthalten (Verengung der Aussage).
- $e \Leftrightarrow e'$ : Äquivalenz der Einschließungen.
Domänenbewusst (Domain-Aware):
- $e \leadsto_d e'$ $e ⇝_{d} e^{'}$ : Domänen-sichere Umformung. Dies erfordert:
  1. Der zulässige Bereich von $e$ ist in dem von $e'$ enthalten ( $AdmDom(e) \subseteq AdmDom(e')$ ).
  2. Die Werte von $e'$ auf dem Bereich von $e$ liegen innerhalb der definierten Einschließung von $e$ .
- Dies führt zu einer gerichteten Beziehung: Das Entfernen einer Singularität ist sicher (erweitert den Bereich), das Einführen einer Singularität ist nicht sicher.
- Nicht-Transitivität: Im Gegensatz zur reinen Einschließung ist domänen-sicheres Umformen nicht transitiv. Eine Kette von sicheren lokalen Vereinfachungen kann global unsicher sein.
Support-relativ:
- Um lokale Ergebnisse (z. B. für positive Intervalle) in den globalen Rahmen zu integrieren, werden Admissibilität und Einschließung auf eine beliebige Unterstützungs-Menge $S$ relativiert. Dies erlaubt die Formulierung von „kontextuellen" Äquivalenzen.

4. Wichtige Beiträge und Ergebnisse

Einheitliche Theorie: Die Autoren zeigen, dass die herkunfts-basierte Theorie (Enclosure) ein Spezialfall der vereinten Theorie ist, der auf dem „universell zulässigen" Fragment (keine Divisionen oder keine Null im Nenner) gilt.
Positive Klassifikationsfamilien: Es werden spezifische Fälle identifiziert, in denen Umformungen sicher sind:
- Kürzung: $Meas(t) - Meas(t) \to 0$ ist sicher (gleicher Token), aber $Meas(t_1) - Meas(t_2) \to 0$ ist es nicht.
- Hintergrund-Subtraktion: $(s + b) - b \to s$ ist nur sicher, wenn $b$ derselbe Token ist.
- Selbst-Division: $Meas(t, I)/Meas(t, I) \to 1$ ist sicher, wenn das Intervall $I$ strikt positiv ist (keine Null).
Strenge negative Ergebnisse (Strictness Theorems):
- Einseitigkeit: Wenn Singularitäten erreichbar sind (z. B. Division durch ein Intervall, das 0 enthält), ist die Vereinfachung $x/x \to 1$ nur einseitig sicher. Die Umkehrung ist falsch.
- Nicht-Kollaps (Non-Collapse): Zwei Ausdrücke können auf ihrem gemeinsamen Definitionsbereich identisch sein, aber keiner kann den anderen ersetzen, weil ihre zulässigen Bereiche inkommensurabel sind (z. B. $x/x$ vs. $(x-1)/(x-1)$ ).
Unzulänglichkeits-Theorem (Insufficiency Theorem):
- Das Löschen der Token-Identität kollabiert wichtige Unterscheidungen. Weder reine Herkunfts-Information noch reine Definiiertheits-Information allein reicht aus. Beide sind notwendig für eine sichere Klassifikation von Umformungen.

5. Signifikanz und Formalisierung

Mechanisierung: Alle Definitionen und 143 Theoreme wurden in Lean 4 formalisiert (ca. 2.700 Zeilen Code). Das Projekt ist vollständig bewiesen („sorry-free"). Dies dient als semantische Zertifizierung, dass die Klassifikationsergebnisse korrekt sind und keine Fehler in der komplexen Domänenlogik (insbesondere bei asymmetrischen Bedingungen) übersehen wurden.
Abgrenzung: Die Arbeit unterscheidet sich von klassischer Intervallarithmetik (die sich auf die Schmalheit der Intervalle konzentriert) und Provenance-Semirings (die algebraische Zertifikate verfolgen). Der Fokus liegt hier auf der Klassifikation von Umformungen unter Berücksichtigung von Messwert-Herkunft und Singularitäten.
Praktische Implikation: Für jeden zertifizierten Vereinfacher oder Rewrite-Kalkül in wissenschaftlichen Pipelines ist es unerlässlich, sowohl die Token-Identität (Herkunft) als auch die Definiiertheit (Admissibilität) zu verfolgen. Reine algebraische Gleichheit ist für Messdaten unzureichend.

Fazit: Das Paper etabliert, dass mathematische Gleichheit als Umformungsprinzip für messwerttragende Ausdrücke versagt, sobald Wiederverwendung von Messdaten und Divisionen (Singularitäten) im Spiel sind. Eine sichere Vereinfachung erfordert eine Semantik, die sowohl die Abhängigkeit zwischen Beobachtungen als auch die Gültigkeitsbereiche der Ausdrücke explizit modelliert.