Unit Equivalence

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.

The 'Word Problem'

//TODO Term Rewriting, Normal-Form

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 -> x -> log(base, x)
EXP ... ExpConverter x -> x -> base^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