Quick Facts
- Two Units (of the same quantity) are equivalent if by replacing one with the other you achieve equivalent numerical results when doing quantity calculus.
- Instances of
Unit
must hold an instance of UnitConverter
.
UnitConverters
represent transformations.
UnitConverters
allow composition, such that composing 2 UnitConverters
is equivalent to composing their transformation functions.
- Two
UnitConverters
of same type can be equivalent but are not in general, e.g. they may not be equivalent because of different prefix.
Suppose we have UnitConverter
types A,B,C.
Let S be the set of UnitConverter
types available.
S:= {A,B,C}
Now if we pick any x
and any y
from S
we need to know
- whether
x
commutes with y
, such that a composition x.y is equivalent to y.x
x.y =?= y.x
- whether there are any simplification rules
x.y
-> x
or x.y
-> y
or similar.
- whether one instance of x is equivalent to another instance of x
Given this information we are ready to state a Word Problem
[1] for any given pair of Units, for example:
Suppose we know A commutes with B, but C does not commute with any other
A.B == B.A
A.C != C.A
B.C != C.B
Suppose we know C composes with C, such that C.C can be simplified to another C
C.C -> C
Suppose we have a UnitConverter p
created by composition of types A, B and C (namely a0, b0 and c0).
p:= b0.a0.c0 (with type composition B.A.C)
Suppose we have a UnitConverter q
created by another composition of types A, B and C (namely a2, b2, c1 and c2).
q:= a2.b2.c1.c2 (with type composition A.B.C.C)
We would then apply Term Rewriting
rules to the type compositions of p
and q
until we find that these are equivalent (or not). Ideally we have such rules that produce a normal form
.
p: B.A.C -> A.B.C
q: A.B.C.C -> A.B.C
Given
p: a0.b0.c0
q: a2.b2.(c1.c2)
then p
is-equivalent-to q
, only if all these hold true
a0 is-equivalent-to a2
b0 is-equivalent-to b2
c0 is-equivalent-to c1.c2
If the Term Rewriting
rules are carefully designed to always produce a normal form
, then the Unit-1 is-equivalent-to Unit-2 problem is decidable. Otherwise it's not for the general case.
[1] https://en.wikipedia.org/wiki/Word_problem_(mathematics)
Needs #39