.Open Dimensioned Numbers

. Motivation
The numbers of pure mathematics never appear `naked and unadorned` in 
practice.  They appear with units attached to them - feet, meters, inches,
centimeters, miles, yards, .... Therefore a practical mathematical notation
must provide a meaningful way for this to be done.  This set of notes set up
a suitable system loosely inspired by the PMS notation of C Gordon Bell and
Allen Newell 
.See [BellNewell70]
.See [BellNewell71]
combined with "Dimensional Analysis" as used in Applied Mathematics 
and Physics[Crank 62: John Crank, Mathematics and Industry, Oxford UP 1962].

. Also see
.Source Novak93, Conversion of Units of Measurement, IEEE Trans Software Engineering SE-21n8(pp651-661).

. Metrology
Metrology::=the science of all aspects of measurement including the theory and practice in all fields of science and technology -- however uncertain.

A standardized quantitative measurement is based on an underlying attribute,
a defined unit, a primary reference of example of the unit, some secondary
references used in practice and some methods of measurement used to get
these measurements.  For example the idea of "the inertia of an object"
is experienced when we try to move a heavy and light object, or compare
the effort to brake a truck with that of a child's toy car. This idea
is refined into the concept of inertial mass with a unit like the kilogram and
standard ways of measuring it.

In America the National Institute of Standards (NIS) is in charge of
these things
.See http://www.nist.gov/
Their Information Technology Laboratory has been working on deriving
the metrology of Information technology
.See http://www.itl.nist.gov/

The SI Units are described at
.See http://physics.nist.gov/cuu/Units/units.html
(with thanks to Vince Tilroe, February 17th 2005)

. Measurement Theory
Some measures do not have the complete set of properties of numbers.  The 
classification commonly used are: nominal, ordinal, interval, and ratio.

.Hole
. Dimensions 
We don't add feet and pounds together.  And yet we can add pounds to pounds 
and get pounds: Hence we have a large number of similar sets of arithmetic - 
one arithmetic for each dimension.  Because we can also add ounces and pounds,
each dimension has several sets of units associated with it.   The numbers in
different units are proportional, however ( 16.oz=1.lb).


Now if we multiply two lengths then we get an area - not another length.  So 
the different dimensions are also related.  Dimensional Analysis expresses all
dimensions ( length, mass, weight, velocity, force, magnetic flux,...) in 
terms of a small number of fundamental dimensions - length, mass, time, and a
few others.

