Dimensional Analysis Community Input

Stream: maths

[Max Bobbin]

A recent project of mine has been formalizing dimensional analysis in Lean. So far, I am at a point where the code is better than Sympy and nearing on par or surpassing wolfram. However, I'm at a point where I'm stuck with defining addition. To give background, I defined a new inductive type, called dimension, which has one constructor, a function.

inductive dimension
| Q : rat → rat → rat → rat → rat → rat → rat → dimension
-- L → M → N → I → θ → T → J → dimension

This corresponds to the function Q = L^a*M^b*N^c*I^d*O^e*T^f*J^g, which allows any dimension to be constructed (assuming the seven common base dimensions )
Thus, length is defined as:

def length               : dimension := Q 1 0 0 0 0 0 0

Defining multiplication looks like:

protected def mul : dimension → dimension → dimension
|(Q a b c d e f g) (Q h i j k l m n) := (Q (a+h) (b+i) (c+j) (d+k) (e+l) (f+m) (g+n))

since the exponents just get added. The difficult part is addition. Two dimensions can be added together if they are the same, so we can add length, and get length + length = length. The other thing is we want addition to combine two of the same elements into one element, rather then multiply that element by two. This was done by

protected def add : dimension → dimension → dimension
|(Q a b c d e f g) (Q h i j k l m n) := ite (a=h∧b=i∧c=j∧d=k∧e=l∧f=m∧g=n) (Q a b c d e f g) dimensionless

where dimensionless is defined as

def dimensionless        : dimension := Q 0 0 0 0 0 0 0

In this case, dimensionless is used as a junk value that is thrown for improper addition. This definition encompasses most of the addition, but there is one more case. Adding a dimensionless number with a dimension simplifies to that dimension. So, dimensionless_number + length = length. The dimensionless number takes on the role of the identity element. For multiplication, it acts like 1 and for addition, it acts like zero.
I wanted to get feedback from the community and suggestions on how to implement this functionality. Specifically, defining addition so that the only acceptable cases are either addition of two of the same elements or an element with a dimensionless number.

[Johan Commelin]

Can't you just do

protected def add : dimension → dimension → dimension :=
λ Q₁ Q₂,
     if Q₁ = Q₂ then Q₁
else if Q₁ = dimensionless then Q₂
else if Q₂ = dimensionless then Q₁
else dimensionless

[Andrew Yang]

I don't think adding a dimensionless number with one with a dimension makes sense though?
What is 2 seconds + π ? Is (2 seconds + π) * 1 second equal to 6 seconds ^ 2 + π seconds?

[Yaël Dillies]

Maybe you want to talk about \Q[length, time, ...]?

[Yaël Dillies]

Or rather the corresponding add_monoid_algebra

[Andrew Yang]

I think fin n -> rat might be a better approach than what you have now. Also I wouldn't restrain to the case n = 7 since there are cases where introducing additional base units are useful.

[Kyle Miller]

Another option is to effectively use option dimension, with none signalling that there is an error in the dimensional analysis.
If you want, you can encode that as

inductive dimension
| Q : rat → rat → rat → rat → rat → rat → rat → dimension
| error : dimension

and then you have that any operation that involves a dimension error yields a dimension error. It's like a NaN for dimensions.

If you make errors yield dimensionless, then you can get weird situations like (1 second + 1 ft) * 3 kg = 6 kg

[Max Bobbin]

Andrew Yang said:

I don't think adding a dimensionless number with one with a dimension makes sense though?
What is 2 seconds + π ? Is (2 seconds + π) * 1 second equal to 6 seconds ^ 2 + π seconds?

I see the contradiction you are trying to show, but I don't think there ends up being a problem. If you had seconds*(seoncds+dimensionless) = seconds^2+seconds. If we used the addition rule, we would get seconds = seconds^2+seconds, and we could factor the right side to get seconds = seconds. We are looking at dimensional congruity. The reason I think we have to have this rule is Buckingham Pi Theorem stipulates that the dimensions form a vector field over the rational numbers. In Lean, the module definition requires the module part to be an add_comm_monoid, which requires this idea of adding an identity element.

[Max Bobbin]

Yaël Dillies said:

Maybe you want to talk about \Q[length, time, ...]?

Could you elaborate on what the \Q[length, time, ...] means? I've never used something like that in Lean before

[Max Bobbin]

Andrew Yang said:

I think fin n -> rat might be a better approach than what you have now. Also I wouldn't restrain to the case n = 7 since there are cases where introducing additional base units are useful.

I can try out this, I see what you that its much more manageable then seven rat and arrows, but I would need to learn how to properly use fin n so it translate to what I've been doing so far.

[Andrew Yang]

I don't really get what you mean by factor out seconds^2+seconds. I think we both agree that adding two different dimensions (as in this expression) is meaningless?
The dimension forms a Q-vector field because multiplying two dimensions corresponds to adding the exponents of each base units. The Q-action refers to taking powers. There is no "addition of dimensions" involved, and there should be no need to adjoin an identity: the dimensionless is already a multiplicative identity.

[Max Bobbin]

Yes, I see the contradictions that could form. I'm not trying to advocate for adding two different dimensions. The problem I'm having is showing that this Q-vector field exists. Using the module class that Lean already defines requires that dimension be an add_comm_monoid, which requires the idea of a zero element and adding the identity element. Plus, to use the definitions of the basis vectors requires this same property as well as being a module. I could just define a vector space and basis vectors and such without these requirements, but I didn't think this would be necessary and I could just use the module class already definined

[Max Bobbin]

Andrew Yang said:

