💻 computer science

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

Este artículo presenta una semántica unificada que rastrea el origen y la definibilidad de expresiones con unidades de medida, demostrando que la igualdad algebraica ordinaria no es un principio de reescritura válido y estableciendo un marco formalizado en Lean 4 para reescrituras seguras y unidireccionales.

Autores originales: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Publicado 2026-04-10

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que tienes un laboratorio de cocina muy preciso. En este laboratorio, no solo te importa cuánto azúcar tienes, sino de dónde salió ese azúcar y si puedes usarlo sin que la receta explote.

Este artículo científico es como una "guía de seguridad" para las matemáticas que usan los científicos cuando trabajan con mediciones reales (como la temperatura, la velocidad o la cantidad de una sustancia).

Aquí está la explicación sencilla, usando analogías:

1. El Problema: La Igualdad Matemática "Miente"

En la escuela, aprendemos que $x - x = 0$ y que $x / x = 1$ . Siempre es verdad, ¿verdad?
No, cuando trabajas con mediciones reales.

El paper dice que si usas las reglas de matemáticas normales para simplificar fórmulas científicas, a veces cometes errores graves. Hay dos "trampas" principales:

Trampa A: El "Fantasma" de la Origen (Proveniencia)

Imagina que mides la temperatura de tu sopa dos veces.

Escenario 1: Usas el mismo termómetro, en el mismo momento, y anotas el número dos veces en tu fórmula.
- Matemática: $T - T = 0$ . Es correcto. Es la misma cantidad de calor.
Escenario 2: Mides la sopa con un termómetro, luego mides otra sopa (o la misma sopa un segundo después) con otro termómetro. Aunque ambos marquen "80 grados", son dos mediciones diferentes.
- Matemática: Si restas $T_1 - T_2$ , el resultado no es necesariamente 0. Podría ser 0.1 o -0.2.

La analogía: Es como si tuvieras dos billetes de 10 dólares.

Si tomas el mismo billete y lo restas de sí mismo, te quedas con 0.
Si tomas un billete de tu bolsillo y otro de la mesa (ambos de 10 dólares) y los restas, no sabes si son exactamente el mismo billete físico. En el mundo de las mediciones, importa de dónde viene cada número. Si olvidas el "origen" (proveniencia), la matemática te miente.

Trampa B: El "Hoyo" en el Camino (Definición)

Imagina que tienes una fórmula que divide un número entre sí mismo: $x / x$ .

Si $x$ es 5, el resultado es 1.
Si $x$ es 100, el resultado es 1.
Pero, ¿qué pasa si $x$ es 0? ¡Dividir entre cero es imposible! La fórmula se rompe.

La analogía: Imagina que estás construyendo un puente.

La fórmula $x/x$ es como un puente que funciona perfecto en todas las carreteras, excepto en un punto donde hay un abismo (el cero).
La fórmula "1" es un puente que funciona en todas partes, incluso donde está el abismo.
Si cambias el puente con abismo ( $x/x$ ) por el puente seguro (1), estás arriesgándote a que alguien caiga al abismo si la medición llega a ser cero.
El paper dice: No puedes simplificar $x/x$ a 1 si existe la posibilidad de que $x$ sea cero. A veces, simplificar es peligroso.

2. La Solución: El "Detective" de Fórmulas

Los autores crearon un nuevo sistema para revisar las fórmulas científicas antes de simplificarlas. Este sistema actúa como un detective que hace dos preguntas antes de dejar pasar cualquier cambio:

¿Son los mismos ingredientes? (Proveniencia): ¿Estoy reutilizando la misma medición o son dos mediciones distintas que se parecen?
¿Es seguro el camino? (Definición): ¿Hay algún punto donde la fórmula se rompa (división por cero) que no tenga la fórmula original?

3. Las Reglas de Oro del Paper

El paper demuestra tres cosas importantes con un lenguaje muy riguroso (y probado por una computadora llamada Lean 4):

Regla 1: La dirección importa.
A veces puedes simplificar una fórmula para hacerla más segura (quitar un riesgo), pero nunca puedes hacer lo contrario.
- Ejemplo: Puedes cambiar $x/x$ por $1$ solo si sabes con certeza que $x$ nunca será cero. Si no lo sabes, no puedes hacerlo. Es como quitar un letrero de "Peligro" solo si estás 100% seguro de que no hay peligro.
Regla 2: No todo lo que parece igual, es igual.
Dos fórmulas pueden dar el mismo resultado en el 99% de los casos, pero si una tiene un "hoyo" (riesgo de división por cero) y la otra no, no son intercambiables. No puedes usar una en lugar de la otra.
Regla 3: Necesitas los dos ojos.
Si solo miras "de dónde viene el dato" (proveniencia) pero ignoras si la fórmula explota, fallas. Si solo miras si la fórmula explota pero ignoras de dónde viene el dato, también fallas. Necesitas ambas cosas para estar seguro.

