似乎矩阵数学有许多有用的应用,其中并非给定矩阵中的所有条目都共享相同的单位。我想研究可以跟踪这些单元并确保我们不会犯错误的类型系统(类似于已经对标量算术进行维度检查的许多库和语言)。我将举一个我所说的例子,然后我有几个问题从那里开始。
(从这里抄写一个随机混合单位线性规划示例,尽管这不是一个家庭作业问题,希望会变得清晰)
鲍勃的面包店出售百吉饼和松饼。烤一打百吉饼 Bob 需要 5 杯面粉、2 个鸡蛋和 1 杯糖。烤一打松饼 Bob 需要 4 杯面粉、4 个鸡蛋和 2 杯糖。Bob 可以以 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)
,但我不知道如何在一般情况下显示它,或者即使对于一般情况也是如此。 - 你知道关于这些问题的任何学术工作吗?或者对某种语言的程序执行这种静态分析的软件?我可能使用了错误的搜索词,但我找不到任何东西。
我感兴趣的实际应用程序是通过确保所有滤波器增益等在任何地方都具有正确的单位来防止信号处理/控制器软件出现问题,在这些应用程序中,在不同单元中使用具有不同单位的此类矩阵非常常见。