0
$\begingroup$

Is there support in the foundation of mathematics for dimensioned quantities?

Those immersed in real-world software problems, continually confront the absence of dimensioned quantities in programming languages. Occasionally this results in a billion dollar disaster, such as the Mars Climate Orbiter. This absence appears in the foundation of mathematics!

The absence of support afflicts even Wolfram's Mathematica, which has a bug-riddled subsystem to deal with what it calls "Quantity" entities. I say "bug-riddled" as someone who has attempted to use this subsystem rigorously and found numerous bugs not attributable to my admittedly less-than-masterful grasp of its Byzantine structure, evidenced by the following response to the latest bug with dimensioned quantities I ran into:

enter image description here

For an example of an approach to this vital topic, consider that First Order Logic (FOL) plays a central role in relational intension. Relation tables resulting from the application of intensions are relational extensions. The columns of relation tables may be treated as properties being observed during measurement with each row a specific observation.

Since FOL is at the very foundation of mathematics, it would seem strange if there was no work in CS to found their treatment of dimensioned numbers in terms of FOL.

Note, I'm not suggesting that this is the only rigorous approach to the problem of programming language design in which dimensioned numbers are a natural result of the foundational principles.

I'm just wondering what I'm missing, since it seems CS is all-but silent on such an important topic?

Improve this question
$\endgroup$
2
  • 4
    $\begingroup$ What is your question? $\endgroup$
    – orlp
    Commented Mar 24 at 19:52
  • $\begingroup$ FOL is not "a the very foundations of mathematics". That's just one possibility that works very well for logicians who study foundations as a topic, but is not a workable solution for the working mathematician. $\endgroup$
    – Andrej Bauer
    Commented Apr 4 at 6:15

2 Answers 2

Reset to default
1
$\begingroup$

Of course there is mathematical support for dimensioned quantities. It's kind of trivial from mathematical point of view.

Off the top of my head, here's a suggestion. Given some basic units of measurement, represented by a set of symbols $U$, say $\lbrace \mathtt{g}, \mathtt{m}, \mathtt{s}\rbrace$ consider the free abelian group $F(U)$. Its elements are all possible products of (integral) powers of the basic units, such as $\mathtt{m}/\mathtt{s}^2$ and $\mathtt{s}^2 \mathtt{m}^3$. These correspond to compound units generated from the basic ones. A dimensioned quantity is then just a pair $(q, u)$ where $q \in \mathbb{R}$ and $u \in F(U)$. If this does not satisfy you, then you need to explain what it is that you want the theory to accomplish.

With regards to ensuring correctness of software, there are of course approaches to programmign that ensure correct treatment of dimensioned quantities. For example, there is a Haskell units package, and I am sure many others can be found with a bit of Googling. The problem is not that these things don't exist, but that they don't get used in software development.

Improve this answer
$\endgroup$
8
  • $\begingroup$ I'm aware of units-as-afterthought in programming languages going clear back to the physics Prof Bruce Sherwood's calc command for the TUTOR programming language in the early 1970s and was there when the Visicalc guys introduced TK!Solver, etc. and on and on. The problem is pure numbers simply don't occur. They always count something. Even the highfalutin functional programming world can't admit that functions are degenerate relations and FOL is prior even to set theory. FOL extensions are tables, so what are count tables if not fuzzy dimensioned numbers? $\endgroup$
    – James Bowery
    Commented Mar 26 at 1:24
  • 1
    $\begingroup$ I don't think that this is really the foundational issue you believe it is. If it's possible to express dimensions as types in a typed language like Haskell (see the package linked by Andrej Bauer), then it's also easily possible to extend their type system such that these notions are already encoded. $\endgroup$
    – Knogger
    Commented Mar 26 at 7:46
  • 1
    $\begingroup$ Also I'd wager that many functional programmers will be well aware of how functions are constructed in set-theory, and that (most) formulations of set-theory are models of FOL. But functional programming languages are mostly based on different forms of λ-calculi, in which functions aren't constructed but primitives. $\endgroup$
    – Knogger
    Commented Mar 26 at 7:51
  • $\begingroup$ Not very different from what Andrej suggests, but for a "foundation of mathematics" it seems nicer tho have types for the different physical dimensions (like Haskell does), for instance a type L for lengths, T for times etc. We would postulate that these are real one dimensional vector spaces and that the meter m is a basis of L, the inch another basis of L, the hour h a basis of T etc. A length would then just be a term of type L... On could multiply terms of different dimensions (tensor product of vector spaces) but not add them. $\endgroup$
    – Michael Bächtold
    Commented Mar 26 at 8:03
  • $\begingroup$ @JamesBowery: let me join the others in saying that FOL is irrelevant in this discussion and has almost nothing to offer in terms of a workable solution. Also, programming languages have made quite a bit of progress since 1970's, so I'd advise not to draw too many conclusions from software from that era. Modern type-theoretic accounts will prevent unit-related errors during compilation. $\endgroup$
    – Andrej Bauer
    Commented Mar 26 at 9:42