4. ¿Por qué es importante esto?

Los científicos usan computadoras para simplificar fórmulas complejas automáticamente (como cuando usas una calculadora científica o un software de ingeniería).

Si el software usa las reglas matemáticas antiguas (donde $x-x$ siempre es 0), podría dar resultados incorrectos en experimentos reales.
Este paper ofrece las reglas correctas para que los programas de computadora sepan cuándo es seguro hacer un cambio y cuándo es peligroso.

En resumen

Imagina que las fórmulas científicas son recetas de cocina.

La vieja matemática dice: "Si pones dos huevos y los quitas, no hay huevos". (Correcto).
La nueva matemática dice: "Si usaste el mismo huevo dos veces en la receta, al quitarlo no hay nada. Pero si usaste dos huevos diferentes que se parecen mucho, al quitarlos podría quedar un poco de yema o clara. Además, si la receta dice 'dividir por cero', ¡no la hagas, o la cocina explota!".

Los autores han creado un manual de seguridad, probado por una computadora, para que nadie se queme la cocina al simplificar las recetas del universo.

Aquí presento un resumen técnico detallado del artículo "When Equality Fails as a Rewrite Principle: Provenance and Definedness for Measurement-Bearing Expressions", estructurado según los puntos solicitados.

1. El Problema: La Falacia de la Igualdad Algebraica en Mediciones

El artículo aborda un problema fundamental en la simplificación de expresiones científicas que contienen mediciones: la igualdad algebraica estándar no es un principio de reescritura seguro (sound). En el contexto de datos de medición, reemplazar una expresión por otra "algebraicamente equivalente" puede ser incorrecto debido a dos modos de fallo que a menudo se estudian por separado, pero que aquí se demuestran como conjuntamente necesarios:

Procedencia (Provenance):
- En las matemáticas estándar, $x - x = 0$ . Sin embargo, en mediciones, si $x$ representa una misma observación (un único "token" de medición), el resultado es 0. Pero si $x_1$ y $x_2$ son dos observaciones independientes (aunque con el mismo instrumento y rango de incertidumbre), $x_1 - x_2$ no es necesariamente 0.
- Los tratamientos formales clásicos (como el análisis dimensional o la aritmética de intervalos estándar) son "ciegos a la procedencia": no distinguen entre la reutilización de un mismo valor oculto y el uso de dos valores distintos pero similares.
Definición (Definedness):
- La división introduce singularidades. Dos formas algebraicas pueden coincidir donde ambas están definidas, pero diferir en dónde están definidas.
- Ejemplo: $x/x$ es igual a 1 donde $x \neq 0$ , pero la constante 1 está definida en todo el dominio. Reemplazar 1 por $x/x$ introduce una singularidad artificial. La dirección de la simplificación importa: eliminar una singularidad es seguro, pero introducirla no lo es.
- Además, dos expresiones pueden ser "la misma función" en su dominio común, pero tener estructuras de singularidades incomparables, bloqueando el reemplazo en cualquier dirección.

El objetivo del trabajo es desarrollar un marco unificado que precise estos fallos y clasifique cuándo un reemplazo es seguro.

2. Metodología y Marco Semántico Unificado

Los autores proponen una semántica formal que integra el seguimiento de la procedencia y la definición. La metodología se basa en los siguientes pilares:

