【发布时间】：2012-08-12 02:57:44
【问题描述】：
似乎有许多有用的矩阵数学应用程序，其中并非给定矩阵中的所有条目都共享相同的单位。我想研究可以跟踪这些单元并确保我们不会犯错误的类型系统（类似于已经对标量算术进行维度检查的许多库和语言）。我将举一个我所说的例子，然后我会从那里提出一些问题。
（抄袭here 中的一个随机混合单位线性规划示例，尽管这不是一个家庭作业问题，希望能变得清晰）
Bob 的面包店出售百吉饼和松饼。烤一打百吉饼 Bob 需要 5 杯面粉，2 鸡蛋，一杯糖。烤一打松饼 Bob 需要 4 杯面粉，4 鸡蛋和两杯糖。 Bob 可以以 10 美元/打的价格出售百吉饼和以 10 美元的价格出售松饼 12 美元/打。 Bob 有 50 杯面粉、30 个鸡蛋和 20 杯糖。 Bob 应该烤多少个百吉饼和松饼才能使他的收入最大化？
所以让我们把它放在矩阵形式（任意具体语法......）：
A = [ [ 5 cups of flour / dozen bagels, 4 cups of flour / dozen muffins ],
[ 2 eggs / dozen bagels, 4 eggs / dozen muffins ],
[ 1 cups of sugar / dozen bagels, 2 cups of sugar / dozen muffins ] ]
B = [ [ 10 dollars / dozen bagels, 12 dollars / dozen muffins ] ]
C = [ [ 50 cups of flour ],
[ 30 eggs ],
[ 20 cups of sugar ] ]
我们现在想要最大化内积B * X 使得A * X <= C 和X >= 0，一个普通的线性规划问题。
在带有单元检查的假设语言中，我们如何理想地表示这些矩阵的类型？
我认为 m x n 矩阵只需要 m + n 个单位，而不需要完整的 m * n 个单位，因为除非这些单位以合理的方式分布到行和列中，否则剩下的唯一合理操作就是用另一个形状完全相同的矩阵加/减完全通用的矩阵，或乘以一个标量。
我的意思是A中的单位排列比在：
WTF = [ [ 6 pigeons, 11 cups of sugar ],
[ 1 cup of sugar, 27 meters ],
[ 2 ohms, 2 meters ] ]
而且像后者这样的情况在实践中根本不会出现。 （谁有反例？）
在这个简化的假设下，我们可以用 m + n 个单位表示矩阵的单位如下。对于 m 行中的每一行，我们找出该行中所有条目共有的单位，对于 n 列也是如此。让我们将行单位放在列向量中，将列单位放在行向量中，因为这样会产生Units(M) = RowUnits(M) * ColUnits(M)，这似乎是一个不错的属性。因此，在示例中：
RowUnits(A) = [ [ cups of flour ],
[ eggs ],
[ cups of sugar ] ]
ColUnits(A) = [ [ dozen bagels ^ -1, dozen muffins ^ -1 ] ]
RowUnits(B) = [ [ dollars ] ]
ColUnits(B) = [ [ dozen bagels ^ -1, dozen muffins ^ -1 ] ]
RowUnits(C) = [ [ cups of flour ],
[ eggs ],
[ cups of sugar ] ]
ColUnits(C) = [ [ 1 ] ]
似乎（虽然我不确定如何证明...）M1 * M2 的单位是RowUnits(M1 * M2) = RowUnits(M1)、ColUnits(M1 * M2) = ColUnits(M2)，为了使乘法有意义，我们需要ColUnits(M1) * RowUnits(M2) = 1。
我们现在可以推断X 的单位，因为表达式A * X <= C 必须表示A * X 和C 具有相同的单位。这意味着RowUnits(A) = RowUnits(C)（签出）、ColUnits(X) = ColUnits(C) 和RowUnits(X) 是ColUnits(A) 转置的元素倒数，换句话说，RowUnits(X) = [ [ dozen bagels ], [ dozen muffins ] ]。
（“万岁”，我听到你在欢呼，“我们刚刚绕着月球转了一圈，看到了一些非常明显的东西！”）
我的问题是：
- 您能想到现实世界的示例，其中矩阵元素的单位不属于“行单位”和“列单位”吗？
- 你能想出一种优雅的方法来处理相同单元是每个单元格中的一个因素的情况，因此它可以等效地放置在每个“行”或每个“列”中，因此也可以放置在行单元和列中单位不是唯一的表示吗？将它们保持在“最低条件”并消除诸如将每一行乘以
furlongs ^ 17以便您可以将每一列乘以furlongs ^ -17的愚蠢条件应该是什么？ - 您能证明我提到的通过矩阵乘法传播这些单元注释的规则吗？
- 您能否发现/展示这些单元注释如何通过矩阵逆运算传播的规则？我对 2x2 矩阵进行的一些手工计算表明
Inverse(M)的单位是Transpose(M)单位的元素倒数，但我不知道如何在一般情况下显示它，即使它是一般情况下为真。 - 您是否知道有关这些问题的任何学术工作？或者对某种语言的程序执行这种静态分析的软件？我可能使用了错误的搜索字词，但找不到任何内容。
我感兴趣的实际应用是通过确保所有滤波器增益等在任何地方都有正确的单位来防止信号处理/控制器软件出现问题，在不同的单元格中使用具有不同单位的此类矩阵非常常见应用程序。
【问题讨论】：
-
5（在动态设置中）的部分答案是这个 python 库：inference.phy.cam.ac.uk/db410/dimpy/docs/docs/node5.html。它有一个奇怪的加法格式条件，不过我不太理解，而且它似乎没有讨论矩阵求逆。
-
哦，看起来Prof. George Hart 想通了这一切并写了a book。是时候参观图书馆了，如果它确实像看起来那样全面，请从亚马逊购买最后几本。
标签： linear-algebra units-of-measurement type-systems