0
$\begingroup$

Dimensions play an important role in all natural sciences (physics, chemistry, engineering, etc.), but not in mathematics. The reason is that the property of "having a dimension" is not really a property of a quantity. It is a property of a physical law that involves that quantity. The property is formulated as a continuous symmetry with respect to multiplication the quantity by a positive real number.

An example is the simple law of "conservation of mass". It says that if we split a chunk of something with mass $m$ into two chunks with masses $m_1$ and $m_2$ then $m = m_1 + m_2$. This law is invariant with respect to multiplying all masses by a positive real number. So, we may measure masses in kilograms or pounds or whatever, but the law will remain the same.

This would not be true if the law of mass conservation had the form $m = \sqrt {m_1 + m_2}$ or something else that is not invariant under multiplication of all masses by a constant. But there aren't any laws like that.

In fact, almost all physical laws that involve masses will always have the same property: we may change the units of mass but the laws will remain the same.

Why is that? Nobody knows. But that's the laws of physics that we have discovered.

So, the fact that "mass has dimension" is really just a property of the physical laws that involve masses.

The same holds for other quantities (distance, time, charge, and so on). All physical laws involving those quantities are invariant under multiplication of all distances by an arbitrary number, all times by another arbitrary number, all charges by another number, etc. There are no laws where a distance $L$ would enter via a formula $L + \sqrt L$, or $L + \frac{1}{L}$, or anything else that is not scaled linearly under multiplication.

This is why physical quantities are always formulated using dimensions. Dimensions enforce the fundamental symmetry under rescaling.

But mathematics is not concerned with just the physical laws. Mathematics studies any equations or laws whatsoever. In mathematics, the equation $m = m_1 + m_2$ is just as interesting as $m = \sqrt{m_1 + m_2}$.

Also, mathematicians are always looking for simpler and at the same time more abstract formulations of laws. It is simpler to drop dimensions from consideration. If a law is invariant under rescaling, that's interesting and important. There is an entire theory around that (Lie groups and their orbits and representations). But it doesn't help to keep weird names around our equations: kilogram, inch, etc. Those names don't really help to study the mathematical properties of equations.

That's why mathematics-oriented software doesn't support dimensions. Or if it does, its support for dimensions was added as an afterthought.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Did you miss my comment on FOL? Do you know what FOL is and its bearing on both the foundation of mathematics and observations of the empirical world? $\endgroup$
    – James Bowery
    Commented Mar 25 at 21:21
  • $\begingroup$ "Dimensions play an important role in all natural sciences, but not in mathematics" This is not true. Dimensions, as the ones appearing in physics and natural sciences, also play an important role in mathematics, for for instance in the form of "abstract" one dimensional vector spaces (that are not canonically isomorphic to $\mathbb{R}$), or more interestingly in the form of line bundles, which leads to K-theory for instance. $\endgroup$
    – Michael Bächtold
    Commented Mar 26 at 8:08
  • $\begingroup$ @JamesBowery I would agree with the comment of Andrej Bauer - FOL is irrelevant to the question of dimensional quantities. $\endgroup$
    – winitzki
    Commented Mar 26 at 19:46
  • $\begingroup$ @MichaelBächtold It's not the same use of the term "dimension". The original post is asking about dimensions such as kilograms and meters. You are talking about dimensions of vector spaces. $\endgroup$
    – winitzki
    Commented Mar 26 at 19:46
  • $\begingroup$ It is the same use, if you accept that the space of lengths, times, masses etc (i.e. physical dimensions) are one dimensional vector spaces. $\endgroup$
    – Michael Bächtold
    Commented Mar 27 at 8:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.