When Equality Fails as a Rewrite Principle: Provenance and Definedness for Measurement-Bearing Expressions
2026-04-08 • Logic in Computer Science
Logic in Computer ScienceProgramming Languages
AI summaryⓘ
The authors explain that normal algebra rules don’t always work correctly when dealing with expressions that involve measurements or observations. They introduce a new way to keep track of where values come from and when expressions are valid. Their approach helps decide when you can safely replace parts of an expression without changing its meaning, even when division or other operations complicate things. All their definitions and proofs are carefully verified using the Lean 4 proof assistant.
algebraic equalitymeasurement-bearing expressionsprovenancedefinednessrewriting rulestoken-sensitive enclosureadmissible domainLean 4simplificationreduction theorems
Authors
David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz
Abstract
Ordinary algebraic equality is not a sound rewrite principle for measurement-bearing expressions. Reuse of the same observation matters, and division can make algebraically equal forms differ on where they are defined. We present a unified semantics that tracks both provenance and definedness. Token-sensitive enclosure semantics yields judgments for one-way rewriting and interchangeability. An admissible-domain refinement yields a domain-safe rewrite judgment, and support-relative variants connect local and global admissibility. Reduction theorems recover the enclosure-based theory on universally admissible supports. Recovery theorems internalize cancellation, background subtraction, and positive-interval self-division. Strictness theorems show that reachable singularities make simplification one-way and make common-domain equality too weak for licensed replacement. An insufficiency theorem shows that erasing token identity collapses distinctions that definedness alone cannot recover. All definitions and theorems are formalized in sorry-free Lean 4.