DIMENSION::=Net{

BASIS::=Net{
Dimension::@Field(archimedian).  Actually, each dimension is isomorphic to the
real numbers.

 |- (partitioned): For all D1,D2:$Dimension, D1=D2 iff some D1&D2.

 Numbers::Dimension.

 |- (dgroup): GROUP($Dimension, (*), $Numbers, (/)). Given two Dimensions we 
can multiply them (*) to get another $Dimension.  Pure $Numbers act like 1 in
this multiplication and we have some kind of division as well.


A unit gives a mapping of numbers into dimensions. For instance using
'inch' as a unit of length means that `1.inch` is a measure of length,...
A set of units works exactly like a set of numbers under addition. If
Length is a dimension and inch a unit of length  `Length./inch` indicates
numbers which represent the numbers of inches of length.

In general then a unit is map from abstract numbers into dimensions that
preserves the operation of addition and the value of zero:
 For $Dimension D, Units(D) ::=(+,0)$Numbers---D.
.See http://www/dick/maths/math_11_STANDARD.html#Structure Preserving Maps

}=::BASIS.

	|- (D0): BASIS.  This just asserts the assumptions named BASIS above.

MECHANICAL_UNITS::=Net{
There are three basic physical dimensions - length, time, and mass.  A more
abstract one is that of information. We can also include angles from
geometry.  We assume that every possible dimension is expressible in terms
of these 5 component dimensions:
dim::Net{L,T,M,I,A:Rational}---$Dimension,
Number::=	dim(L=>0,T=>0,M=>0,I=>0,A=>0).

Length::=	dim(L=>1,T=>0,M=>0,I=>0,A=>0),
Mass::=  	dim(M=>1,L=>0,T=>0,I=>0,A=>0),
Time::=  	dim(T=>1,M=>0,L=>0,I=>0,A=>0),
Angle::= 	dim(T=>0,M=>0,L=>0,I=>0,A=>1),
Information::=	dim(I=>1,T=>0,M=>0,L=>0,A=>0).



Next define product and quotient of two dimensions.
 For a:D1, b:D2, a/b::=dim(a./dim-b./dim),
 For a:D1, b:D2, a*b::=dim(a./dim+b./dim).
()|-(ex1):Length*Length/Time=dim(L=>2,T=>-1,M=>0,I=>0, A=0).
()|-(ex2): For $Dimension D, D/D=Number.

 For $Dimension D, a:D, dim(a) ::=D.

 |- (D1): Number=Real.
()|-(D1.0):For $Dimension D, a:D, n:Number, dim(a*n)=dim(a).

 |- (D2): For $Dimension D1, D2, u1:Units(D1), u2:Units(D2), a,b:$Numbers, 
c:$Numbers-{0}, a.u1/b.u2=(a*c).u1/(b*c).u2 and 
a.u1*b.u2=(a*c).u1*(b/c).u2=(a/c).u1*(b*c).u2.

 |- (D3): For Dimensions D1, D2, u1:Units(D1), u2:Units(U2), 
u1/u2::Units(dim(u1./dim-u2./dim)=((_).u1/1.u2).
 |- (D4): For $Dimension D1,D2, u1:Units(U1), u2:Units(U2), 
u1*u2::Units(dim(u1./dim+u2./dim)=((_).u1*1.u2).
 |- (D5): For all D:$Dimension, u1,u2,u3:Units(D), a,b:$Numbers, if a.u1=1.u2
and b.u2=1.u3 then (a*b).u1=1.u3.
 For example, (D5) |- 60*1000.ms=1.hr.

 |- (D6): For all $Dimension D, u1,u2:Units(D), a,b,c:$Numbers, if a.u1=b.u2 
then (a*c).u1=(b*c).u2.
 For example, (D6) |- 30.min=0.5.hr.

Notice that if `n` is a number and `u` a unit the `n.u` is the measure.  But 
if `c` is some constant measure (say the speed of light or the acceleration 
due to gravity) then `c./u` is the number in units `u`.

 |- (D7):  For all $Dimension D, u:Units(D), a:number, a.u./u = a.

}=::MECHANICAL_UNITS.

.Open Common Units

 |- (common_units): MECHANICAL_UNITS.

. Lengths
	km::Units(Length),
	mm::Units(Length),
	cm::Units(Length),
	m::Units(Length),
	ft::Units(Length),
	inch::Units(Length),
	yd::Units(Length),
	miles::Units(Length),
	...
	|- (l1): 100.cm=1.m,
	|- (l2): 10.mm=1.cm,
	|- (l3): 1000.m=1.km,
	|- (l4): 12.inch=1.ft,

	|- (l5): 3.ft=1.yd,
	|- (l6): 1760.yd=1.mile.
	...

. Area and Volume
Area::=Length*Length,
	acre::Units(Area),
	 hectare::Units(Area),
	 ...
Volume::=Length*Length*Length.
()|- (VL): Volume=Length*Area=Area*Length.


	gallon::Units(Area), varies in size depending on geography.
	pint::Units(Area), varies in size depending on geography.
	|-(pg): 8.pint = 1.gallon.
	quart::Units(Area), varies in size depending on geography.
	|-(qg): 4.quart = 1.gallon.
	(pq,qg)|-(qp): 2.pint = 1.quart.

Metric system units of volume (international):
	liter::Units(Area),
	cc::Units(Area),
	...


mpg::Units(dim(L=> -2))=miles/gallon.

. Times and Dates
	ns::Units(Time), nanosecond
	ms::Units(Time), millisecond
	sec::Units(Time), second
	min::Units(Time), minute
	hr::Units(Time), hour
	day::Units(Time),
	week::Units(Time),
	month::Units(Time),
	year::Units(Time).
	|- (t1): 1000.ms=1.s and 1000.ns=1.ms,
	|- (t2): 60.min=1.hr,
	|- (t3): 60.s=1.min,

	|- (t4): 24.hr=1.day,
	|- (t5): 7.day=1.week.
.Dangerous_bend
The relationship between days, months and years depends on the calendar 
adopted.

	DATE::=Net{

		day::Integer & Time./day.
		month::Integer & Time./month.
		year::Integer & Time./year.
	}=::DATE.
	|- (d1): Dates<--$ $DATE.
The precise elements of $ $DATE that are valid is an interesting exercise in 
local trivia.


	|- (d2): $loset(Dates, <=, <).

loset::=http://www/dick/maths/math_21_Order.html#loset,
a linearly ordered set.

	+ :: Dates><Time->Dates.
	+ :: Time><Dates->Dates.
	|- (d5): For all d1:Time,t1:Dates ( d1+t1 = t1+d1 ).
	- ::Dates><Dates->Time.
	|- (d3): For all d1,d2,d3:Dates( d1+(d2-d3) = (d1-d3)+d2).
	|- (d4): For all d1,d2(d1-d2= -(d2-d1))

		...

.Dangerous_Bend
A common mistake is to think that a light-year is a measure of time.  It is a
measure of distance - the distance covered by light in one year.  At the 
atomic level the light_second is a similar useful unit of distance.

 light_year::Length,  distance covered by light in a vacuum in one year.
 light_second ::Length, distance covered by light... in one second.

.See Velocity and Acceleration

. Units of Mass
	oz::Units(Mass),
	lbs::Units(Mass),

	gm::Units(Mass),
	kg::Units(Mass).
	|- (m1): 16.oz=1.lb,
	|- (m2): 1000.gm=1.kg, ...

Do not confuse these with the forces that they cause due to the gravity
of earth....
.See Force and weight

. Angles
	deg::Units(Angle), degree -- basically Babylonian.
	rad::Units(Angle), radian.
	turn::Units(Angle), recent idea.
	|- (a1): 1.turn=360.deg=(2*\pi).rad.

Angles are an abstraction form the ratios between the radius of a circular
arc and it's length.

CIRCULAR::=following
.Net
	radius:: Length,
	diameter::Length=2*radius.
	circumference:: Length,
	area::Length*Length,
	\pi::Number=3.1415..., ratio of circumference ro diameter in a circle. .
	\tau::Number=2*\pi.
	(a1)|- 1.turn = \tau.rad.
	|- (circ1): circumference=2*\pi*radius,
	|- (circ2): area=\pi*radius^2.
	ARC::=Net{angle:Angle./rad, length:Length, length=angle*radius,area=angle*radius*radius.}.
.Close.Net CIRCULAR

\pi::$Number=CIRCULAR.\pi.

PI::=\pi.

. Information
	bit::Units(Information),
	byte::Units(Information),
	Kb::Units(Information),
	KB::Units(Information),
	MB::Units(Information),
	GB::Units(Information).
	|- (i1): 1024.bit=1.kb,
	|- (i2): 8.bit=1.byte,
	|- (i3): 1024.byte=1.KB,
	|- (i4): 1024.KB=1.MB,

	|- (i4): 1024.MB=1.GB.
	|- (i5): baud::=bit/s.
	|- (i6): bpi::=bit/inch.


. Velocity and Acceleration
	Velocity::=dim(L=>1,T=>-1,M=>0,I=>0,A=>0),
	()|-(v1): for all l:Length, t:Times, l/t in Velocity.
	fps::Units(Velocity).

	mph::Units(Velocity).
	()|-(v2): 60.mile/2.hour=30.mile/1.hour=30.mph.

	mph=miles/hour.
	|- (v3): 1.mph=1.mile/1.hour.
	|- (v4): 1.fps=1.ft/1.s.
	()|-(v5):x.fps=((60*60)*x/(12*3*1760)).mph.
	()|-(v6): x.ft/s=x.ft/1.s.

Physicists believe that the speed of light is a fundamental constant - a kind
of universal speed limit for all matter.  It is often symbolized by the letter
"c":
	c::Velocity.
	|- (c1): c./mph = 186000 (??).
	|- (c2):light_year=year/c.
	|- (c3): light_second=sec/c.

Acceleration::=dim(M=>0, L=>1, T=>-2,I=>0,A=>0).
	fpss, ...:Units(Acceleration).
	|- (a1):1.fpss=1.ft/1.s/1.s.



. Force and weight
Force::=dim(M=>1, L=>1, T=>-2, I=>0,A=>0).
	dynes::Units(Force),
	newtons::Units(Force).


	|- (f1):dyne=gm*cm/(s*s),
	|- (f2):newton=kg*m/(s*s),
	|- (f3):poundal=lb*ft/(s*s)=lb*fps=ftlb/ss,
	|- (f4): ss=s*s,

	|- (f5): ftlb=ft*lb.

If `g` is the acceleration due to gravity in units `ug` and `m` is a mass in 
units of `um` then the weight of a mass is the force exerted by gravity, or 
`g*m` in the units of `ug.um`.  To simplify some expressions there are special
units that take this into account:
	lb_weight::Units(Force),

	kg_weight::Units(Force).
	|- (f6):1.lb_weight= g.poundals.
	|- (f7):1.kg_weight= g.newton.

.Close Common Units

. Example in Computing
 If a track on a hard disk has radius `R`.inch,  turns once every `n`.s, and 
stores `b`.bpi then the transfer rate `t`.baud will be
	t= (2 * \pi * r / n).baud.
	(baud=bit/s=inch*bpi/s, 1.turn=2*\pi.rad, a disk_track:$ $CIRCULAR)

}=::DIMENSION.

.Open SI Units
The SI (
.Key System International
) Units are described at
.See http://physics.nist.gov/cuu/Units/units.html
, here is a quick summary.
SI::=Net{
SI_base_units::=Net{
	|- (SI0): $DIMENSION.$BASIS.
	Dimension_Unit_Abbreviation::=Net{ 1st:$Dimension, 2nd:units(first). 3rd:=2nd}.
	DUA::=Dimension_Unit_Abbreviation.
	|- (SIl): DUA(length, meter, m).
	|- (SIt): DUA(time, second, s).
	|- (SIT): DUA(temperature, kelvin, K).
	|- (SIm): DUA(mass, kilogram, kg).
	|- (SIc): DUA(electric_current, ampere, A).
	|- (SIM): DUA(amount_of_substance, mole, mol).
	|- (SIL): DUA(luminous_intensity, candela, cd).

(with thanks to Vince Tilroe, February 17th 2005,
who emailed me corrections)

}=::SI_base_units.
SI_derived_units::=Net{
To Be Done...
}=::SI_derived_units.
}=::SI.

.Close SI Units

.Open Temperature
Unlike most units, temperature scales have different zeroes:
	Kelvin - absolute zero
	Centigrade - melting ice under standard pressures etc.
	Fahrenheit - the lowest temperature Fahrenheit could get - mixture of
ice and salt.

This means that the definition of unit implies that temperature is not a unit!
Instead we can use a weaker form:
	For $Dimension D, Scale(D) ::=(+)$Numbers---D,
and formally define:
	Temperature::$Dimension.
	Centigrade::Scale($Temperature).
	C::=Centigrade.
	Fahrenheit::Scale($Temperature).
	F::=Fahrenheit.
	Kelvin::Units($Temperature).
	K::=Kelvin.

	For all t:$Temperature, t./C = t./K + $absolute_zero.

absolute_zero::=`that temperature at which all motion ceases`, this
is inaccessible as it takes more and more work to extract heat (motion)
from something, the closer you get to absolute zero.  Absolute zero
is the
.Key the lowest possible temperature.

In the centigrade scale:
absolute_zero::= -273.15./C.

There are well known formulas for converting 
.Key Fahrenheit to Centigrade
and 
.Key Fahrenheit to Centigrade:
	For all t, t./C = (5/9)*(t./F - 32 ),
	For all t, t./F = 32 + (9/5)*t./C.


For details see
.See http://en.wikipedia.org/wiki/Temperature
in the Wikipedia.

.Close Temperature

.Open Money
	money::$Dimension.
	dollars::units(money).
	cents::=units(money).

	|-(USA1): 1.dollars = 100.cents.


Please add the definitions for any other currencies that you know about
by clicking here:
.Hole
.Close Money

.Close Dimensioned Numbers