Consistency Checking by Type Inference and Constraint Satisfaction

Abstract

This paper presents a method for checking the consistency of equations involving physical units, by applying techniques similar to type inference in programming languages over a formal specification of the system to check. The checking is performed by a physical units inference system relying both on the algebraic structure of the international physical units system and a formal notation we designed to express the equations. The inference system is a three steps process: first, variables are assigned to the various expressions of the system; second, a set of equations representing the constraints of the international units system involving these variables is constructed. Finally, this set of equations is handled by a specific algorithm, which decides if the original system is consistent, and computes the physical units in a polymorphic way. We show that specializing the traditional type inference algorithms to the particular structure of the international units system boils down to solving classical linear systems symbolically.