DRAFT
A
Type Theory for Applied Mathematics
Dr Mark Tarver
dr.mtarver@ukonline.co.uk
Lambda Associates
April 2006
www.lambdassociates.org
You can get the
.pdf version of this paper here.
Some related work on this area
is given in the links at the bottom of this page -
courtesy of reddit and comp.lang.lisp.
The source for the water tank
problem cited in section 4.0 can be downloaded here.
An apprentice
carpenter may want only a hammer and saw, but a master
craftsman employs many precision tools. Computer
programming likewise requires sophisticated tools to cope
with the complexity of real applications, and only
practice with these tools will build skill in their use.
Robert L. Kruse,
Data Structures and Program Design
Just over one
hundred years ago, in 1903, the first powered flight was
made by Orville Wright at Kittyhawk. The Wright aeroplane
was assembled by two brothers armed with a background in
making bicycles and a rudimentary grasp of the principles
of aerodynamics. The Flyer I cost less than a thousand
dollars to construct.. It had a wingspan of 40 feet,
weighed 750 pounds, and sported a 12 hp, 170 pound
engine.
One hundred years later the American air force unveiled
the F-22 Raptor stealth fighter at a unit cost of over
300 million dollars. Using advanced metallurgy, including
composite materials, the Raptor uses Raytheon processors
rated at 10.5 billion instructions per second to process
its radar information and the programs controlling the
flight and radar total 1.7 million lines of code.
The technological gap between these two pieces of
engineering is tribute to the progress in science and
engineering that took place during the last century. But
the very complexity of our creations has placed undue
strain on our traditional methods of organizing our
communication and integrating the efforts of our
engineers necessary to create products like the Raptor.
These processes are often stretched to breaking point and
when they do break in the context of a major engineering
initiative, the results can be embarrassing, expensive
and potentially even fatal.
One such example was the NASA Mars Lander. Dr Edward
Weiler, NASA's Associate Administrator for Space Science,
recorded the reason for the $120 million crash of the
Mars Lander in 1999.
"People sometimes make errors. The problem here
was not the error, it was the failure of NASA's systems
engineering, and the checks and balances in our processes
to detect the error. That's why we lost the
spacecraft."
http://www.space.com/news/orbiter_error_990930.html
The peer review
preliminary found that one software team had used English
units (i.e. inches, feet and pounds) while the other used
metric units for a key spacecraft operation. This
information was critical to the maneuvers required to
place the spacecraft in the proper Mars orbit. Apart from
the loss of money, the blow to NASA’s prestige was
severe.
1.0
One Reason Why Engineering Projects Often Result in Buggy
Software
Modern science and engineering is now massively dependent
on computing resources to the extent that hardly any
significant scientific or engineering project can be
conducted without the use of computers to perform the
math. The part of math that we are concerned with here is
of course applied mathematics. We define applied
mathematics as the application of mathematics to the
calculation of quantity. By quantity we understand any
form of measure – whether of mass, energy, work,
length or time.
Since applied mathematics is concerned with measure, we
might expect that computer models that use applied
mathematics would explicitly represent those measures. In
fact, this is not generally true. In current computer
science, computations involving applied mathematics are
not different from computations of pure mathematics. In
both cases, numerical computations are involved, and it
is the interpretation given to these computations that
demarcate pure from applied studies. This interpretation
is typically not part of the program itself, but exists
in the mind of the developer. If she is particularly
thorough, then it may exist informally as documentation
to the program; but this documentation is incidental to
the compilation and execution of the program itself.
This rather loose and haphazard arrangement has
significant dangers. The dangers arise when the informal
interpretation does not match the numerical computation.
This of course is precisely what happened in the case of
the Mars Lander. Since the interpretation is informal and
not part of the program itself, a failure of this kind
will pass unnoticed by the computer.
2.0
Tackling the Problem
Existing approaches to the problem emphasise project
management approaches to develop reliable software.
However though organizing and reshuffling the human
component may have its uses, a more promising approach is
to minimize human error by formalizing the hitherto
informal interpretations attached to the parameters of
the computation. Just as applied mathematics originally
advanced in speed and reliability by removing the
responsibility for calculation from slow and error-prone
human beings, so it is logical to look to computers to
tackle the problem of guaranteeing the reliability of
engineering projects. Such a guarantee must rely on the
formalisation of the hitherto informal and loosely worded
descriptions of what the program is supposed to be
calculating. Such a formalisation can be either explicit
or implicit.
The explicit approach relies on explicitly attaching the
interpretation to the parameters in the program. Hence
instead of writing 9.8 and commenting that this figure is
to be read in pounds, it would be possible to explicitly
write [9.8 lbs]. The interpretation of any applied
mathematics program would then be immediately
recognisable to the computer. In the philosophy of
mathematics, objects that mix units of measure with
numbers are referred to as impure numbers. Hence the
explicit approach requires that impure numbers be treated
as structures distinct from numbers.
However there are two compelling arguments against the
explicit approach.
The first is that programmers in science and engineering
do not operate with impure numbers as objects different
in kind from numbers. Since impure numbers, under the
explicit approach, are lists and not numbers, two impure
numbers cannot be multiplied together nor can any impure
number be multiplied by any kind of number. Not a single
mathematical operation, however humble, could be applied
to an impure number without recoding that operation.
Using impure numbers with explicit measures means that
all math libraries must be redefined.
Second, even if the libraries could be rewritten, the
resulting operations would be less efficient since every
arithmetic operation would require extracting the
numerical component from a structure, performing the
operation, and then re-embedding the result back into a
new structure. The explicit approach is not a feasible
solution.
In contrast the implicit approach does not divorce impure
numbers from numbers. This approach follows the orthodox
view that impure numbers are just numbers put to a
certain use. The difference is that the implicit approach
requires that the use is codified and formalised in the
type theory of impure numbers. It then becomes the
responsibility of the computer running the type checker
to ensure that the program is free from certain basic
coding errors common to engineering applications. These
errors range from basic blunders involving inappropriate
metrics to conversion errors of various kinds and the
misrepresentation of mathematical equations within
stretches of code.
The implicit
approach is promising, but the requirements placed on the
type checker go well the resources of what current
programming languages can deliver; including those
considered state of the art such as ML, Haskell and
O'Caml. To implement this approach comprehensively, a
type notation is required capable of expressing the
complex logical and numerical relationships that exist
within the type theory of applied mathematics.
The sequent
calculus notation of Qi, derived from the foundational
work of the logician Gerhard Gentzen, is a good notation
for constructing a specification of these requirements.
It has the advantage of being based on a clear and
powerful notation used widely in theoretical computer
science, and, through Qi’s efficient compiler
technology, of delivering fast and efficient type
checkers from what is, in effect, an executable
high-level specification of a type theory. This notation
is used throughout this paper.
3.0 A Type
Theory of Metrics
What does this theory look like? It is a formal theory of
metrics. Metrics are what we use to measure quantity.
There are an indefinitely large number of metrics
corresponding to the conventional metrics for measuring
distance, mass, energy, time and many other aspects of
the physical world. The theory begins with a statement
about metrics.
1. Objects grouped under metrics are numbers.
This is a fundamental claim. This immediately allows the
connection of impure numbers to any mathematical
operation and opens the way for the free application of
functions from pure mathematics to applied mathematics.
We use Qi sequent notation to express these
relationships.
____________________
(subtype metric number);
(subtype B A); X : B;
X : A;
Lets concentrate on metrics for distance. There are many
different conventions for measuring distances; the
European metric system and the Imperial are but two. Let
us take one metric from each; inches and centimeters.
_______________
centimeters : metric;
____________
inches : metric;
We can add distances under different metrics to produce
numbers.
(define add-distances
{inches --> centimeters --> number}
X Y -> (+ X Y))
But we cannot add inches to centimeters to produce inches
which was precisely the sort of error that destroyed the
Mars Lander. .
(define add-distances
{inches --> centimeters --> inches}
X Y -> (+ X Y))
However our system is too severe, we cannot add inches to
inches and produce inches.
(define add-inches
{inches --> inches --> inches}
X Y -> (+ X Y))
This leads to the second claim.
2. Adding or subtracting numbers grouped
under the same metric gives a number of the same metric.
We want to say that two objects that belong to the same
metric can added or subtracted together and the result
will be an object belonging to the same metric as the
inputs.
if (element? Op [+ -])
A : metric; M : A; N : A;
(Op M N) : A;
It is tempting to generalize this rule to other
arithmetical operations, but caution is needed here as we
shall see later.
3. Applying a numerical operation to a metric
gives a metric of the same type.
If we know that we have to travel 10 miles to reach our
destination then simply doubling that number will give
the round trip in miles. Applying a unary mathematical
function (like doubling) to a metric will result in a
figure grouped under the same metric. Here is the rule
Op : (number --> number); N : A; A : metric;
(Op N) : A;
There is a special class of such functions which are used
extensively in business and science to drive exchanges of
many kinds; they are called metric conversion functions.
3.1 Metric
Conversion
Metric conversion is a basic operation. It occurs
whenever we want to convert one metric into another;
dollars to pounds, inches to centimeters, joules to
calories are examples. Often this involves multiplication
or division by a constant.
Inches to centimeters is a good example. Inches convert
to centimeters under the formula C centimeters = (C *
2.54) inches. But by the previous principle, when we
multiply I inches by 2.54 we drive a figure in inches
(since (/. X (* X 2.54)) : (number --> number)). But
we are also saying that when we do that we derive a
figure in centimeters. Is there a contradiction in saying
this?
According to one representation there is a contradiction.
If we accept the following identities
1 inch * 2.54 =
2.54 centimeters
1 inch * 2.54 = 2.54 inches
then we derive the
absurd identity
2.54 centimeters = 2.54 inches
But since we do operate with conversions without ending
up in absurdities, these identities cannot accurately
reflect the reasoning that we use in converting from
inches to centimeters. Lets retrace our steps.
Consider these two problems.
Problem A: I am given a length of wood 9 inches long
and I am asked the length of this piece in centimeters.
Problem B: I am given a length of wood 9 inches long and
told that I need to find a larger piece nearly 2 ½ times
larger - 2.54 times larger to be exact.
Now in each case I am asked to perform a computation
which is multiplying the length 9 inches by 2.54. The
result is in both cases the same number – however
the number that results happens to answer two different
questions; i.e. the length in centimeters and the length
in inches of the larger piece of wood I am looking for.
The question of which enterprise I am involved in cannot
be ascertained by examination of the computation
involved. The answer as to the type of the result is not
in the computation but in the purpose to which the
computation is put.
Hence even at this early stage of our investigations, we
begin to discern one important feature of programs in
applied mathematics. That is the automatic hands-off
certification of the types of the results of these
computations in the manner of SML and related languages
is an impossible task. We cannot expect a type checker to
divine the nature of the results merely from looking at
the computation itself without knowing what question the
computation is supposed to answer. Hence any machinery
for divining whether the applied mathematics program is
type secure must rely on the formal annotations of the
programmer.
When we place the results of a computation under a type
we are saying something indirectly about the question
which prompted the computation. If the same object should
answer two different questions then the identity of the
questions does not follow any more than the identity of
the two types under which the number falls. Hence the
absurdity represented earlier cannot be the correct
logical representation of our reasoning in this area of
applied mathematics.
The mistake in the absurdity before mentioned is that
type rules involving metrics do not state identities;
rather they express legitimate ways of classifying the
results of computations. It is therefore not
contradictory to affirm that the same result can be
legitimately classified under two different types
provided we understand that the purpose of the
computation must determine which is the correct type. The
job of the type theorist is to express these legitimate
paths; the job of the programmer is to indicate which one
he has chosen.
3.2
Computing Inverses from Equations of the Form x = Ky
To return now to the question of metric conversion.
Inches convert to centimeters under the formula C
centimeters = (C * 2.54) inches. In sequent form;
____I : inches;___
(* I 2.54) : centimeters;
The inverse conversion is trivially derivable
C : centimeters;
(/ C 2.54) : inches;
But if the inverse conversion is trivially derivable then
it should be the responsibility of the computer to infer
it. By adopting this approach, we avoid having to write
an inverse for every conversion of this kind. We know I
: inches;
(* I 2.54) : centimeters; if and only if C :
centimeters;
(/ C 2.54) : inches;
In fact the nature
of the metric (inches, centimeters etc) and the value of
the constant 2.54 is irrelevant here. We can assert for
all metrics A, B and for any constant K. I : B;
(* I K) : A; if and only if C : A;
(/ C K) : B;
Hence
I : B; and C
: A; implies (/ C K) : B;
(* I K) : A;
Written in sequent
calculus we are affirming that where I is an arbitrary
term and A and B are metrics, the following rule holds
C : A;
I : B >> (* I K) : A;
(/ C K) : B;
In Qi this is easily transcribed. The following script
shows the modus operandus.
(1+) (datatype inches-to-centimeters
I : inches;
___________
(* I 2.54) : centimeters;
______________
inches : metric;
___________________
centimeters : metric;)
(2+) (datatype simple-metric-conversion
C : A;
I : B >> (* I K) : A;
A : metric; B : metric;
___________________
(/ C K) : B;)
(3+) (define inches_to_centimeters
{inches --> centimeters}
I -> (* I 2.54))
inches_to_centimeters : (inches --> centimeters)
(4+) (define
centimeters_to_inches
{centimeters --> inches}
C -> (/ C 2.54))
centimeters_to_inches : (centimeters --> inches)
The
simple-metric-conversion rule removes the necessity for
providing inverses for every conversion rule driven by a
simple equation of the form x = Ky where K is a constant.
3.3 A
Simple Conversion Program
Now lets suppose that we want to write a simple program
that receives an input in inches and prints the output in
centimeters. Seems trivial, but we have a catch. We need
a function that receives the user's input in inches. In
Qi such a typed function is called input+. Thus (input+ :
number) waits to receive a user input of type number. The
catch is that we have no rule for testing whether a
user's input is a figure in inches. A figure in inches
could as well be a figure in centimeters. It is by fiat,
or intention that the figure entered is to be taken as
representing inches and not centimeters. What we need is
some way for the programmer to signal this act of
intention to the computer.
To do this we invent a function input-metric which
carries its own type with it as a signal of the
programmer's intention. The definition is very simple
(DEFMACRO input-metric (Metric String)
(DECLARE (IGNORE Metric))
`(PROG2 (output ,String) (input+ : number)))
The input-metric function passes control to input+ which
simply waits for a number. The Metric argument is not
passed forward or evaluated (hence the definition of this
function as a Lisp macro), but it has an important role
in the type theory of the function. A sequent rule deals
with the type properties of this function.
S : string;___________
(input-metric A S) : A;
The rule says that
this function is self-certifying as regards the type of
its output; the type is the type that the programmer says
it is.
With this function the program is now indeed trivial;
here it is.
(define ic-converter
{A --> centimeters}
_ -> (let I (input-metric inches "Enter length in
inches: ")
(do (output
"Length in centimeters is ")
(inches_to_centimeters I))))
3.4
Computing Inverses from More Complex Equations
Many but not all conversion rule are driven by equations
of the form x = Ky. The conversion of centigrade to
fahrenheit is driven by an equation, but not one of that
precise form. The equation is xoF = (yoC * 5/9) + 32.
It is certainly
possible to orient this equation to derive the inverse
conversion using a similar, but rather more complex
pattern of reasoning, than the one used to compute the
simple-metric-conversion. But the utility of such a rule
is also far less than the simple-metric-conversion type
rule relating multiplication and division. Also the
possibility of a human making a mistake calculating the
inverse transformation from the equation is far from
impossible.
Couched in terms of the computer, we have an equation
that can be represented as a list structure involving
types.
[[X : fahrenheit]
= [[Y : centigrade] * 5/9] + 32]]
From this equation
(list structure), we wish the computer to infer two rules
of the form. …..Y : centigrade .....
….........................
X : fahrenheit; …..X : fahrenheit .....
….........................
Y : centigrade;
In general we have
an equation in which there is a dependent variable (X)
and 1 or more independent variables (Y1, …Yn etc). A
single such equation generates n+1 sequent rules. Each
sequent rule results from the transposition of the
equation according to algebraic reasoning where an
independent variable is pushed into the dependent
position. The computation of the relevant sequent rule is
trivial once the equation is oriented into the proper
form. For example for the equation
[[X : fahrenheit]
= [[[Y : centigrade] * 5/9] + 32]]
The appropriate
rule is
(X = (+ (* Y 5/9)
32));
Y : centigrade;
X : fahrenheit;
And an extra rule
concerning the reflexivity of identity needs to be added
to the type checker to make the whole thing work.
______
(X = X);
The hard part of
this work is the algebraic transformation of the equation
to yield the different dependent variables. A general
purpose program of this type, though beyond the scope of
this paper, is certainly possible for a wide class of
cases, subsuming of course the essentially trivial x = Ky
cases mentioned earlier.
3.5 Derived
Metrics as Ratios
Derived metrics are metrics that express relations
between other metrics. A simple example is speed which is
the ratio between distance covered and time taken. In
English the word ‘per’ is used to denote such
ratios. Type theoretically, per is a 2-place type
operator receiving metrics as operands.
4. The ratio of any two metrics is a new
metric
The type rule is
A : metric; B
: metric; X : A; Y : B;
(/ X Y) : (per A B);
______________
(per X Y) : metric;
We assume seconds
as a metric.
______________
seconds : metric;
This allows the
immediate definition of inches-per-second.
(define inches-per-second
{inches --> seconds --> (per inches seconds)}
I S -> (/ I S))
If we multiply 5.6 inches per second by 4 seconds we get
a figure in inches. Also if we divide 5.6 inches per
second into 4 inches we get seconds. This is generally
true of derived metrics built using per and the reasoning
is encapsulated in two rules.
X : (per A B); Y : B;
(* X Y) : A;
Y : (per A B); X : A;
(/ X Y) : B;
3.6 Derived Metrics as Powers
A basic operation over impure numbers is the raising of a
metric to a higher power. Examples are centimeters to
square centimeters, square centimeters to cubic
centimeters and so on. Typically such numbers are derived
by the multiplication of two impure numbers that use
identical metrics of distance.
3 inches * 4
inches = 12 square inches
5. The
multiplication of two objects under identical metrics
produces an object under a metric of a higher power.
Type theoretically, multiplying quantities Q1 and Q2
grouped under identical metrics results in an object of
type quite distinct from the type of the object that
results simply adding Q1 and Q2. For example, we reject
the identity
(3 inches * 4
inches) = 3 inches + 3 inches + 3 inches + 3 inches
though we do accept
that
(3 inches * 4) =
3 inches + 3 inches + 3 inches + 3 inches
The reason why we
affirm the latter and deny the former is that we want to
allow metrics to be raised to a higher power by the
multiplication of Q1 and Q2. We want to say that (3
inches * 4 inches) gives 12 square inches. Accepting the
equation
(3 inches * 4
inches) = 3 inches + 3 inches + 3 inches + 3 inches
or equivalently
(3 inches * 4
inches) = 12 inches
and the equation
(3 inches * 4
inches) = 12 square inches
we derive the
absurdity
12 square inches
= 12 inches
Hence (3 inches * 4
inches) is type theoretically distinct from (3 inches *
4) and its effect is to raise the metric to a higher
power. (Hence our caution earlier in extending the
treatment of addition and subtraction of metrics to
multiplication).
Conventionally this higher power is represented by terms
such as ‘squared’ or ‘cubed’. For our
purposes we use ‘square’ as an operator for
raising the power of a metric. Hence ‘9 : (square
(square inches))’ means for us the same as ‘9
cubic inches’.
Two metrics are similar when they are both powers of the
same metric. More precisely, where A and B are metrics.
1. A is similar to B if A = B.
2. (square B) is similar to A if B is similar to A.
3. (square A) is similar to B if A is similar to B.
The sum of two similar metrics A and B is defined
inductively
1. The sum of A and A is (square A) where A is not
squared.
2. The sum of (square A) and B is the square of the sum
of A and B.
3. The sum of A and (square B) is the square of the sum
of A and B.
The statement the multiplication of two objects under
identical metrics produces an object under a metric of a
higher power is the limiting case of the raising of a
metric to a higher power where similarity is couched in
terms of identity. The type rule for this statement is
A : metric; X : A; Y : A;
(* X Y) : (square A);
However a more general and powerful formulation works for
all similar types. Here are the rules for the more
general formulation using summing.
X : B; Y : C; ((sum B C) = (square A));
(* X Y) : (square A);
if (symbol? A)
____________________
((sum A A) = (square A));
______((sum A B) = C);________
((sum (square A) B) = (square C));
______((sum A B) = C);________
((sum A (square B)) = (square C));
6. The division of an object of grouped under
a metric of higher power by one grouped under a lower
power using the same metric produces an object under that
metric of a power which represents the difference of the
two powers.
To lower the power of a metric, we divide a higher power
of that metric by a lower power. The simplest case is
represented by the following rule.
X : (square A); Y : A;
(/ X Y) : A;
A more general
version of this principle is given here.
X : B; Y : C; (A = (sum B C));
(/ X Y) : A;
A potent operation combines the raising of the power of a
metric within the scope of a ratio. A metric may be
raised to a higher power within the scope of a ratio by
the multiplication by a similar metric. For example; the
multiplication of meters per second by square meters to
give cubic meters per second as a rate of flow. The
required rule is
X : (per C B); Y : D; ((square A) = (sum C D));
(* X Y) : (per (square A) B);
4.0 gives a concrete example of the use of this principle
and several others discussed here.
4.0 A
Concrete Problem
Let us take as an example the following problem.
A pipe with a diameter of 10 inches pumps water at a rate
of 1.5 meters/sec into a tank which has sides 10 meters
long by 4 meters wide. How long does it take to fill the
tank to a depth of 3 meters?
This is a good
example involving several metrics and two different
measuring systems. To implement a program to compute the
answer requires first designing an interface to receive
the inputs. These inputs must carry with them the metrics
which are attached to them if the program is to be
checked as type secure. The program cited can be
downloaded here.
The program begins by requiring the user to enter the
parameters of the problem.
(define solve-problem
{A --> seconds}
_ -> (compute-solution (input-metric inches
"Enter bore of pipe in inches: ")
(input-metric (per meters seconds) "Enter flow rate
in meters per second: ")
(input-metric meters "Enter length of tank in
meters: ")
(input-metric meters "Enter width of tank in meters:
")
(input-metric meters "Enter depth of water in
meters: ")))
The program that computes the solution performs the
following operations.
1. It calculates the radius of the bore in meters.
2. It uses this figure to calculate the area of the bore
in square meters.
3. It uses the area figure to calculate the volume flow
in cubic meters per second .
4. It calculates the volume of the tank in cubic meters.
5. It divides the volume by the volume flow to get a
figure in seconds.
The task of the
type system is to check that the computation is type
secure with respect to its use of metrics. Here is the
program.
(specialise per)
(specialise input-metric)
(datatype applied-maths
_________________
(value *pi*) : number;
C : centimeters;
______________
(/ C 100) : meters;
I : inches;
__________________
(* I 2.54) : centimeters;
S : string;
___________________
(input-metric A S) : A;
if (element? M [inches seconds centimeters meters])
_____________________________________________
M : metric;
A : metric; B : metric;
_______________________
(per A B) : metric;
A : metric;
_______________
(square A) : metric;
Op : (number --> number); N : A; A : metric;
___________________________________________
(Op N) : A;
X : (per A B); Y : B;
_____________________
(* X Y) : A;
Y : (per A B); X : A;
_____________________
(/ X Y) : B;
X : B; Y : C; ((sum B C) = (square A));
______________________________
(* X Y) : (square A);
if (symbol? A)
____________________
((sum A A) = (square A));
((sum A B) = C);
__________________________
((sum (square A) B) = (square C));
((sum A B) = C);
__________________________
((sum A (square B)) = (square C));
X : B; Y : C; ((sum B C) = A);
_______________________
(/ X Y) : A;
X : (per C B); Y : D; ((sum C D) = (square A));
____________________________________
(* X Y) : (per (square A) B);)
(define solve-problem
{A --> seconds}
_ -> (compute-solution
(input-metric
inches "Enter bore of pipe in inches: ")
(input-metric (per meters seconds)
"Enter flow rate in meters per second: ")
(input-metric meters "Enter length of tank in
meters: ")
(input-metric meters "Enter width of tank in meters:
")
(input-metric meters "Enter depth of water in
meters: ")))
(define
compute-solution
{inches --> (per meters seconds) --> meters -->
meters --> meters --> seconds}
Bore Flow Length Width Depth
-> (let Diameter (inches-to-meters Bore)
Radius (half
Diameter)
Area (circle-area Radius)
Volume-per-sec (cubic-meters-per-second Flow Area)
Tank-Volume (volume Depth Length Width)
Time (time-taken Tank-Volume Volume-per-sec)
Time))
(define
inches-to-meters
{inches --> meters}
Bore -> (/ (* Bore 2.54) 100))
(define half
{number --> number}
N -> (/ N 2))
(define circle-area
{meters --> (square meters)}
Radius -> (times-pi (* Radius Radius)))
(define times-pi
{number --> number}
N -> (* N (value *pi*)))
(define volume
{meters --> meters --> meters --> (square
(square meters))}
Depth Length Width -> (* Depth (* Length Width)))
(define cubic-meters-per-second
{(per meters seconds) --> (square meters) --> (per
(square (square meters)) seconds)}
Flow Area -> (* Flow Area))
(define time-taken
{(square (square meters)) --> (per (square (square
meters)) seconds) --> seconds}
Tank-Volume Volume-per-sec -> (/ Tank-Volume
Volume-per-sec))
(set *pi* 3.142)
Here is a script.
(1+) (load
"tank problem.txt")
per : symbol
input-metric : symbol
applied-maths : unit
solve-problem : (A --> seconds)
compute-solution
: (inches --> ((per meters seconds) --> (meters
--> (meters --> (meters --> seconds))))
inches-to-meters : (inches --> meters)
half : (number --> number)
circle-area : (meters --> (square meters))
times-pi : (number --> number)
volume : (meters --> (meters --> (meters -->
(square (square meters)))))
cubic-meters-per-second : ((per meters seconds) -->
((square meters)
--> (per (square (square meters)) seconds)))
time-taken : ((square (square meters)) --> ((per
(square (square meters)) seconds) --> seconds))
3.142 : number
typechecked in 6156 inferences.
Real time: 0.609375 sec.
Run time: 0.53125 sec.
Space: 6285184 Bytes
GC: 10, GC time: 0.09375 sec.
loaded : symbol
(2+) (solve-problem _)
Enter bore of pipe in inches: 10
Enter flow rate in meters per second: 1.5
Enter length of tank in meters: 10
Enter width of tank in meters: 4
Enter depth of water in meters: 3
1578.6157 : seconds
5.0
Conclusion
Orthodox programs in science and engineering manipulate
figures which correspond to physical quantities. However
orthodox programming is simply ‘number
crunching’ without safeguards to guarantee that the
computation models a physically tenable process. This
arises because the interpretations attached to the
parameters of the program are typically held either (a)
within the brain of the programmer or (b) written in an
informal and ad hoc fashion in the supporting
documentation. No formal guarantee exists that the
program is representing any process consistent with the
equations that are supposed to drive its development.
This draft has described a way of tackling this problem
though the use of type theory. Using a small but
essential fragment of the type theory of applied
mathematics it is possible to prove the type integrity of
programs using basic applied mathematics. The
construction of an adequate theory for all of applied
mathematics is not a small project. But by carefully
codifying this type theory in the manner shown here, it
is possible to automate the verification of the physical
credentials of engineering and science programs with
respect to the underlying realities they are supposed to
represent.
References
1. Functional Programming in Qi, 2005, available
as .pdf from www.lambdassociates.org
2. Report on the Mars Lander Catastrophe
http://www.space.com/news/orbiter_error_990930.html
3. Online Program
www.lambdassociates.org/studies/tank.zip
4. Robert L. Kruse, Data Structures and Program
Design, Prentice Hall, 1987.
Related
Work
The following relevant pieces of
work were provided courtesy of reddit and comp.lang.lisp.
[cunis92] R. Cunis, ``A Package
for Handling Units of Measure in Lisp'', ACM Lisp
Pointers, vol. 5, no. 2, 1992. http://www.isi.edu/isd/LOOM/documentation/measures-implementation.text
http://www.isi.edu/isd/LOOM/documentation/measures-usage.text
http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/lang/lisp/code/...
http://lss.fnal.gov/archive/1998/conf/Conf-98-328.pdf
"Introduction to the SILibrary of Unit-Based
Computation" by WalterE. Brown; October 1998
Presented at the International Conference on Computing in
High Energy Physics (CHEP’98), Chicago, Illinois,
August31-September4,1998
|