Lenguaje de Expresiones y Tokens:
- Se define un lenguaje mínimo con hojas que son constantes racionales exactas o cantidades medidas.
- Cada hoja medida lleva un token opaco ( $t$ ) que identifica el evento de observación, un intervalo racional ( $I$ ) que acota el valor exacto oculto, y una dimensión física.
- La identidad del token es crucial: si dos hojas comparten el mismo token, deben evaluar al mismo valor exacto en cualquier entorno consistente.
Semántica de Enclosure (Cerradura) Sensible a Tokens:
- Se define un entorno de tokens $\sigma$ que asigna un valor racional exacto a cada token.
- Enclosure Garantizado ($Encl(e)$): El conjunto de todos los valores realesizables por entornos que son consistentes con los tokens de la expresión. Esto captura la procedencia.
Dominios Admisibles y Definición:
- Se introduce el predicado WellDefined, que verifica que ningún subexpresión de división tenga un denominador cero en un entorno dado.
- Dominio Admisible ($AdmDom(e)$): El conjunto de entornos que son consistentes con los tokens y donde la expresión está bien definida (sin divisiones por cero).
- Enclosure Definido ($DefinedEncl(e)$): El conjunto de valores obtenidos solo sobre el dominio admisible.
Juicios de Reescritura:
- Nivel de Enclosure: Basado en la inclusión de conjuntos de valores ( $Encl(e') \subseteq Encl(e)$ ).
- Nivel Sensible al Dominio: Introduce la Reescritura Segura al Dominio ( $e \rightsquigarrow_d e'$ $e ⇝_{d} e^{'}$ ), que requiere:
  1. $AdmDom(e) \subseteq AdmDom(e')$ (el objetivo debe ser admisible donde el origen lo es).
  2. Los valores del objetivo en el dominio del origen deben estar dentro del enclosure definido del origen.
- Nivel Relativo al Soporte: Permite evaluar la admisibilidad sobre un subconjunto arbitrario de entornos, conectando resultados locales (ej. intervalos positivos) con la clasificación global.

3. Contribuciones Clave

El artículo presenta seis contribuciones principales:

Semántica de Enclosure Sensible a Tokens: Un modelo denotacional que asigna a cada expresión su "enclosure garantizado", diferenciando explícitamente entre reutilización de tokens y uso de tokens distintos.
Juicios de Reescritura Sensibles al Dominio: Definición de una reescritura segura que impone restricciones de contención de dominio. Se demuestra que esta relación no es transitiva, lo que significa que una cadena de simplificaciones locales seguras no garantiza que la simplificación global compuesta sea segura.
Teoremas de Reducción y Recuperación:
- Se demuestra que en el fragmento "universalmente admisible" (sin divisiones o denominadores alejados de cero), la teoría unificada colapsa a la teoría basada solo en procedencia.
- Se internalizan familias positivas de reescritura (cancelación, sustracción de fondo, división propia de intervalos positivos) dentro de la capa relativa al soporte.
Resultados de Estricticidad (Strictness):
- Una vez que las singularidades son alcanzables, la simplificación que elimina una singularidad es unidireccional (segura solo en una dirección).
- Expresiones con estructuras de singularidades incomparables bloquean la reescritura en ambas direcciones, incluso si coinciden funcionalmente en su dominio común.
Teorema de Insuficiencia: Se demuestra que borrar la identidad de los tokens (ignorando la procedencia) colapsa distinciones que la definición por sí sola no puede recuperar, y viceversa. Ninguna de las dos dimensiones por separado es suficiente para una clasificación segura.
Formalización en Lean 4: Todas las definiciones y teoremas (143 teoremas y 45 definiciones en ~2,700 líneas) están formalizados en Lean 4 sin errores (sorry-free), proporcionando una certificación mecánica de la teoría.

4. Resultados Principales

Fallo de la Transitividad: La reescritura segura al dominio no es transitiva. Un ejemplo mecánico muestra que $A \rightsquigarrow_d B$ y $B \rightsquigarrow_d C$ no implican $A \rightsquigarrow_d C$ , porque el dominio de $A$ puede ser demasiado pequeño para controlar el valor del objetivo final en ciertos puntos críticos.
Separación de Singularidades: Para una expresión $x/x$ con intervalo $[0, 1]$ , la relación con la constante 1 es estrictamente unidireccional ( $x/x \rightsquigarrow_d 1$ es válido, pero $1 \rightsquigarrow_d x/x$ no lo es) porque el dominio de $x/x$ excluye el cero.
No-Colapso (Non-Collapse): Se presentan casos donde dos expresiones son "la misma función" en su dominio común (ej. $x/x$ y $(x-1)/(x-1)$ ), pero ninguna puede reemplazar a la otra porque sus dominios admisibles son incomparables (uno excluye 0, el otro excluye 1).
Insuficiencia Conjunta: La clasificación de reescritura segura requiere simultáneamente el seguimiento de la procedencia (tokens) y la definición (dominios). Ignorar cualquiera de los dos lleva a clasificaciones erróneas.

5. Significado e Impacto

Este trabajo tiene implicaciones significativas para la computación científica y la verificación formal:

Más allá de la Aritmética de Intervalos: Mientras que la aritmética de intervalos clásica y el álgebra afín se centran en la "estrechez" de los límites (tightness) y la dependencia de variables, este marco aborda la seguridad de la reescritura basada en la identidad de la observación y la validez del dominio.
Fundamento para Optimizadores Simbólicos: Proporciona la base teórica necesaria para que los optimizadores de fórmulas científicas realicen simplificaciones seguras. Muestra que las optimizaciones locales no pueden aplicarse ciegamente; cada paso debe verificar la procedencia de los tokens y la admisibilidad del dominio.
Certificación Formal: La formalización completa en Lean 4 establece un nuevo estándar de rigor para la semántica de expresiones de medición, eliminando ambigüedades sobre cuándo es válido cancelar términos o simplificar divisiones.
Limitaciones y Futuro: El trabajo se centra en singularidades por división (excluyendo desbordamientos o errores de tipo) y utiliza números racionales ( $\mathbb{Q}$ ) en lugar de reales ( $\mathbb{R}$ ) para garantizar la decidibilidad. El sistema de dimensiones es sintáctico y podría extenderse a un sistema de unidades más rico.

En conclusión, el paper demuestra que la igualdad matemática es insuficiente para la manipulación de datos de medición y propone un marco semántico unificado, riguroso y formalmente verificado que integra la procedencia y la definición como pilares inseparables para la reescritura segura.