王國輝,許京然,劉永梅,施智平,關 永
1(首都師范大學 信息工程學院,電子系統(tǒng)可靠性技術北京市重點實驗室,北京 100048)2(首都師范大學 北京成像理論與技術高精尖創(chuàng)新中心,北京 100048)3(北京城市學院 信息學部,北京 101399)4(首都師范大學 電子系統(tǒng)可靠性與數理交叉學科國家國際科技合作示范型基地,北京 100048)
人造地球衛(wèi)星在地球引力的作用下沿閉合軌道繞地球做周期性運行.當地球是一個質量分布均勻的標準球體時,衛(wèi)星的軌道應該為標準的橢圓形,并服從開普勒三大定律.然而,地球表面高低起伏,地球內部結構復雜,使得地球引力在空間分布不均.人造地球衛(wèi)星在地球引力場的作用下,其運行軌道發(fā)生較為復雜的變換,產生攝動問題[1].因此,攝動開普勒問題在衛(wèi)星軌道分析研究過程中得到廣泛應用.該領域對安全性與可靠性要求非常嚴格,微小的錯誤將導致災難性后果.
早在1920年Levi-Civita就提出二維諧振子描述平面開普勒問題[2].1964年Kustaanheimo和Stiefel提出四維諧振子描述空間開普勒問題[3].這兩種類型將開普勒問題中的微分方程轉化為線性微分方程且都是可行的.1995年Vivarelli和Vrbik提出了利用四元數解決該問題的可行性[4].直到2006年Waldvogel利用四元數合理的解決了該問題并給出了推導方法與過程.從二維復數到三維四元數的代數轉換,是一次突破性進展[5].但是上述方法在解決衛(wèi)星攝動開普勒問題的建模與分析過程中涉及到矢量代數、旋量代數、復數、四元數等多種不同的代數系統(tǒng),在各個代數系統(tǒng)相互轉換過程中極易引入錯誤.2008年哈爾濱工業(yè)大學方茹等[6]提出了利用幾何代數解決攝動開普勒問題.該方法利用幾何代數將攝動開普勒問題的建模與分析統(tǒng)一到相同代數結構中,同時把攝動開普勒方程轉換成旋量方程來求解,有效避免奇點的同時彌補傳統(tǒng)分析方法的不足.
由于上述建模與分析方法主要依靠紙筆演算、數值計算和計算機代數系統(tǒng).紙筆演算的方法耗時耗力,容易引入人為錯誤;計算機數值計算方法由于計算機無法精確表示實數,數值計算不能給出精確的結果;計算機代數系統(tǒng)在邊界條件、奇異表達簡化方面的處理具有缺陷,此外龐大的符號計算程序不能排除程序漏洞的存在[7].相對于傳統(tǒng)的建模與分析方法,基于定理證明的形式化方法采用嚴格的高階邏輯描述數學問題的屬性和規(guī)范,以公認的邏輯公理和推理規(guī)則為基礎構建形式化建模和驗證過程,在安全攸關的系統(tǒng)設計中具有很大優(yōu)勢.
中國科學院李洪波[8]在2002年首次提出應用Clifford代數自動證明共形幾何模型,創(chuàng)立了高效的幾何計算和推理新方法.2013年Harrison等曾使用HOL Light對幾何代數的基本內容,主要包括多重矢量和基矢量做出了形式化定義,完成了幾何代數核心運算和部分性質的證明[9].2016年馬莎等[10]完成了共形幾何代數的高階邏輯形式化驗證工作,為幾何代數定理證明做了鋪墊.2018年李黎明[11]在HOL Light定理證明器中構建了幾何代數的高階邏輯定理庫,為攝動開普勒問題的形式化建模與分析提供了必要條件.本文通過定理證明的方法對基于幾何代數的攝動開普勒問題進行形式化建模與分析,并給出嚴格的高階邏輯推理,從而最大程度確保數學模型的正確性和分析方法的可靠性.
幾何代數是由Grassmann 代數和Clifford 代數發(fā)展而來的,能夠統(tǒng)一多種代數結構到同一框架下,從而避免多種代數系統(tǒng)之間相互轉換的問題.利用幾何代數中幾何體、幾何關系和幾何變換描述不依賴坐標的優(yōu)點,可以將描述衛(wèi)星軌道運動的攝動開普勒方程轉化為線性、正則旋量方程,即KS方程[12].
表1 幾何代數基本運算在定理證明庫中的表示Table 1 Representation of the basic operations of geometric algebra in the theorem proving library
幾何代數建立在多重向量空間上,其基本元素為多重向量.幾何代數運算主要包括內積、外積和幾何積.在使用過程中,內積還分為一般內積、左縮積、右縮積和標量積四種.在HOL Light定理證明庫中,幾何代數基本運算如表1所示.幾何代數基本運算不依賴研究對象的坐標系統(tǒng),只與坐標基之間的相對位置有關.其運算規(guī)則符合雙線性、結合律和分配律等基本性質,有效的統(tǒng)一了標量運算、矢量運算、維度運算和幾何運算.
本文以一般內積為例簡要介紹其定義及性質的高階邏輯形式化描述.其他運算的定義與性質可參見幾何代數的高階邏輯定理證明庫1.
定義1.幾何代數一般內積
|- x innerga y:real^(P,Q,R)geomalg =
Productga(s t.if s={} / t={} /
~(s SUBSET t)/~(t SUBSET s) then & 0
else --(& 1)pow CARD {i,j | i IN 1..(pdimindex(:P)
+pdimindex(:Q)+pdimindex(:R))/
j IN 1..(pdimindex(:P)+pdimindex(:Q)+
pdimindex(:R))/ i IN s / j IN t / i > j} *
--(& 1)pow CARD((pdimindex(:P)+
1..pdimindex(:P)+pdimindex(:Q))
INTER s INTER t)* & 0 pow
CARD((pdimindex(:P)+pdimindex(:Q)+
1..pdimindex(:P)+pdimindex(:Q)+
pdimindex(:R))INTER s INTER t))x y
其中real^(P,Q,R)geomalg為幾何代數基本元素多重向量的類型.
性質1.一般內積雙線性性質
|- bilinear f =(!x.linear(y.f x y))/
(!y.linear(y.f x y))
其中l(wèi)inear為線性性質描述.
|-linear(f:real^M->real^N)=
(!x y.f(x+y)= f(x)+f(y))/
性質2.一般內積結合律性質
|- !x y z.op x(op y z)= op(op x y)z
其中op為二元操作符.
由幾何代數基礎知識可知,歐式空間內的旋轉和伸縮變換滿足如公式(1)所示的歐式空間內矢量與幾何空間內的旋量或四元數之間的關系.
(1)
基于幾何代數理論的衛(wèi)星攝動KS方程涉及衛(wèi)星與地球的位置、速度和加速度的關系.因此需要構建多重向量微分及其基本定理的形式化,為開展攝動開普勒問題的形式化工作做準備.Maggesi等[13]在HOL Light系統(tǒng)中完成了向量函數的微分,本文以此為基礎,實現(xiàn)多重向量微分形式化.
定義2.多重向量函數f與微分函數f′之間的關系
|-(f has_ multivector _derivative f′)net <=>
(f has_multivector_derivative(x.drop(x)% f′))net
定義3.多重向量函數f在某點進行向量微分的函數值
|- multivector _derivative(f:real^1->(P,Q,R)geomalg)net=@f′.(f has_multivector _derivative f′)net
|- !x y:real^1->real^(′3,′0,′0)geomalg x′ y′ t.
(x has_ multivector _derivative x′)(at t)/
(y has_ multivector _derivative y′)(at t)
==>(( .(x t inner y t))
has_multivector _derivative
((x(t)inner y′)+x′ inner y(t)))(at t)
|-!x y:real^1->real^(′3,′0,′0)geomalg x′ y′ t.
(x has_ multivector _derivative x′)(at t)/
==>(( .(x t outer y t))
has_ multivector _derivative
((x(t)outer y′)+x′ outer y(t)))(at t)
|-!x y:real^1->real^(′3,′0,′0)geomalg x′ y′ t.
(x has_ multivector _derivative x′)(at t)/
==>(( .(x t * y t))
has_ multivector _derivative
((x(t)* y′)+x′ * y(t)))(at t)
上述三個多重向量函數運算微分的性質形式證明,為衛(wèi)星攝動開普勒問題形式化建模奠定了基礎.
人造地球衛(wèi)星在三維歐式空間的慣性坐標系中,衛(wèi)星與地球之間有微小且不可忽略的攝動力,在微小的攝動力f的作用下,系統(tǒng)的攝動開普勒方程可以表示為方程(2).
(2)
定義4.慣性坐標系中攝動開普勒方程形式化描述
|-multivector_derivative((multivector_derivative
(rotation_t r)(at t))(at t)=
((-k:real^1)*(r_position q t)/
norm(r_position q)pow & 3)+
(f:real^1->real^(′3,′0,′0)trip_fin_sum)
其中變量rotation_t r表示的是天體的矢量位置,它是一個與時間t有關的矢量函數;f是一個與時間t有關的多重向量函數;multivector_derivative f(at t)表示函數f對時間t的微分.k是一個實數,即公式(1)中的變量μ.
利用幾何代數相關理論,可以將攝動開普勒方程轉換為運動的旋量方程,記為KS方程.該方程形式簡單,計算方便,同時能夠有效消除引力位奇異點1/r,如方程(3)所示.
(3)
定義5.基于幾何代數的攝動開普勒方程形式化描述
|-& 2 % multivector_derivative
((multivector_derivative q)(at s))(at s)-(E_DEF q t k)*(q t)=q t*r_position u t *
(f:real^1->real^(′3,′0,′0)trip_fin_sum)
其中開普勒能量E定義6所示.
定義6.開普勒能量
|-E_DEF(q:real^1->real^(′3,′0,′0)geomalg)(t:real^1)(k:real)
=(& 2 %
((conjugation(multivector_derivative q(at t))*
(multivector_derivative q(at t)))MYMMYM {})- k)
/norm(r_position q t)
本小節(jié)將利用定理證明庫中已有的和補充的定義、定理對基于幾何代數的攝動開普勒方程進行形式化推導.根據能量守恒原則,證明上述兩種攝動開普勒問題建模分析方法的等價性.從而驗證了基于幾何代數的攝動開普勒方程的正確性與完備性.
在歐式慣性坐標系中,地球與人造地球衛(wèi)星中心相對位置矢量關系滿足公式(4):
(4)
其中u為采用幾何代數系統(tǒng)中多重向量的四元數表示,u+為u的共軛.
定義7.地球與衛(wèi)星相對位置矢量形式化
|-r_position(q:quat)=
(geomalg_300_quat q)* mbasis{1} *
conjugation(geomalg_300_quat q)
其中,quat為四元數類型.conjugation(u)表示u的共軛.e1是一個矢量基,用mbasis{1}表示.geomalg_300_quat表示四元數表示與多重向量表示的轉換,其形式化定義如定義7所示.
定義8.四元數與多重向量轉換形式化定義
|-geomalg_300_quat(q:quat)=
(Re q)% mbasis{} +(Im1 q)% mbasis{2,3} +
(Im2 q)% mbasis{1,2} +(Im3 q)%
(--(mbasis{1,3}:real^(′3,′0,′0)geomalg))
由地球與人造地球衛(wèi)星中心相對位置矢量關系公式(4)可得關系式(5):
(5)
定理1.地球與衛(wèi)星相對位置標量化
|-!q:quat.norm(r_position q)=
(norm(geomalg_300_quat q))pow 2
其中,norm表示矢量取模.
為了證明定理1的成立,需要引入兩個引理.即引理1位置矢量與多重矢量共軛的關系和引理2多重矢量與其共軛乘積的交互性.首先,用重寫策略(REWRITE_TAC)將定理1中的r_position和geomalg_300_quat定義展開.其次,運用化簡策略(SIMP_TAC)并結合HOL Light向量庫中的相關定理對目標進行化簡.最后,將定理目標推導為實數相等,并應用實數推導自動策略(REAL_ARITH_TAC)完成證明.
引理1.位置矢量與多重矢量共軛關系
|-!q:quat.norm(r_position q)% mbasis{}=
geomalg_300_quat q *
conjugation(geomalg_300_quat q)
引理2.多重矢量與其共軛積的交互性
|-!q:quat.conjugation(geomalg_300_quat q)*
geomalg_300_quat q=
geomalg_300_quat q *
conjugation(geomalg_300_quat q)
(6)
在形式化推導驗證過程中,直接證明公式(6)成立相對復雜,所以先由多重向量的共軛性質(u+)+=u去證明等式(7).
(7)
|-!q′ q:quat.
((geomalg_300_quat q′ * mbasis{1} *
geomalg_300_quat(cnj q))$${1,2,3}=& 0 )
==>conjugation(geomalg_300_quat q′*mbasis{1} *
geomalg_300_quat(cnj q))=
geomalg_300_quat q′*mbasis{1}*
geomalg_300_quat(cnj q)
|-!q′ q:quat.((geomalg_300_quat q′*mbasis{1}*
geomalg_300_quat(cnj q))$${1,2,3}=& 0 )
==>geomalg_300_quat q′*mbasis{1}*
geomalg_300_quat(cnj q)=
geomalg_300_quat q*mbasis{1}*
geomalg_300_quat(cnj q′)
根據引理3和引理4可以把公式(6)化簡,如公式(8)所示.
(8)
其高階邏輯形式化表示如定理2所示.
|-!q′:quat q:real^1->quat t:real^1.
((geomalg_300_quat q′*mbasis{1}*
geomalg_300_quat(cnj(q t)))$${1,2,3}=& 0 /
==>(( .(r_position(q t)))
has_multivector_derivative
(& 2 %(geomalg_300_quat q′*mbasis{1}*
geomalg_300_quat(cnj(q t)))))(at t)
公式(8)左右兩邊同乘e1u,再對時間t求導,可得公式(9).
(9)
其形式化描述為定理3.
|-!(q:real^1->real^(′3,′0,′0)geomalg)
(s:real^1->real^(′3,′0,′0)trip_fin_sum)(t:real^1).
& 2 % multivector_derivative((r_position q t)*
(multivectorr_derivative q(at t)))(at t)=
& 2 / norm(r_position q t)*
multivector_derivative(
(multivector_derivative q)(at s))(at s)
此時可以得到關于u對s的二次微分,如公式(10)所示.
(10)
(11)
為了證明公式(11)成立,在邏輯推導過程中仍需引入dt=rds表示t與s的關系,用引理5表示其形式化描述.
|-!(q:real^1->real^(′3,′0,′0)geomalg)(t:real^1)
(s:real^1->real^(′3,′0,′0)trip_fin_sum).
multivector_derivative s(at t)=
& 1 / norm(r_position q t)
通過上述推導,可以獲得地球與人造地球衛(wèi)星攝動開普勒問題的幾何代數高階邏輯模型,并且形式化證明了幾何代數方法構建衛(wèi)星攝動開普勒問題數學模型的正確性.
根據基于幾何代數的攝動開普勒方程公式(2)可知,公式(11)滿足攝動開普勒問題的旋量方程,根據能量守恒原則,可證如下公式(12)成立,
(12)
公式(12)可形式化為定理4,即開普勒能量守恒性質.
定理4.開普勒能量性質
|-!(q:real^1->real^(′3,′0,′0)geomalg)(t:real^1)
(k:real).E_DEF q t k =
(norm(multivector_derivative(r_position q)
(at t))pow 2 / & 2)-k/norm(r_position q t)
為了證明定理4的成立,需要證明開普勒能量引理,即引理6.
引理6.開普勒能量引理
|-!(q:real^1->real^(′3,′0,′0)geomalg)(t:real^1).
norm(r_position q t)*
(norm(multivector_derivative(r_position q)
(at t))pow 2)= & 4*norm
(multivector_derivative q(at t))pow 2
通過引理6的證明我們可以得到開普勒能量在幾何代數下的形式化描述.定理4以開普勒能量守恒為形式化驗證的最終目標.其證明過程主要借助上文提到的定義、引理和定理,運行重寫、化簡和自動求解等策略組合實現(xiàn)邏輯推導.從而證明攝動開普勒問題幾何代數模型與慣性坐標模型具有等價性.
本小節(jié)的重點是將攝動開普勒旋量方程的形式化建模與驗證.經過過嚴密的高階邏輯形式推導,最大程度確保基于幾何代數的攝動開普勒問題數學模型的正確性和分析方法的可靠性.
幾何代數系統(tǒng)能夠將多種代數系統(tǒng)統(tǒng)一在同一個代數系統(tǒng)中,避免了代數系統(tǒng)之間轉換問題,有效的提高了衛(wèi)星攝動開普勒問題分析的可靠性.本文以幾何代數為數學基礎,在高階邏輯定理證明器HOL Light中建立攝動開普勒方程邏輯模型,對攝動開普勒問題進行了形式化分析與驗證.由于解決攝動開普勒問題的需要,本文首先補充了幾何代數基本運算微分性質定理;其次完成從歐式空間到幾何代數空間的轉換關系進行形式化;再次形式化證明多重向量的線性性質、共軛性質以及共軛的線性性質;最后采用高階邏輯對基于幾何代數的衛(wèi)星攝動開普勒問題的數學模型進行形式化建模與推導,從而最大程度確保數學模型的正確性和分析方法的可靠性.
此外,攝動開普勒問題不僅應用于研究衛(wèi)星軌道和姿態(tài)運動,也是研究兩個帶電粒子的運動方程基礎,在測試物理理論和測量自然常數的模型系統(tǒng)中發(fā)揮了重要作用.因此下一步工作將圍繞基于幾何代數理論的微觀世界粒子運動方程的形式化建模與驗證展開.