In many computing situations, we might like to associate a unit expression with a number, for example

As humans, we’d also like it if our computing tools could understand that many unit expressions are equivalent.

Better yet, it would be very useful for our tools to know that some unit expressions are convertable.

Equally important, we wish to define the idea that units may not be compatible.

It turns out that there is a straightforward and efficient way to define such an algorithmic unit analysis. Start with the following definition:

For example, $base(meter)$ declares the atom meter to be a base unit. Every base unit also implicitly defines an abstract quantity. The term $base(meter)$ defines the abstract quantity of Length; $base(second)$ defines an abstract quantity of Duration, and so on.

Unit expressions may be constructed from these atomic base units, inductively:

In our constructions above, we introduced a special atom $\emptyset$ represents a unitless expression where all units have canceled. For example $meter / meter$ is equivalent to $\emptyset$. We also introduced the idea of a derived unit, where a named unit d is declared as equivalent to $c e$. For example we can use a derived unit to define a liter as a unit of volume: $derived(liter, meter^3, 1/1000)$.

Next, I will define the notion of the canonical form of a unit expression. Intuitively, an expression’s canonical form is an equivalent representation expressed purely as a product of a numeric value with base units raised to non-zero powers. For example, the canonical form of $meter / (second^2)$ is $1 \ meter^1 second^{-2}$, and the canonical form of $liter / second$ is $(1/1000) \ meter^3 second^{-1}$.

The canonical form of a unit expression $e \triangleq canonical(e)$ is recursively defined, as follows.

By convention, a canonical form of $c \times \emptyset$ represents the unitless state where all other powers of unit atoms have canceled out to zero, and so for example $canonical(meter / meter) = 1 \ \emptyset$, and $canonical(\emptyset \times second) = 1 \ second^1$

We are now in a position to define some algorithmic unit analysis! A fundamental question of unit analysis is whether two unit expressions are convertable, and if so, what is the conversion factor between them. Using the above definition of canonical forms, it is straightforward to capture this idea mathematically:

Consider this example: Is $foot / second / second$ convertable to $meter / (second^2)$ ? Allowing that we’ve declared $base(meter)$, $base(second)$ and $derived(foot, meter, 0.3048)$, then:

and so the answer is yes! These unit expressions are convertable, and 0.3048 is the coefficient of conversion.

Likewise, this algorithm can conclude when units are not compatible:

This approach to the question of unit convertability is very amenable for use in computing. The canonical form of a unit expression is easily representable in various data structures. For example, the canonical form $1 \ meter^1 second^{-2}$ can be represented as the sequence [(meter, 1), (second, -2)]. It might also be represented as a mapping, such that map[meter] -> 1 and map[second] -> -2. The inductive definition of unit expressions is straightforward to implement in most modern computing languages, as is the recursive definition of the canonical function itself.

I have been experimenting with an implementation of these algorithmic definitions for defining unit analysis as a static typing system for Scala. However, by defining these concepts mathematically, my hope is that it may make applying computational unit analysis more amenable for any programming language that can support it.