I don't really get what you mean by factor out seconds^2+seconds. I think we both agree that adding two different dimensions (as in this expression) is meaningless?
The dimension forms a Q-vector space because multiplying two dimensions corresponds to adding the exponents of each base units. The Q-action refers to taking powers. There is no "addition of dimensions" involved, and there should be no need to adjoin an identity: the dimensionless is already a multiplicative identity.

However, doesn't it mean that if dimension forms a Q - vector space, then dimension must be an additive abelian group?

[Andrew Yang]

The add_comm_monoid is given by realizing each dimension as a n-tuple of exponents, and adding each exponent correspondingly. This in turn corresponds to multiplication of the dimensions and not the addition of the dimension.

[Andrew Yang]

By modeling dimensions as fin n -> rat, this vector space structure will come for free.

[Max Bobbin]

Ok, just had the break thought I needed. Thank you so much, that clears things up. I think that was the blockade that was confusing me, but I'm now on the same page. Thank you for your time and help! After I finish class, I'm going to try this out

[Max Bobbin]

Ok, that's perfect. I'll try that out tonight

[Anand Rao]

Since dimension is more the analog of a "type" of a physical quantity, would including the dimension information at the type level help here?

What I had in mind is something like this:

inductive physical_quantity {R : Type*} [comm_ring R] : R → R → R → R → R → R → R → Type*

where this inductive type either has no constructors, or has a single constructor for introducing a "value".

This way the problem of type-safe addition of physical quantities can be delegated to Lean.

[Yakov Pechersky]

I would suggest using a structure instead of a plain inductive to be able to index into each base through keywords

[Max Bobbin]

I think I can already do that with inductive though. Since, I can use def to define the seven base dimensions

[Tomas Skrivan]

This got me interested how to do dimensional analysis in Lean 4, I also got into a problem with addition

To me it seems you are not making the distinction between the unit itself and a value that has a unit. I would say you can't add units but you can add values with the same units.

Also I would argue that the unit checking should be done on the type checking level i.e. I do not like that adding two different units produce a junk value. I think such addition should be disallowed by the type system.

[Eric Rodriguez]

what if two units are propeq but not defeq? would seem like a pain

[Yaël Dillies]

What about just using formal series? Then you can add two values with different units without junk values.

[Tomas Skrivan]

Yes that is exactly the problem I got into :/

[Eric Rodriguez]

also maybe it's worth to have physical quantity just be fin n -> rat or something, because that way a) you can reuse API b) you can add random units that maybe don't exist but are useful theoretically or exclude units you don't care about at the time

[Eric Rodriguez]

fin 7 -> rat also makes sense

[Eric Rodriguez]

multiplication should then come automatically from pi.has_mul, addition would need a specific definition but

[Tomas Skrivan]

The fin n -> rat would be used for the unit not a quantity(value + unit), right?

[Eric Rodriguez]

yea

[Tomas Skrivan]

Why would you need multiplication on that type then?

[Eric Rodriguez]

meters squared * per seconds for example

[Johan Commelin]

When do rat-valued powers of units show up? (I only ever studied physics in high school...)

[Tomas Skrivan]

Eric Rodriguez said:

meters squared * per seconds for example

Maybe I'm misunderstanding something , but then you are adding or subtracting the powers: m^1 * m^1 * s^(-1) = m^(1+1) * s^(-1), no?

[Shing Tak Lam]

Johan Commelin said:

When do rat-valued powers of units show up? (I only ever studied physics in high school...)

Wave functions in quantum mechanics

[Eric Rodriguez]

Tomas Skrivan said:

Eric Rodriguez said:

meters squared * per seconds for example

Maybe I'm misunderstanding something , but then you are adding or subtracting the powers: m^1 * m^1 * s^(-1) = m^(1+1) * s^(-1), no?

ahh, sure, you definitely have to take care with the multiplication. sorry!

[Tomas Skrivan]

Now I'm thinking about it. A unit should be fin n -> rat × rat, it needs scaling and power.

For example this should be expressible: feet * km = 0,3048 m * 1000 m = 306,8 m^2. So we need multiplication in the first(scale) component and addition in the second(power).

[Andrew Yang]

I don't think we should focus on units rather than dimensions. And I don't think we should care about adding or multiplying concrete physical quantities since we would like the results to cover arbitrary transcendental functions. In particular, If a function f : (fin n -> real) -> real whose arguments have dimensions d : fin n -> dimension scales like some d' : dimension under the scalings induced by d on fin n -> real, it should be considered "physically meaningful" with dimension d' and our result should apply on it.

[Tomas Skrivan]

Makes sense, I guess it depends what is the application. My interest in this is to write code that prevents another Mars Climate Orbiter crash :)

[Eric Wieser]

Does the defeq problem actually come up? It seems quite unusual for your dimensions not to be known constants rather than free variables

[Tomas Skrivan]

In my Lean 4 attempt the defeq problem definitely comes up. For example 'meter per second' times 'second' is not defeq to meter, or at least I don't know how to make it so.

[Eric Wieser]

I don't see how that could be the case, that sounds like claiming that {s := -1 + 1, m := 1} is not defeq to {s := 0, m := 1}

[Eric Wieser]

It looks like your problem in that thread is that lean is not attempting to unify the types and check if they're defeq

[Eric Wieser]

And instead is using typeclass inference to match syntactically

[Tomas Skrivan]

Ohh I see, that makes sense. Well, it looks like that I do not understand defeq properly.

[Eric Wieser]

I don't know what the solution to your issue is though; I think this is a problem that Lean 3 solves by only having homogenous multiplication, which forces lean to unify the two types into a single defeq type