Solving Unit-1 is-equivalent-to Unit-2

[andi-huber]

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

1. whether x commutes with y, such that a composition x.y is equivalent to y.x
   x.y =?= y.x
2. whether there are any simplification rules x.y -> x or x.y -> y or similar.
3. 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

[andi-huber]

So I'd conclude, for any implementers to consider

• designing such a normal form
• and let UnitConverter.concatenate(UnitConverter converter) always produce a normal form

[keilw]

Thanks for pointing that out. Either for the Spec or UoM Guidebook I assume some of this information will also help.

[desruisseaux]

I propose an amendment to the first point:

• Two Units of the same quantity are equivalent if by replacing one with the other you achieve equivalent numerical results when doing quantity calculus.

For example kilometre and kilowatt have the same UnitConverter to their system unit (their converters can even be the same instance) but are not equivalent.

I agree that implementations should produce normal forms. In the case of unit conversions, this is simplified by the fact that the vast majority of conversions are linear, in which case commutativity (among other) applies. However one difficulty we have with current API is that UnitConverter.isLinear() method specification is wrong. Its current specification said:

Indicates if this converter is linear. A converter is linear if:

• convert(u + v) == convert(u) + convert(v)
• convert(r * u) == r * convert(u)

It is not the usual definition of linear conversion since a converter of the form y = scale * x + offset would not comply to this definition. This prevent implementations to detect e.g. that commutativity applies for Celsius units for instance.

[andi-huber]

@desruisseaux thanks for the hint, I've updated the description.

[andi-huber]

Regarding UnitConverter.isLinear(): This could be superseded by something like UnitConverter.characteristics() to return a set of enums like Java's Collector does ...
https://docs.oracle.com/javase/8/docs/api/java/util/stream/Collector.Characteristics.html

[keilw]

We could add new methods but should not remove any without deprecating them first. Pulling MetricPrefix from the RI into the API was already a bit of a challenge but i was not removed and the package name also changed, so existing code may be migrated with little changes to impor statements. Completely removing a method would only work another version down the road.

[andi-huber]

Sorry, I did not mean to start a naming discussion.
Just as a side-note: isLinear will be used rather by API implementers than by API users.

[keilw]

Actually @desruisseaux started it already #39

[keilw]

@andi-huber Is there anything to do here?

[andi-huber]

I think we can close this.

[keilw]

Thanks