Skip to content

Unit Equivalence

Jump to bottom
Andi Huber edited this page Oct 27, 2018 · 25 revisions

Quick Facts

  • Two Units (of the same quantity) are equivalent if by replacing one with the other we achieve equivalent numerical results with quantity calculus.
  • Instances of Unit must hold an instance of UnitConverter.
  • UnitConverters represent transformations x -> f(x).
  • UnitConverters allow composition, such that composing 2 UnitConverters is equivalent to composing their transformation functions (a, b) -> a ○ b, or more verbose ...
    given f: x->f(x), g: x->g(x), then f ○ g ≡ x->g(f(x)).
  • Two UnitConverters of same type can be equivalent but are not in general, e.g. they may not be equivalent because of different parameter values.

The 'Word Problem'

For in-depth material on 'Term Rewriting' and 'Normal-Form' we refer to Wikipedia

Decide-ability of 'Equivalence'

Given two unit-conversions (where each generally speaking is a sequence of transformation steps), it cannot always be decided, whether these are equivalent. We can only check whether two sequences of transformations can be reduced to the 'same' (equal) 'Normal-Form'.

Take for example Add(3) ○ Mul(2) ○ Add(-7) === Mul(2) ○ Add(-1), where the left sequence of transformations is mathematically speaking equivalent to the right sequence of transformations. But due to limitations of transformation composition algorithms, these two might have different 'Normal-Forms', such that a check for equality results in false, while it should be true.

We conclude that equivalence checks might be wrong if they result in false, but on the other hand they are guaranteed to be right, if they results in true.

Implementing a Normal-Form

Composition Table

NormalFormOrder Composition POWER RATIONAL PI MULTIPLY ADD LOG EXP
1 POWER If same base → POWER, Else → LBO RATIONAL NFO NFO COMP COMP COMP
2 RATIONAL # RATIONAL NFO NFO COMP COMP COMP
3 PI # # PI NFO COMP COMP COMP
4 MULTIPLY # # # MULTIPLY COMP COMP COMP
5 ADD # # # # ADD COMP COMP
6 LOG # # # # # COMP ID
7 EXP # # # # # # COMP

# ... Omitted due to symmetry typeOf(a ○ b) ≡ typeOf(b ○ a)

ID ... IDENTITY x -> x
POWER ... PowerOfIntConverter x -> x * base^exponent
RATIONAL ... RationalConverter x -> x * dividend/divisor
PI ... PowerOfPiConverter x -> x * π^exponent
MULTIPLY ... MultiplyConverter x -> x * factor
ADD ... AddConverter x -> x + offset
LOG ... LogConverter x -> log(base, x), or if(base=Math.E) x -> ln(x)
EXP ... ExpConverter x -> base^x, or if(base=Math.E) x -> e^x

COMP ... composition (a, b) -> a ○ b
LBO ... composition with order (lower base first)
(a, b) -> sort(a, b).first ○ sort(a, b).last
NFO ... composition with order (lower normal-form-order first)
(a, b) -> sort(a, b).first ○ sort(a, b).last

Simplification Rules

  1. Mul(r) ○ Add(s) ○ Mul(t) ≡ Mul(r * t) ○ Add(s * t)
  2. Add(r) ○ Mul(s) ○ Add(t) ≡ Mul(s) ○ Add(r * s + t)

Proof

  1. Mul(r) ○ Add(s) ○ Mul(t) ≡ x -> ( (x * r) + s ) * t = x r t + s t ≡ Mul(r * t) ○ Add(s * t)
  2. Add(r) ○ Mul(s) ○ Add(t) ≡ x -> ( (x + r) * s ) + t = x s + r s + t ≡ Mul(s) ○ Add(r * s + t)

Composition Examples

Given the composition lookup table above, we define for every pair of transformations how to derive the composition result.

Suppose Add(3) ○ Add(2) ≡ x -> (x + 3) + 2 = x + 5 which can be simplified to Add(5), meaning that the original and the simplified composition are equivalent. We conclude that for the Add transformation we can always simplify Add(r) ○ Add(s) ≡ Add(r + s).

Suppose Mul(3) ○ Mul(2) ≡ x -> (x * 3) * 2 = x * (3 * 2) which can be simplified to Mul(6), meaning that the original and the simplified composition are equivalent. We conclude that for the Mul transformation we can always simplify Mul(r) ○ Mul(s) ≡ Mul(r * s).

Suppose Add(3) ○ Mul(2) ○ Add(-7) ≡ x -> ( (x + 3) * 2 ) -7 = 2x - 1 which can be simplified to Mul(2) ○ Add(-1), meaning that the original and the simplified composition are equivalent (see Simplification Rules above).

Suppose Power(10^3) ○ Rational(20/1) ≡ x -> (x * 10^3) * 20 which according to the lookup table results in Rational(20000/1), which can not be further simplified and hence is a normal-form.

Suppose we swap the order of the previous to Rational(20/1) ○ Power(10^3) ≡ x -> (x * 20) * 10^3 which according to the lookup table also results in Rational(20000/1), which can not be further simplified and hence is a normal-form.

Given the 2 previous examples we can now state the equivalence Power(10^3) ○ Rational(20/1) ≡ Rational(20/1) ○ Power(10^3) because both simplify (by using the lookup table) to the same normal-form.

Commutativity of Addition and Multiplication Compositions

Suppose a composition C0 ○ C1 ○ ... ○ X ○ Y ○ ... Cn. Given that X and Y represent a multiplication transformation, then X and Y might always be swapped within a sequence, provided X and Y are consecutive:
C0 ○ C1 ○ ... ○ X ○ Y ○ ... Cn ≡ C0 ○ C1 ○ ... ○ Y ○ X ○ ... Cn

The same applies to the addition transformation.

Implementing a 'Normal-Form' yielding Composition Algorithm

Given a sequence of transformations (eg. Add(3) ○ Mul(2) ○ Mul(-1) ○ Add(-7) ), where order matters, we form a permutation group of all permutations 'reachable' through 'allowed' swapping of transformations within this sequence.

Swapping is allowed for 2 consecutive transformations (a, b) that commute with each other (a o b === b o a).

We search this permutation group for any sequence of transformations, that allows simplification: For every pair of consecutive transformations within a sequence, check whether a simplification is possible, then apply simplification and start over until no more simplification is found.

Finally sort according to normal-form order.

Clone this wiki locally