Unit Equivalence

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'

References: Wikipedia
//TODO Term Rewriting, Normal-Form

Decide-ability of 'Equivalence'

//TODO can not always be decided, we can only check whether two sequences of transformations (when in 'normal-form') represent the same transformation ...

Implementing a Normal-Form

Composition table, yielding a normal-form.

NormalFormOrder	Composition	POWER	RATIONAL	MULTIPLY	PI	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
4	MULTIPLY	#	#	MULTIPLY	NFO	COMP	COMP	COMP
3	PI	#	#	#	PI	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 ... PowersOfIntConverter x -> x * base^exponent
RATIONAL ... RationalConverter x -> x * dividend/divisor
PI ... PowersOfPiConverter 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

Composition Examples

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. However this requires algebraic simplification, which we don't implement. Instead we say the composition Add(3) ○ Mul(2) ○ Add(-7) can not be further simplified by 'standard' means and hence is a normal-form.

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

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 that 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.

Also note from the mixed example above that equivalence of these Add(3) ○ Mul(2) ○ Add(-7) ≡ Mul(2) ○ Add(-1) is given, but since the left-hand side and the right-hand side resolve to different normal-forms, the check for equivalence will be negative.

Implementing a Simplifier, that produces a Normal-Form

//TODO pseudo code of the solve algorithm