Page 49 - 《软件学报》2025年第8期

3472 软件学报 2025 年第 36 卷第 8 期

lift 表示将一个实数转换为一维向量, 即实现从实数到向量的转换; drop 是 lift 的逆操作, 将一个一维向量转
∧
∧
∧
换为实数; real (2,1)finite_sum 表示一个类型为 real 2 的向量和一个类型为 real 1 的向量的拼接; fstcart 表示返回
给定拼接向量的第 1 个向量; sndcart 表示返回给定拼接向量的第 2 个向量; fspace 表示给定集合的连续函数空间;
mspace 表示特定区间; IMAGE 表示函数自变量在特定区间内的值域; has_vector_derivative 表示该向量值函数有
导函数.
条件 A1 表示给定一个从 t0 到 t1 的区间 , 在区间 中; 条件 A2 用于表示广义坐标和动能有导数的区间分
s
s t
s0、 s1; 条件 A3 ˙ θ ¨ x 和 组
¨ θ
θ
别是 表示广义坐标 q 由 x 和 组成, 广义速度 ˙ q 由 ˙ x 和 组成以及广义速度的导数 ¨ q 由
成; 条件 A4 表示广义坐标 x 的导函数为 , ˙ θ, 广义速度 ˙ x 的导函数为 , ¨ θ; 条件 A5 是
˙ x θ 的导函数为
¨ x ˙ θ 的导函数为
动能和势能的表达式, 拉格朗日量等于动能和势能之差, 即公式 (7); 条件 A6 表示公式 (9) 对应变量的值; 条件 A7
表示广义力和广义坐标的函数; 条件 A8 [22] 表示该系统满足的拉格朗日方程, 即公式 (8). 目标 G1 表示公式 (9) 的
形式化表示.
该定理的证明过程可分为如下 3 部分.
∂L 1
2
(1) 验证拉格朗日量对广义坐标 x 的偏导数 = − m t rl˙x sin(x)−m t rl˙x ˙ θsin(x)+m t glsin(x) 成立, 拉格朗日量对
∂x 2
∂L ∂L [ ]
2
2
广义坐标 θ 的偏导数 = 0, 拉格朗日量对广义速度 ˙ x 的偏导数 = I t +m t l +m t rlcos(x)+ I b +(m b +m t )r ˙x+
∂θ ∂˙x
∂L
[ 2 ] ˙ θ 2
I b +(m b +m t )r +m t rlcos(x) ˙ θ, 拉格朗日量对广义速度 的偏导数 = [I b +(m b +m t )r +m t rlcos(x)]˙x, 在验证过程
∂ ˙ θ
中, 涉及和的导数法则、差的导数法则、积的导数法则以及复合函数链式求导法则等数学定理的应用.
( )
d ∂L
2
2
(2) 验证拉格朗日量对广义速度 ˙ x 求导后再对时间 t 求导的导数 =[I t +m t l +m t rlcos(x)+ I b +(m b +m t )r ]¨x+
dt ∂˙x
I b +(m b +m t )r +m t rlcos(x) ¨ θ −m t rl˙x sin(x)−m t rlsin(x)˙x ˙ θ 成立, 之后, 对另一个广义速度 进行类似处理, 即验证
[ ]
˙ θ
2
2
( )
d ∂L [ ]
2
2
拉格朗日量对广义速度 ˙ θ 求导后再对时间 t 求导的导数 = [I b +(m b +m t )r +m t rlcos(x)]¨x+ I b +(m b +m t )r ¨ θ−
dt ∂ ˙ θ
2
m t rl˙x sin(x), 在验证过程中, 涉及向量点乘导数法则、向量复合函数求导链式法则等数学定理的应用.
(3) 验证广义力分别为 0 和 τ. 代入广义坐标和广义力等变量, 对广义力进行重写, 再应用导数相关定理得到广
义力的值. 最后, 将上述等式代入拉格朗日方程, 进行代换, 最终得到和结论的相同矩阵, 即完成该定理的证明. 在
对该定理进行形式化的过程中, 除了显性条件外, 还涉及许多隐含条件. 例如, 动能和势能在特定区间内有导函数,
这些都是验证过程中必须考虑的要求. 定理的条件涉及可导性、可微性以及导函数的存在等概念, 这些概念相似
又彼此关联, 增加了本文工作的复杂性. 此外, 验证过程中采用的策略以及对已知定理的运用, 也为验证工作带来
了诸多挑战.
[ ]
α+γ +2βcos(x) α+βcos(x)
在对该部分验证的过程中, 发现了两处系数错误. 在文献 [10] 中, 惯性矩阵 M(q) = ,
α+βcos(x) α
[ ] [ ]
−βsin(x)˙x 0 α+γ +βcos(x) α+βcos(x)
科氏力与离心力矩阵 C(q, ˙q) = , 本文经过改正, 正确的应为 M(q) = ,
−βsin(x)˙x 0 α+βcos(x) α
[ ]
−(1/2)βsin(x)˙x 0
且 C(q, ˙q) = , 随后进行了形式化描述, 顺利完成了证明.
−βsin(x)˙x 0
根据验证后的公式, 可以计算作用力与加速度之间的关系. 为更直观地说明这一关系, 我们将通过数值示例来
[ ] [ ]
α+γ +βcos(x) α+βcos(x) −(1/2)βsin(x)˙x 0
进行演示. 将惯性矩阵 M(q) = , 科氏力与离心力矩阵 C(q, ˙q) = ,
α+βcos(x) α −βsin(x)˙x 0
[ ]
−µsin(x)
重力矩阵 g(q) = 等参数代入公式 (9), 可以得到以下等式:
0
 2
2(α+γ +βcos(x))¨x+2(α+βcos(x)) ¨ θ −βsin(x)˙x −2µsin(x) = 0

 ,
2
 (α+βcos(x))¨x+α ¨ θ −βsin(x)˙x = τ
联立两式, 可得:

2
2γ ¨x+2βcos(x) ¨ θ +βsin(x)¨x −2µsin(x)+2τ = 0.