几何代数由Clifford创建,又称Clifford代数.Clifford通过引入几何积的概念,使几何代数结合了Grassmann的扩张代数与Hamilton的四元数,实现了高维几何计算与分析的统一,使其有可能成为连接代数和几何、数学和物理、抽象空间和实体空间的统一的描述性语言^[1].几何代数是几何与代数的完美结合,近10年来,它在理论和应用研究上取得了突破式进展,成为重要的数学工具之一,并广泛应用于各个科学领域,如机器人学、计算机视觉、宇宙论、信息编码等,甚至有学者提出,将几何代数作为物理学和工程领域统一的数学语言^{[2, 3, 4, 5]}.

目前,利用几何代数为数学工具进行计算和建模,分析传统上使用纸笔演算、数值计算和计算机代数系统方法,然而这3种方法并不能完全保证结果的正确性和精确性:

· 纸笔演算的方法耗时耗力,容易引入人为错误;

· 计算机数值计算方法利用计算机软件进行几何代数的数值计算,例如MATLAB中的几何代数工具箱GABLE,由于计算机无法精确表示实数,计算的迭代次数受限于计算机内存和浮点数限制,数值计算不能给出精确的结果;

· 计算机代数系统(computer algebra systems,简称CASs)提供的处理几何代数符号方法,例如Maple,CLUCalc,Gaalop^[6]等,虽然利用核心算法可以精确推导出符号表达式的解,在一定程度上避免了数值计算解不精确的问题,但是对庞大的符号集进行运算的算法并没有经过验证,不能排除Bug的存在;并且在边界条件的处理上和奇异表达简化方面存在短板,所得到的结果仍然可能存在问题.

因此,这些传统的几何代数分析方法难以满足安全攸关系统的高可靠性要求^[7].为避免这些传统方法造成结果不精确等问题,对几何代数理论进行形式化分析是一种理想的解决办法.近几十年来,形式化方法在很多领域中都取得了巨大进步^{[8, 9]},基础研究的进展加上技术进步的推动,使新方法和新工具不断出现,并逐步完善成为一种成熟的高可靠验证技术.它的主要思想是,根据数学理论来证明所设计的系统满足系统的规范或具有所期望的性质.与人为笔纸分析和上述传统方法相比,形式化方法可根据数学逻辑的严密性提高发现微小而关键的早期设计错误的机率.高阶逻辑定理证明^[10]是形式化方法的一种,与模型检验方法^[11]相比,不能实现自动化证明,但是拥有更好的灵活性,从而能够处理结构大小不同的系统,其理论上的优势使其成为当前研究的最热点.综上所述,本文将使用高阶逻辑定理证明器对几何代数基本理论进行形式化验证.

定理证明的过程主要分为3个步骤:将现实的物理模型提取关键属性和性质转换为数学模型,描述成一系列的定义和待证明的定理;运用定理证明器中的Objective CAML(OCaml)语言和逻辑规则等将数学模型转换为逻辑模型,从而得到一个形式化系统;由专家给出每一步采用的证明策略,定理证明器根据给出的策略进行推导,直到定理证明成立为止,如果待证明的目标不成立,则需要考虑目标的建立是否严密完善.HOL-Light^[12]是最流行的定理证明器之一,不仅拥有庞大的研究团队和用户群,而且包含一系列高效的证明策略和丰富的数学定理库,如实数分析库、超越函数库、积分微分库等,为我们的工作开展提供了保障.目前,定理证明器技术在实际应用验证中也有一些成功的先例,例如运用HOL-Light定理证明器对两连杆平面机械手运动学分析验证^[13].本文选择HOL-Light进行验证的主要原因是:John Harrison在该定理证明器中对欧氏几何代数Cl_n进行过验证^[14],为我们工作的开展提供了有力保障.几何代数根据应用领域不同有几种不同的定义,其中,适应于几何应用和物理空间等应用领域中普遍采用典型的Cl_p,q,ρ形式,被称为空间Clifford代数.本文将对几何代数Cl_p,q,ρ进行形式化分析,内容主要包括4个部分.

(1) 对基本数据结构片积(blades)、多重矢量(multivectors)、单位正交基及其相关性质进行形式化定义与验证;

(2) 对核心运算几何积、外积、内积及其运算性质进行形式化定义与验证,并扩充其他基本运算,如几何反(reverse)、几何逆(inverse)、对偶(dual)、多重矢量求模等内容;

(3) 对变换算子如投影、反射、旋转等进行形式化建模分析;

(4) 基于几何代数Cl_p,q,ρ的形式化,在共形几何代数空间Cl_4,1,0中建立刚体运动的逻辑模型,并验证该模型的正确性.

第(2)部分是本文主要内容,也是主要难点.对第(2)、(3)部分的形式化分析与验证,不仅保证了几何代数的代数空间完整性,还凸显了几何代数的几何意义,扩展了HOL-Light中几何代数库的建模能力和应用范围.本文的主要贡献在于:利用定理证明方法对几何代数的基本理论进行验证推导成库后,能够最大限度地减少用户使用几何代数为数学工具研究其他代数理论、几何空间、应用领域的交互程度,例如部分(4)中,基于几何代数的形式化可以很容易构建出五维共形空间,并可以在该空间对刚体运动问题进行分析.

本文第1节介绍几何代数相关理论和相关研究的进展.第2节在高阶逻辑定理证明器中对几何代数的基本数据结构进行形式化.第3节对几何代数中基本运算及其性质进行形式化验证.第4节对变换算子进行形式化.第5节基于共形几何代数对刚体运动问题进行形式化建模与验证.第6节总结全文.

1 预备知识

为了更好地理解Harrison在几何代数形式化方面的工作以及与本工作的关系,首先简单介绍几何代数空间的理论知识,然后引出Harrison的工作,最后简单介绍李洪波实现的几何代数在机器证明方面的相关内容.

1.1 几何代数空间

几何代数Cl_p,q,ρ构建在矢量空间V^p,q,ρ上,是一个维数为2ⁿ的线性空间,其中,n=p+q+ρ,对于它的子空间,我们称作片积(blades).如果用e_i表示矢量空间中第i个单位正交基矢量,则几何代数系统Cl_p,q,ρ下,两个单位正交基的几何积可表示为

${e_i}{e_j} = \left\{ {\matrix{ {1,{\rm{ }}i = j \in 1,...,p} \hfill \cr { - 1,{\rm{ }}i = j \in p + 1,...,p + q} \hfill \cr {0,{\rm{ }}i = j \in p + q + 1,...,p + q + r} \hfill \cr {{e_i} \wedge {e_j} = - {e_j} \wedge {e_i} = {e_j},{\rm{ }}i \ne j} \hfill \cr } } \right.{\kern 1pt} $

(1)

其中,p,q,ρ分别代表几何代数空间中单位正交基几何积为+1,-1,0的个数.对于$e_i^2$=+1,-1,0,其中,i=1,2,…n,有3ⁿ种可能性,每一种可能性生成一个代数,因此,有3ⁿ个乘法规则的${R^{{2^n}}}$空间就形成3ⁿ个不同的2ⁿ维代数^[15].通过选取并定义不同单位基矢量间几何积的符号,可实现不同维度几何和代数空间定义,并保证不同空间中运算的坐标无关性^[16].当q=0,ρ=0时,矢量空间是熟知的欧几里得空间,具有欧氏度量,对应的几何代数空间可表示为Cl_n.此时,n相当于公式(1)中的p值,该空间的单位正交基的几何积均为正.

1.2 Harrison的几何代数形式化模型

Harrison等人曾使用HOL-Light对欧氏空间上的几何代数Cl_n的基本内容进行了形式化验证,并建立Clifford库,主要内容包括欧氏空间下多重矢量定义、基矢量定义、几何代数核心运算定义和部分简单线性性质等.该库总文本代码共979行,库中对欧氏几何代数的形式化,为我们的工作开展奠定了基础,但是仍然存在一定的局限性.欧氏几何代数虽然可以对3D基本几何实体和变换进行表达,但是欧氏几何代数中的齐次多重向量只能用来表达过原点的直线和平面,如果需要表达任意一条直线,则需要运用非齐次的多重向量;并且欧氏几何代数中的旋转和平移表达式不能统一为旋转子的变换,需要同时用到几何积和加法,具有非齐次性,这在实际应用中如机器人学中增加了计算的复杂度,通常并不可取.同时,Harrison的几何代数定义对于构造非欧几何空间如双曲几何、球体几何^{[17, 18]}有一定的难度,而几何代数系统Cl_p,q,ρ通过直接设置p,q,ρ的数值使代数构造和空间构造更加方便直接.所以从必要性上看,完成几何代数系统Cl_p,q,ρ的形式化不仅将几何代数所对应的空间扩展到非欧氏空间,即,不局限于单位正交基的几何积只为正的情况,更凸显了几何代数的几何意义,扩展了基于几何代数为数学工具的应用领域平台.

Clifford库中,将n维欧氏空间下的多重矢量表示为ρⁿ的列矩阵,HOL类型定义为real^(N) multivector,并且提供了表征n维多重矢量和2ⁿ个不同维度子空间的一一映射关系的相关定义及定理.库中还构建了lambdas函数和中缀符号“$$”表示多重矢量.

为了能更好地理解后文,这些定义与函数见表1.

表1中涉及到HOL-Light中二进制库(binary library)的部分函数,比较抽象.

其中,setcode函数分别涉及到函数binarysum,IMAGE和PRE,这些函数的定义和说明分别如下:

· ∀n,PRE 0=0∧(!n,PRE(SUC n)=n);

· ∀f s,IMAGE f s={y|∃x,x IN s∧y=f x};

· ∀s,binarysum s=nsum s(li.2 EXP i).

IMAGE函数是常用的值域函数,其中,f表示映射关系,s表示定义域,函数返回f函数中s对应的值域,类型为集合,当s为空时,IMAGE f{}={}.binarysum函数中,nsum是自然数求和函数,利用iterate函数迭代而成,其中,s表示后面映射的定义域,nsum返回的s所对应的值域的总和,当s为空时,nsum{} f=0.函数EXP的功能是求自然数的幂,在HOL中,实数的幂函数被定义为real_pow,可以看出,类型的匹配在HOL中是比较严格的.setcode函数的输入为集合s,返回的是自然数.

通过上述函数定义我们可以计算:

· 当s={}时,setcode{}=1+binarysum(IMAGE PRE{})=1;

· 当s={1}时,setcode{1}=1+binarysum(IMAGE PRE{1})=1+2^0=2;

· 当s={2}时,setcode{2}=1+binarysum(IMAGE PRE{2})=1+2^1=3;

· 当s={1,2}时,setcode{1,2}=1+binarysum(IMAGE PRE{1,2})=1+2^0+2^1=4;

依此类推,可以发现,setcode函数实现了从集合{1,2,…,n}到自然数x$ \in ${1,2,…,2ⁿ}的映射.

函数codeset也嵌套了IMAGE函数、SUC函数,其中,bitset函数为:

∀n,bitset n={i|ODD(n DIV(2 EXP i))}.

该函数输入是自然数n,返回的是集合.该集合返回的i值满足约束关系{i|x=n/2ⁱ∧x为奇数},通过该函数的定义,我们可以计算:

· 当n=1时,codeset 1=IMAGE SUC(bitset(1-1))={};

· 当n=2时,codeset 2=IMAGE SUC(bitset(2-1))=IMAGE SUC{0}={1};

· 当n=3时,codeset 3=IMAGE SUC(bitset(3-1))=IMAGE SUC{1}={2};

· 当n=4时,codeset 4=IMAGE SUC(bitset(4-1))=IMAGE SUC{0,1}={1,2}.

依此类推,可以发现:codeset函数是setcode的反函数,从自然数x$ \in ${1,2,…,2ⁿ}到集合{1,2,…,n}的映射.定理CODESET_SETCODE_BIJECTIONS验证两者的一一映射关系.

sindex函数表征s和setcode s的关系,(setcode s)返回与s相对应的自然数,x$$i表示多维向量x的第i个元素.因为HOL中将N维向量都表示成N维列矩阵,所以用$$符号取其元素.例如,当s={1,2,3}时,x$${1,2,3}=x$$8,x$$8表示取向量x中第8个元素.可见,通过符号$$可解析出多重矢量中对应不同子空间的大小.

lambdas函数调用了欧氏多维向量库(vectors library)^[19]中提供的lambda函数:

∀h,(lambda)h=(@f,∀i,1≤i∧i≤dimindex(:N)→f$$i=h i).

其中,函数lambdas和lambda调用了binder语法.在定义前,首先利用parse_as_binder语句声明:

· parse_as_binder “lambdas”;;

· parse_as_binder “lambda”;;

parse_as_binder “χ”中,χ的类型为string,作用可将χ (lx.y)结构简化为χ x.y,其中,(lx.y)表示以x为自变量y为映射关系的函数.声明为binder后,定义函数χ时需用括号包围起来,否则HOL解析失败.

lambda定义中,自变量函数h的类型为num→real,自然数到实数的映射函数.lambda函数的类型为(num→ real)→real^N,即,返回值为N维向量.其中,符号@表示有一个向量f满足后面的约束条件.dimindex(:N)为有限维数函数,dimindex(:N)函数的返回值为自然数,表示有限空间的维数为N.当i取1~N时,f的第i个元素等于h i,即h(i).

lambdas的定义嵌套了lambda函数,其中,i.γ(codeset i)是li.γ(codeset i)的简写,为lambda定义中的抽象函数h的具体形式.由于codeset函数返回的是自然数集合,类型为num→bool,所以γ的类型为(num→bool)→real,由自然数集合到实数的映射函数.lambdas函数的类型为((num→bool)→real)→real^(N)multivector,即,返回值为N维多重向量,由N个实数表示不同空间大小.codeset函数由于可构建子空间与整个多重矢量空间的关系,返回的集合(子空间下标)作为函数γ的自变量,最终返回对应的实数值.例如i=8时,f$$8=γ(codeset 8)=γ{1,2,3}.以公式(4)中的三维多重矢量A为例,i为8时,取出对应子空间e₁₂₃的大小a₁₂₃.最终,(lambdas)γ返回类型为real^(N) multivector,即,以不同阶数子空间的大小为元素组成集合来表征整个多重矢量空间,可用{a₀,a₁,a₂,a₃,a₁₂,a₂₃,a₃₁,a₁₂₃}来表示.

同理,函数mbasis调用lambdas,其中,s. if i=s then &1 else &0是ls. if i=s then &1 else &0函数的简写,是lambdas定义中的抽象函数γ的具体形式.其中,符号&将num类型转换为real类型.集合i表示片积子空间下标,如果集合i等于集合s,则该空间大小为1,否则为0.即,函数mbasis可表示基本片积函数.例如,mbasis{2,3}表示二阶基本片积e₂₃,mbasis{}表示0阶子空间即标量1.单位片积的定义仍然保留了多重矢量的类型和结构,在证明多重矢量各运算性质时,单位正交基可以进行匹配,只是某些子空间大小为0而已.

1.3 李洪波的几何代数机器证明

中国科学院的李洪波研究员自1994年起首次提出并应用Clifford代数于几何定理机器证明^[20],创立了高效的几何计算和推理新方法,这是数学机械化向核心数学发展的重要一步.方法的主要思想是:结合吴方法与几何的Clifford代数表示进行几何定理机器证明,建立了基于Clifford向量代数的解多向量方程组方法,特别是首次创立了Clifford括号代数,它以广义Grassmann-Plücker关系为基础,是一种高效的代数工具.与本文方法最大的区别在于:本文对几何代数的验证是基于逻辑推理并在一个相对可靠的环境下进行的,验证过程是通过定理证明器或用户编译的推理规则和已有的定理库进行推导.本方法侧重在定理证明器中根据几何代数数学理论建立逻辑模型,然后用建立的逻辑模型对基于几何代数的系统或者算法的规范或具有所期望的性质进行验证, 在不能证明所期望的性质时,则可能发现早期设计错误.整个过程要求使用者具有严密的思维和具备一定的逻辑推理经验.

2 片积与多重矢量的形式化

片积和多重矢量是几何代数空间中最基本的代数元素.由于叉积只在三维空间内有效的局限性,几何代数引入了外积.矢量a,b的外积是两矢量在空间中张成的有方向并且有边界的平面区域,称作二重矢量或二元矢量(bivector),记作a∧b.如果再将二重向量a∧b沿着一个矢量χ去延伸就得到定向体积元a∧b∧χ,称为三重矢量或三元矢量(trivector),如图1所示.

普遍地,k个线性无关的多维矢量的外积称作k阶片积(k-blade),表示为

Ak=a1∧a2∧…∧ak

(2)

片积中,线性无关的向量个数称为片积的阶数,阶数k用于表达片积的空间维度数.例如:标量(scalar)的阶数为0,即,零维子空间;矢量的阶数为1,即,一维子空间;二重矢量的阶数为2,即,二维子空间.如果采用k-blades表示所有阶数为k的blade,则标量可表达为0-blade,矢量为1-blade,二重矢量为2-blade.值得注意的是:几何代数中,描述和计算几何实体的基本元素不是向量,而是具有更广泛意义的子空间,因此,向量只能作为一维的子空间.

N维几何代数空间中共有2^N个片积,即,由0阶片积,1阶片积,…,N阶片积张成.例如,三维几何代数空间的基本片积为{1;e₁,e₂,e₃;e₁₂,e₂₃,e₁₃;e₁₂₃},其中,e_ij=e_i∧e_j,e_ijk=e_i∧e_j∧e_k.通常地,阶数最高的基本片积e₁₂₃称作该空间的伪标量(pseudoscalar).

N维多重矢量由不同阶数的片积线性组合而成,最高阶为N.由于阶数用于表达片积的空间维度数,所以多重矢量是通过“+”号连接不同维数子空间的表达式.所以顾名思义,叫做“多”重矢量.若〈〉_i为维度提取运算符,则可解析出多重矢量A中维度为i的片积,记作:

$A = {\langle A\rangle _0} + {\langle A\rangle _1} + ... + {\langle A\rangle _n} = \sum\limits_{k = 0}^n {{{\langle A\rangle }_k}} $

(3)

以三维多重矢量A为例,其数学表达和结构为:

$\eqalign{ & \{ 1\} ,\{ {e_i}\} ,\{ {e_i} \wedge {e_j}\} ,\{ {e_i} \wedge {e_j} \wedge {e_k}\} ,...,\{ {e_1} \wedge {e_2} \wedge ... \wedge {e_{p + q + r}}\} \cr & \{ 1\} ,\{ {e_i}\} ,\{ {e_{ij}}\} ,\{ {e_{ijk}}\} ,...,\{ {e_{12...(p + q + r)}}\} \cr} $

(4)

其中,a₀为标量部分,阶数和维度为0;a₁e₁+a₂e₂+a₃e₃为向量部分,阶数和维数为1;a₁₂e₁₂+a₂₃e₂₃+a₃₁e₃₁为二重矢量,阶数和维数为2,该二重矢量可由两个线性不相关的三维向量外积所得,其中将用到外积的运算性质进行化简;a₁₂₃e₁₂₃为三重矢量,阶数和维数为3.

通过上述定义知,几何代数空间Cl_p,q,ρ共有2^(p+q+ρ)个不同阶数的基本片积张成:

$A = \underbrace {{a_0}}_{} + \underbrace {{a_1}{e_1} + {a_2}{e_2} + {a_3}{e_3}}_{} + \underbrace {{a_{12}}{e_{12}} + {a_{23}}{e_{23}} + {a_{31}}{e_{31}}}_{} + \underbrace {{a_{123}}{e_{123}}}_{}$

(5)

不难看出,该空间的任意基本片积e_s,s一定是{1,2,…,(p+q+ρ)}的子集.若用集合来表示相对应的基本片积对应的下标,则利用集合的运算操作可以实现几何代数空间中子空间的运算,并且非常明晰方便.所以,后文将用集合来表示相对应的基本片积对应的下标,很多定义和性质证明过程都与集合定义及定理紧密有关.

下面对Cl_p,q,ρ空间的多重矢量的类型进行定义.在HOL-Light中,先需利用构建类型new_type_definition语句来定义多重矢量标识名称multivector,由于Cl_p,q,ρ中的多重矢量是2^(p+q+ρ)个不同阶数的片积线性组合,所以需要构建一个集合s,该集合s是{1,2,…,(p+q+ρ)}的幂集.多维向量库中,利用笛卡尔运算符“^”将n维实向量空间ρⁿ表示成real^N;同时,由于笛卡尔库中有限维数求和定理DIMINDEX_FINITE_SUM的支持,可将N分拆成(p,q,ρ)的形式.最终将几何代数Cl_p,q,ρ框架下的多重矢量类型定义为real^(p,q,ρ)multivector的形式,其中,p,q,ρ均是num型,分别代表几何代数空间Cl_p,q,ρ中单位矢量几何积为+1,-1,0的个数.该类型是贯穿本文的基本运算对象,标量和向量都可看做多重矢量,统一为该类型进行运算.

利用幂集的势等定理HAS_SIZE_POWERSET,易证几何代数空间Cl_p,q,ρ的维数为2^(p+q+ρ):

dimindex(:(p,q,ρ)multivector)=2 EXP (dimindex(:p)+dimindex(:q)+dimindex(:ρ)).

由于lambdas函数、符号”$$”可以用来解析一个多重矢量,例如,符号”$$”可以实现多重矢量中子空间的线性运算:

· 子空间相加:

∀x y s,s SUBSET (1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ)))→(x+y)$$s=x$$s+y$$s;

· 子空间减乘:

∀x y s χ,s SUBSET (1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ)))→(χ%x-χ%y)$$s=(χ%x)$$s-(χ%y)$$s.

其中,x,y为多重矢量,s为集合,符号“..”是HOL-Light定理证明器iter库的闭区间函数,符号“%”是标量与矢量相乘运算符.同理,通过限定集合的势为k,即,从多重矢量中取出阶数为k的部分,可得到k阶片积的定义:

定义1. k-blade:

∀k p,blade k p=lambdas s. if s HAS_SIZE k then p$$s else &0.

由于任意多重矢量由基本片积线性组合而成,基本片积的定义和运算性质非常重要.对几何代数Cl_p,q,ρ框架下的基本片积的相关性质的形式化验证,部分如下所示.

定理1. 多重基矢量的组成:

∀s τ,s SUBSET (1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ)))→(mbasis τ)$$s=if s=τ then &1 else &0.

定理2. 多重矢量的展开式:

∀x,vsum{s|s SUBSET 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))}(ls.x$$s%mbasis s)=x.

定理3. k阶blade的展开式:

∀x k,vsum{s|s SUBSET 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧(s HAS_SIZE k)}(ls.x$$s%mbasis s)=blade k x.

定理4. 多维矢量到多重矢量的单映射函数:

∀x,multivec x=vsum(1..dimindex(:N))(li.x$$i%mbasis{i}).

定理2中,利用多维矢量求和函数vsum来生成多重矢量x,其中,vsum的定义为

vsum s f=lambda i.sum s(lx.f(x)$$i).

该函数的类型为(A→bool)→(A→real^N)→real^N,vsum有两个自变量,分别为集合s和以集合s作为定义域的函数f.最终,函数返回为N维实向量.该函数功能是对N维向量函数求和.

定理2嵌套vsum函数后,表示对集合{1,2,…,p+q+r}的每一个子集s做x$$s % mbasis s操作然后求和.定理3表示x中的k阶blade部分是{1,2,…,p+q+r}的幂集中个数为k的集合作为自变量生成的基本片积线性组合而成.定理4中,(multivec:real^(N)→real^(p,q,ρ)multivector)实现了N维矢量到多重矢量的映射,表示对N维向量的第i$ \in ${1,…,N}个元素做x$$i%mbasis{i}操作,然后利用矢量求和函数vsum相加构成相对应的多重矢量.在证明过程中,除了需要处理集合的定理以及求和定理等,还主要用到以下两个定理:

定理5. 多重矢量相等的充要条件:

∀x y,x=yÛ∀s,s SUBSET 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))→x$$s=y$$s.

定理6. 处理lambdas函数:

∀s,s SUBSET 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))→((lambdas) γ)$$s=γ s.

3 几何代数的基本运算

本节先对几何代数空间Cl_p,q,ρ中的核心运算内积、外积、几何积的运算规则进行理论分析,根据分析进行归纳总结,最终描述成形式化定义.由于多重矢量由不同阶数的基本片积线性组合而成,而3个核心运算都满足加法分配律,故多重矢量之间的核心运算都可以先分别展开,最终演算成不同阶数的基本片积运算.这是两个多重矢量间进行3个运算的统一步骤,所以可以在具体定义运算之前先定义一个抽象积,不仅能够体现多重矢量运算的结构特征,并且对运算性质的证明提供了匹配性的可能.更重要的是,几何积、外积、内积的形式化定义分别调用抽象积的函数,可以很大程度上简化定义的复杂度.

由于核心运算规则各不相同,基本片积的表示和运算可以利用集合进行操作,故可使用抽象函数op对基本片积对应的集合s,τ进行操作来反映运算规则.另外,由于几何代数空间Cl_p,q,ρ中单位正交基矢量几何积包括+1,-1,0这3种情况,故在基本片积运算时需要判断基矢量在几何代数中所属空间的符号,所以还需要构造一个mult函数对几何积符号正、负、零进行判定和控制,即公式(1)所述.

定义2. 抽象积:

Product mult op x y=
   vsum{s|s SUBSET 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))}
   (λs.vsum{s|s SUBSET 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))}
   (λt.(x$$s*y$$τ*mult s τ)%mbasis(op s τ))).

上述定义中,函数HOL类型为real^(p,q,ρ)multivector→real^(p,q,ρ)multivector→real^(p,q,ρ)multivector,即,两个多重矢量进行抽象积后仍然是多重矢量.s和τ分别代表x,y的抽象子空间下标,由于x和y都是几何代数Cl_p,q,ρ框架下的多重矢量,则s和τ是集合{1,2,…,p+q+ρ}的子集.该定义嵌套了两个vsum函数.因为x,y要分别进行展开.x$$s表示x中的子空间e_s的大小,y$$τ表示y中的子空间e_t的大小.由于基本正交基在几何代数中所属空间的符号不同,即公式(1)所述,所以利用mult函数进行判断.显然,(mult s τ)函数的返回值只有 +1,-1,0这3种情况.mbasis (op s τ)为运算后的基本片积.在后文的几何积、外积、内积的形式化定义中,mult函数和op函数都有具体的函数表达式,主要是mult函数比较复杂.

3.1 外 积

外积是升维运算,主要用于维度扩充和形体构建.两线性无关对象外积结果维数等于参与运算对象维数之和.当A,B线性相关时,其外积为0,这是外积很重要的一个性质.另外,外积还有反对称性a∧b=-b∧a.根据线性相关性和反对称性,得到一阶基本片积的外积运算规则:

$\left\{ {\matrix{ {{e_i} \wedge {e_i} = 0} \hfill \cr {{e_i} \wedge {e_j} = {e_{ij}}} \hfill \cr {{e_j} \wedge {e_i} = - {e_{ij}}} \hfill \cr } } \right.$

(6)

根据上式对多重矢量x,y的外积运算进行形式化定义.

定义3. 外积:

∀x y,x outer y=

 Product (ls τ. if ~(s INTER τ={}) then &0

  else --(&1) pow CARD {i,j|i IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

    j IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

    i IN s ∧ j IN τ ∧ i>j})

  (UNION)

  x y

外积的mult函数首先利用if..else条件控制语句进行判断,定义中,~(s INTER τ={})表示x和y存在相等的子空间,此时,mult s τ的返回值为0,否则进行else后面的操作.这体现了外积的线性相关性.else后面的语句虽然繁琐,但只是判断mult s τ的返回值是1还是-1,它由满足后面合取式条件的点对(i,j)的个数决定,其中,CARD函数功能是求集合的势.当i,j在1和p+q+ρ范围内并且i> j时,结果积累一个负号,最后通过负号的总个数来判断结果的正负号.op函数利用集合库sets中的并操作UNION来确定进行外积运算后的多重基矢量,根据公式(6)很容易看出,应该是集合s,τ的并集.注意:这里不需要考虑是否去掉交集部分,因为存在交集时mult s τ等于0,与mbasis (op sτ)相乘结果直接为0.

该定义比较抽象难懂,这里举一个简单的实例详细说明整个外积计算过程.以几何代数Cl_4,1,1为例,p取4,q取1,ρ取1.后文几何积、内积的形式化定义计算过程类似.

计算几何代数Cl_4,1,1框架下x=3e₁₃₆+2e₄,y=2e₂₅的外积.

过程:

· 第1步,根据定义2分别展开,由于{1,3,6},{4},{2,5}都是{1,2,…,6}的子集,所以都参与vsum函数运算,并且可知,x$${1,3,6}=3,x$${4}=2,y$${2,5}=2;

· 第2步,根据定义3计算两者外积,主要是逐一计算(mult s τ)和(op s τ)的返回值.首先,将x中的e₁₃₆和y中的e₂₅进行外积,此时,s={1,3,6},τ={2,5}.由于s INTER τ={}进行else后面操作,满足合取式条件的点对个数有card{i,j|…}=card{(3,2),(6,2),(6,5)}=3,所以(mult s τ)=(-1)³=-1;而op s τ相对应等于{1,2,3,5,6}.按照同样的方法求e₄和e₂₅的外积,得到card{i,j|…}=card{(4,2)}=1,则:

(mult s τ)=(-1)¹=-1,(op s τ)={2,4,5};

· 第3步,将求到的(mult s τ)和(op s τ)带入定义2中,求得最终结果为

(x$${1,3,6}*y$${2,5}*(mult {1,3,6} {2,5}))%mbasis(op {1,3,6} {2,5})+
(x$${4}*y$${2,5}*(mult{4} {2,5}))%mbasis(op {4} {2,5})=
(3*2*-1)%mbasis{1,2,3,5,6}+(2*2*-1)%mbasis{2,4,5}=-6e₁₂₃₅₆-4e₂₄₅.

这与理论计算结果一致,证实了抽象积和外积的形式化定义的正确性和有效性.由于几何代数Cl_p,q,ρ空间中存在q,ρ部分,区别于欧氏几何代数,所以对该空间中基矢量之间的运算规则总结十分必要.定理的描述和运算定义是紧密相连的,本文根据运算规则对Cl_p,q,ρ空间的基本片积运算做了大量的形式化,分别会在介绍运算定义后给出相对应的基本片积运算定理.基本片积运算定理在HOL-Light中的验证不仅是多重矢量运算验证的重要基础支撑,反过来还验证了3个核心运算形式化定义的有效性和正确性.下面给出具有代表性的一阶基本片积的外积运算,对应公式(6).N阶基本片积运算定理根据定义可以总结出,这里限于篇幅不列出.

定理7. 一阶基本片积外积运算:

∀i j,mbasis{i}outermbasis{j}=

 if i IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

  j IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

  ~(i=j)

  then if i<j then mbasis{i,j} else --(mbasis{i,j})

 else vec 0

3.2 内 积

内积是降维运算,注意,几何代数中的内积和向量代数中的标准内积即数量积(dot product)不相同.几何代数的内积运算对象既可以是同维度空间对象也可以是不同维度空间对象,即,可以是不同阶数的片积进行运算.内积能够表达复杂空间对象的距离、角度等几何和拓扑属性,但是向量a,b的内积计算与向量代数中标准点积是类似的,返回值是标量.在计算机科学等领域中收缩内积很有使用价值,较多资料中对几何代数空间中的内积都采用左缩积来定义.本文根据需要采用左缩积定义内积,即:当左边的对象维度大于右边的对象维度时为0,并不满足交换律.用运算符左缩“⌋”对其描述:

${\langle A\rangle _s}\,{\langle B\rangle _t} = {\langle AB\rangle _u}{\rm{ where }}u = \left\{ {{\kern 1pt} \matrix{ {s > t,{\rm{ }}0} \hfill \cr {s \le t,{\rm{ }}t - s} \hfill \cr } } \right.$

(7)

其实,多重矢量A到B内积的计算过程是求B中与A正交的组成部分.一阶基本片积的内积运算规则如下:

$\left\{ {\matrix{ {{e_i}\,{e_i} = {e_i}{e_i}} \hfill \cr {{e_i}\,{e_j} = 0} \hfill \cr } } \right.$

(8)

根据上式对多重矢量x,y的内积运算进行形式化.

定义4. 内积:

∀x y,x inner y =

 Product (ls τ. if ~(s SUBSET τ) then &0

  else --(&1) pow CARD {i,j|i IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

    j IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

    i IN s∧j IN τ∧i>j}*

   --(&1) pow CARD {i,j|i IN (dimindex(:p)+1)..(dimindex(:p)+dimindex(:q))∧

    j IN (dimindex(:p)+1)..(dimindex(:p)+dimindex(:q))∧

    i IN s∧j IN τ∧i=j}*

&0 pow CARD {i,j|i IN (dimindex(:p)+dimindex(:q)+1)..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

    j IN (dimindex(:p)+dimindex(:q)+1)..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

    i IN s∧j IN τ∧i=j})

    (ls τ.(s DIFF τ) UNION (τ DIFF s))

    x y

先利用中缀符号语句parse_as_infix(“inner”,(21,“left”))定义内积是左结合运算符,其中,~(s SUBSET τ)表示内积左边的对象维度大于右边的对象维度.当满足这个条件时,mult s τ的返回值为0,体现了内积的方向性.else后面的式子是判断mult s τ的返回值是1,-1,0:当s SUBSET τ时,若s为空集,即,多重矢量x中有标量成分,则该标量与y中基本片积的内积等于它们的几何积;若s非空集,则~(s INTER τ={}),那么外积为0,此时,基本片积矢量运算的内积也等于几何积.当满足s SUBSET τ时.它们的内积都等于几何积,故else后面的形式化代码与几何积相同.该代码的含义在第3.3节介绍几何积时详细解释.下面根据该定义给出一阶基本片积内积运算定理,该定理与一阶基本片积几何积运算,即定理9的验证过程思想类似.

定理8. 一阶基本片积内积运算:

∀i j,mbasis{i} inner mbasis{j}=

  if i IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

   j IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))

    then if i=j then if i IN 1..dimindex(:p)∧j IN 1..dimindex(:p) then mbasis{}

     else if i IN (dimindex(:p)+1)..(dimindex(:p)+dimindex(:q))∧

      j IN (dimindex(:p)+1)..(dimindex(:p)+dimindex(:q)) then --mbasis{}

       else vec 0

    else vec 0

  elsevec 0

3.3 几何积

作为几何代数的核心运算,几何积通过连接内积与外积实现向量空间表达和不同维度混合运算,是构建几何代数空间的基础.对于任意s阶片积A和τ阶片积B,两者几何积运算可表示为

〈A〉s〈B〉t=〈AB〉|s-τ|+〈AB〉|s-τ|+2+…+〈AB〉s+τ

(9)

式(9)反映了两个片积参与几何积运算后的维度构成.可以看出,向量a,b的几何积等于两者外积与内积之和.多重基矢量的几何积运算规则总结如下:

(1) 阶数高于1的基矢量可写成垂直向量的外积形式,因为它们的内积为0.例如,在高维空间中可以写为

e₁₂₄₅₈=e₁∧e₂∧e₄∧e₅∧e₈.

(2) 交换两个不相等的基矢量顺序时,结果取负:

e₁e₂e₄=-e₂e₁e₄=e₂e₄e₁.

(3) 一个基矢量与其本身相等并且相邻,根据公式(1)进行化简.例如在Cl_4,1,1中:

e₁e₁e₃e₄e₅e₅=-e₃e₄=-e₃₄,e₁e₁e₃e₆e₆=0.

根据规则(3)可以看出:两个相等的基矢量相邻,那么该基矢量可以直接去除或者使最终结果为0.根据上述规则,对多重矢量之间的几何积定义为定义5.

定义5. 几何积:

∀x y,x*y=

  Product (ls τ.--(&1) pow CARD {i,j|i IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

    j IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

    i IN s∧j IN τ∧i>j}*

   --(&1) pow CARD {i,j|i IN (dimindex(:p)+1)..(dimindex(:p)+dimindex(:q))∧

    j IN (dimindex(:p)+1)..(dimindex(:p)+dimindex(:q))∧

    i IN s∧j IN τ∧i=j}*

   &0 pow CARD {i,j|i IN (dimindex(:p)+dimindex(:q)+1)..(dimindex(:p)+dimindex(:q)+

    dimindex(:ρ))∧

    j IN (dimindex(:p)+dimindex(:q)+1)..(dimindex(:p)+dimindex(:q)+

     dimindex(:ρ))∧

    i IN s∧j IN τ∧i=j})

   (ls τ.(s DIFF τ) UNION (τ DIFF s))

   x y

几何积的名称和运算符号利用HOL-Light定理证明器重载符号语句overload_interface (“*”,‘geom_mul: real^(p,q,ρ)multivector→real^(p,q,ρ)multivector→real^(p,q,ρ)multivector’)进行声明.该符号“*”虽然与实数乘法运算标识符“*”形式上相同,但根据运算对象的HOL类型做不同的运算:当为实数real,做相乘运算;当为多重矢量real^(p,q,ρ)multivector,则做几何积运算.mult函数中:当i,j在1和p+q+ρ范围内并且i>j时,结果提供一个负号,对应上述规则(2);当i和j相等且在p+1和p+q范围内时,结果提供一个负号;当i,j相等且在p+q+1和p+q+ρ范围内时,mult s τ的返回值为0,对应规则(3).op函数利用并操作UNION和差操作DIFF来确定进行几何积运算后的多重基矢量空间.(s DIFF τ) UNION (τ DIFF s)表示s和τ的并集再减去两者的交集的部分,对应规则(3),即,最终的基矢量一定由两集合的不相交部分构成的.下面根据几何积定义分别给出多重基矢量和一阶基本片积的几何积运算规则.

定理9. 多重基矢量几何积运算:

∀s τ,mbasis s*mbasis τ=

   if s SUBSET 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧τ SUBSET 1..(dimindex(:p)+dimindex(:q)+

    dimindex(:ρ))

   then --(&1) pow CARD {i,j|i IN s∧j IN τ∧i>j}%mbasis((s DIFF τ) UNION (τ DIFF s))

  else vec 0

定理10. 一阶基本片积几何积运算:

∀i j,mbasis{i}*mbasis{j}=

  ifi IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧j IN 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))

   then ifi=j then if i IN 1..dimindex(:p)∧j IN 1..dimindex(:p) then mbasis{}

    else if i IN (dimindex(:p)+1)..(dimindex(:p)+dimindex(:q))∧

     jIN (dimindex(:p)+1)..(dimindex(:p)+dimindex(:q)) then --mbasis{}

     elsevec 0

   else ifi<j then mbasis{i,j}

   else--(mbasis{i,j})

  elsevec 0

定理9主要根据几何积定义可以验证得出.定理10处理e_i和e_j的几何积运算,对应公式(1).该定理真正反映了p,q,ρ的代数意义,非常重要.定理的描述看上去比较复杂,但是思维明确清晰:首先,当i和j不属于{1,2,…,p+q+ρ},结果为零矢量;否则进行运算,然后分3种情况:i=j,i<j,i>j:

⌉ 当i<j时,结果为e_ij;

⌉ 当i>j时,结果为-e_ij;

⌉ 当i=j时,再分3种情况:当i,j属于{1,2,…,p}中,为1;当i,j属于{p+1,…,p+q}中,为-1;否则为0.

定理10的验证过程:首先,重写几何积定义(定义5)、集合库中处理IN函数如IN_NUMSEG,IN_SING等定理将式子展开和化简;然后针对if..else语句,利用定理证明器中的COND_CASES_TAC策略将目标根据判断条件拆分成子目标依次证明.由于该目标嵌套的if..else语句较多,每次证明完一个子目标要继续用该策略进行拆分.这些子目标的证法各不相同但思想一样,在证明过程中,又根据需要建立了10个子目标,子目标的建立是为了化简一些形式非常复杂类似{i,j|…}的集合表达形式,化简的依据是当前假设列表的推导.例如在证明第6个子目标的过程中,当前目标中存在这个集合:

{i',j'|(dimindex(:p)+dimindex(:q)+1≤i'∧i'≤dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

  (dimindex(:p)+dimindex(:q)+1≤j'∧j'≤dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧

  i'=j∧

  j'=j∧

  i'=j'}

而当前假设列表为:

0 [‘(1≤i∧i≤dimindex(:p)+dimindex(:q)+dimindex(:ρ))∧1≤j∧j≤dimindex(:p)+dimindex(:q)+dimindex(:ρ)’]

1 [‘i=j’]

2 [‘~(j≤dimindex(:p))’]

3 [‘~(dimindex(:p)+1≤j∧j≤dimindex(:p)+dimindex(:q))’]

4 [‘~(j≤dimindex(:p)+dimindex(:q))∧j≤dimindex(:p)+dimindex(:q)+dimindex(:ρ)’]

目前,假设列表分别有5个假设,是合取的关系,可以根据假设列表推导建立子目标:该集合等于{(j,j)}.子目标的证明首先运用处理点对的定理EXTENSION,FORALL_PAIR_THM,IN_ELIM_PAIR_THM,PAIR_EQ等进行展开化简;然后,针对不等式问题利用不等式定理LE_SUC_LT,NOT_LE,LT_REFL等处理.验证过程中有7个子目标,根据当前假设列表推导需要证明当前目标中复杂的集合表达式是为空集的.这些证明过程类似,均需要空集相关定理如NOT_IN_EMPTY等.注意,假设列表根据证明推导和if…else语句是变动的,所以验证过程比较复杂,每一步的策略运用和定理重写都是根据当前目标和当前假设作为依据.其中,根据当前假设列表验证的过程中会涉及到分情况讨论可利用策略ASM_CASES_TAC和MAP_EVERY ASM_CASES_TAC完成.由于过程中涉及到很多CARD{i,j|…}之类的点对集合求势问题,为了简化计算,本工作证明了很多引理,将具有代表性的引理展示如下:

引理1. 方阵对角线右上方和左下方元素个数相同:

CARD{i,j|i IN 1..N∧j IN 1..N∧i>j}=CARD{i,j|i IN 1..N∧j IN 1..N∧i<j}.

引理2. 方阵对角线右上方元素个数总和:

CARD{i,j|i IN 1..N∧j IN 1..N∧i>j}=(N*(N-1)) DIV 2.

3.4 运算性质的形式化证明

外积、内积、几何积都满足双线性性质,通过双线性性质,可以很容易验证三者简单的线性性质.定理11验证抽象积具有双线性性质,由于三者都调用了抽象积的定义,故三者的双线性性质匹配定理11即可.其中,双线性性质和线性性质如下:

· ∀f,bilinear f«(∀x,linear(ly.f x y))∧(∀y,linear(lx.f x y)).

· ∀f,linear f«(∀x y,f(x+y)=f(x)+f(y))∧(∀c x,f(χ%x)=χ%f(x)).

根据双线性性质,即,在二元函数f(x,y)中对自变量x,y分别都是线性的,证明得到抽象积函数(Product mult op)满足双线性性质:

定理11. 双线性性质:

∀mult op,bilinear(Product mult op).

该定理的证明主要运用bilinear定义、linear定义以及多维矢量基本运算性质等.下表列出几何积的基本运算性质.外积和内积性质类似.

注意:几何积和外积具有结合性质,内积由于其特殊的方向性不具备结合性质.其中,几何积结合性质验证比较复杂,需要证明以点对(i,j)为元素组成的集合有限,并且根据假设列表来简化集合的表达形式.为了验证思路清晰,利用SUBGOAL_THEN‘…’ASSUME_TAC建立了4个子目标,并且验证完毕后将目标放入假设列表中.子目标的证明需要集合有限定理FINITE_SUBSET,FINITE_CART_SUBSET_LEMMA等以及处理点对的定理,策略会用到将等式自动对应分开的BINOP_TAC和处理存在量词的EXISTS_TAC等.外积除了上述基本线性性质外,还有独特的线性相关性和反对称性:

· ∀i,mbasis{i} outer mbasis{i}=vec 0.

· ∀i j,mbasis{i} outer mbasis{j}=--(mbasis{j} outer mbasis{i}).

3.5 运算性质的形式化证明

本节对几何代数中常用的其他基本运算几何反、几何逆、对偶和多重矢量求模进行形式化.关于这些运算的理论知识见文献^[21].

3.5.1 几何反

几何反类似于序列逆排序来调整运算位序,用A^†表示.若A_k=v₁,v₂,…,v_k且v₁,v₂,…,v_k为支撑A所在的子空间,则$A_k = {v_k}...{v_2}{v_1}$.任意k阶blade A的几何反记作:

$A_k = {( - 1)^{{{k(k - 1)} \over 2}}}{A_k}$

(10)

其中,k(k-1)/2指的是调整顺序的次数,每交换一次顺序即产生一个负号.基于上述定义,对几何反的定义进行形式化.

定义6. 几何反:

∀x,reversion x=lambdas s.--(&1) pow ((CARD(s)*(CARD(s)-1)) DIV 2)*x$$s.

由于几何反具有加法交换不变性与几何积反对称性,所以多重矢量x的几何反求解过程是利用公式(10)依次求出不同阶数子空间的几何反,然后再累加在一起,这个相加在形式化中可以用lambdas函数表示.

3.5.2 几何逆

在3种基本运算中,只有几何积是可逆的.几何逆是几何积的逆运算,用A^-1表示.但并不是任意的多重矢量均可逆,若多重矢量x可逆,则存在一个多重矢量x',满足x与x',x'与x的几何积均为标量1.

定义7. 多重矢量可逆:

∀x,invertible_mult x=$$x'.(x*x'=mbasis{})∧(x'*x=mbasis{}).

几何逆主要是针对可逆的k阶片积求逆,其计算公式为

$A_k^{ - 1} = {{A_k } \over {A_k {A_k}}}$

(11)

注意,并不是所有的片积都可逆.k阶片积几何逆的运算公式(11)需要用到几何除.

定义8. 几何积的除:

∀x y,x/y=@z.x=y*z.

上述定义中,@表示存在且满足条件的元素.定义8表示:存在一个多重矢量z,满足y和z的几何积等于x,那么z等于x与y的几何除.在定义6~定义8的基础上,按照公式(11)对几何逆形式化.

定义9. 几何逆:

∀k p,multiv_inv(blade k p)=

if invertible_mult(blade k p) then reversion(blade k p)/(reversion(blade k p)*(blade k p)) else vec 0.

3.5.3 伪标量和对偶

任意多重向量A的对偶量记做A,可表示为A与伪标量的几何积(或内积):

A=AI-1

(12)

其中,I为单位伪标量.对偶可以理解为片积在伪标量内的补集,其几何含义为广义的法子空间.例如,三维空间中,二重矢量的对偶是它所表示的平面的法向量.由于对偶表达式中需要单位伪标量的几何逆,故需要定义伪标量并且证明它是最高阶的可逆片积:

定义10. 伪标量:

pseudo=mbasis(1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))).

因为伪标量指的是单位伪标量,所以需要构造一个特殊的单位多重矢量:

multiv_unit=vsum{s|s SUBSET 1..(dimindex(:p)+dimindex(:q)+dimindex(:ρ))}(ls.mbasiss).

定理12. 伪标量是最高阶片积:

pseudo=blade(dimindex(:p)+dimindex(:q)+dimindex(:ρ))multiv_unit.

定理13. 伪标量可逆:

invertible_mult(pseudo).

基于上述定义和定理的支持,再根据式(12)将对偶运算进行形式化.

定义11. 对偶算子:

∀x,DUAL x=x*(multiv_inv(pseudo)).

3.5.4 多重矢量求模

多重矢量求模类似于复数的模,记作:

$||A|| = \langle {A }A\rangle _0^{{\raise0.5ex\hbox{$\scriptstyle 1$} \kern-0.1em/\kern-0.15em \lower0.25ex\hbox{$\scriptstyle 2$}}}$

(13)

定义12. 多重矢量的模:

∀x,mult_norm x=sqrt((blade 0(reversion x*x))$${}).

该定义调用了定义1来表示reversion x*x的0阶片积,$${}表示取0阶子空间即标量的大小.

4 几何代数变换算子

几何代数基本运算难以满足复杂几何和拓扑关系分析的需要,因此还需几何变换的投影、反射、求交以及旋转等算子的支撑,几何代数中运用几何积运算使几何变换表达简单化.表3对几何代数变换算子进行形式化定义.关于几何代数运算与算子的详细定义和推导过程见文献^[22].其中,函数project,reject,reflect为了更加形象化,放在两个片积之间来表示x在y上的投影和反射,所以在定义这些算子前都使用了HOL-Light中缀语句进行声明,例如parse_as_infix(“project”,(24,“right”)),其中,right表示运算的右结合性.

5 刚体运动的建模与验证

几何代数为自然科学中的数学工具提供了统一的框架,它还可以在欧几里得空间、闵可夫斯基空间、仿射空间、射影空间、共形空间等进行扩展^{[23, 24, 25]},实现多种代数和几何系统的统一与表达.其中,几何代数在共形空间中进行扩展形成了共形几何代数CGA,它是几何代数研究中最重要的进展之一,与其相对应的是几何代数空间Cl_4,1,0.它由于完全不依赖于坐标,建立了经典几何统一的和简洁的齐次代数框架,在几何建模与计算方面表现出极大的优势,现已成为国际几何代数研究的主流^{[27, 28]}.本节为了说明几何代数空间Cl_p,q,ρ形式化的有效性和实用性,将p,q,ρ分别设置为4,1,0,表示共形几何代数;然后,利用共形几何代数为数学工具对刚体运动进行形式化建模,并以球体为例给出具体的形式化描述与验证.形式化思路如图2所示,包括3个步骤.

(1) 将三维物理世界中刚体运动问题在五维共形空间中进行理论描述,并在定理证明器HOL-Light中进行形式化建模,主要包括几何体的表示和刚体变换等定义;

(2) 基于建立的刚体运动逻辑模型描述刚体对象,本文选择在五维共形空间中对球的刚体运动进行形式化描述;

(3) 将球经过刚体运动后的表示与物理模型中经过理论演算后的表示在定理证明器中进行等价性验证.

5.1 刚体运动建模

CGA利用三维欧氏空间基向量{e₁,e₂,e₃}的同时,又引入Minkowski平面ρ^1,1中的标准正交基{e₊,e_-},使建模的空间由三维变成五维.利用此正交基还可以构造零矢量(null basis)e₀和e_¥,分别表示无穷远点和基准原点.它们与其自身的几何积为0.

${e_0} = {1 \over 2}({e_ - } - {e_ + }),{e_\infty } = {e_ - } + {e_ + },e_\infty ^2 = e_0^2 = 0$

(14)

利用e_¥,e₀取代e₊,e_-,能够更紧凑地表示共形空间中的点.本文将基矢量e₊,e_-定义为mbasis{4}和mbasis{5},表示Cl_4,1,0中第4个基矢量和第5个基矢量.根据多重矢量的定义知,Cl_4,1,0空间中所有多重矢量HOL类型为real^(4,1,0)multivector.

定义13. 零矢量e₀和e_¥:

null_zero=(&1/&2)%(mbasis{5}-mbasis{4})∧null_inf=(mbasis{5})+(mbasis{4}).

零矢量e_¥,e₀的运算性质在CGA几何体计算中有很重要的作用.本文对零矢量的运算性质做了很多形式化,证明过程中主要用到几何积、外积、内积的线性性质和相对应的基矢量运算定理(定理7~定理10)等.

三维空间中的刚体运动由一系列的旋转和平移组成,CGA中平移、旋转等欧氏变换可统一于同一变换框架,均可用几何积来实现:

otransformed=VoV†

(15)

其中,V是变换算子,主要包括转动算子(rotor)、平移算子(translator)、马达算子(motor);V^†表示V的几何反(定义6).基于CGA方法的刚体运动由马达算子实现:

M=RT

(16)

其中,$R = \cos \left( {{\phi \over 2}} \right) - L\sin \left( {{\phi \over 2}} \right)$是转动算子,L为用单位二重矢量表示的旋转轴,f是旋转角;$T = 1 - {1 \over 2}t{e_\infty }$是平移算子,τ=τ₁e₁+τ₂e₂+τ₃e₃是平移向量,表示平移的方向和长度.对象o的刚体运动被描述为

Origid_body_motion=MoM†

(17)

图3给出了球的刚体运动示意图,表明这种变换表达不仅具有表达统一性还具有结合性,不仅可以实现平移、旋转等单一变换,而且可统一表达由上述单一组合而成的复合变换,并可利用运动表达进行顺序调整.

在几何代数形式化的基础上, 根据上述公式对运动算子进行形式化定义.

定义14. 平移算子:

∀τ,Translation_CGA τ=mbasis{}-(&1/&2)%(multivec τ)*null_inf.

定义15. 旋转算子:

∀τ l,rotation_CGA τ l=cos(τ/&2)%mbasis{}-l*(sin(τ/&2)%mbasis{}.

定义16. 马达算子:

∀a τ l,motor_CGA a l τ=rotation_CGA a l*Translation_CGA τ.

定义17. 几何对象_x的刚体运动:

∀x a τ l,rigid_body_motion x a l τ=(motor_CGA a l τ)*x*(reversion(motor_CGA a l τ)).

定义14中,(τ:real^3)为平移向量.(multivec:real^3→real^(4,1,0)multivector)使用定义4的单映射函数,将平移向量τ构建成对应的多重矢量,使运算类型匹配.定义15中,(rotation_CGA:real→real^(4,1,0)multivector→ real^(4,1,0)multivector)表示旋转算子,其中,(τ:real)表示旋转角,(l:real^(4,1,0)multivector)为旋转轴.定义16中,函数motor_CGA表示马达算子,利用几何积运算(定义5)连接转动算子和平移算子实现.定义17根据公式(17)完成了几何体(x:real^(4,1,0)multivector)的刚体运动模型,函数rigid_body_motion返回的是几何对象x经过刚体变换后的表达式.

5.2 球体运动逻辑模型的验证

基于建立的刚体运动逻辑模型,这里验证一个简单的实例,证明刚体运动逻辑模型的正确性和有效性.假设在三维空间中一个以原点为圆心、半径为$\sqrt 2 $的球s先沿着x轴平移4个单位,再绕着y轴旋转180°,可以得知:理论上.变换后的球心为(-4,0,0),半径不变.已知球心为χ、半径为ρ的球在CGA可以表示为

$S = c + {1 \over 2}({c^2} - {\rho ^2}){e_\infty } + {e_0}$

(18)

其中,χ=χ₁e₁+χ₂e₂+χ₃e₃表示三维欧氏空间中的向量.${c^2} = c_1^2 + c_2^2 + c_3^2$是欧氏空间中的点积,可用欧氏空间向量库

中函数dot描述.根据公式(18)得出:球s在CGA中表示为s=-e_¥+e₀,球s经过变换后为s'=-4e₁+7e_¥+e₀.下面验证利用定义(17),球s经过刚体运动变换后的表达式与s'相等.先对球的表达式进行形式化.

定义18. 球在CGA中的表示:

∀χ ρ,sphere_CGA χ ρ=(multivec χ)+((&1/&2)*(χ dot χ-ρ pow 2))%null_inf+null_zero.

根据球s的运动过程,得到平移向量τ=-4e₁、旋转轴l=e₁₃,旋转角f=p.

那么,基于刚体运动函数rigid_body_motion和球函数sphere_CGA在HOL-Light中的目标可以建为:

rigid_body_motion(sphere_CGA(vector[&0;&0;&0])(sqrt(&2)))(pi)(mbasis{1,3})(vector[&4;&0;&0])=

--&4%mbasis{1}+&7%null_inf+null_zero.

证明过程:首先重写定义13~定义18将目标展开,用VECTOR_3,DOT_VECTOR,VEC_COMPONENT等定理化简vector[&0;&0;&0],再利用定义6、定理1、定理5、定理6和子空间线性运算等处理几何反函数,这是证明的一个难点,所以需要建立子目标单独证明.求出几何反后,再利用表2的几何积线性性质,如加法分配律等,将等式左右展开成基本片积的几何积运算,再重写定理9、定理10,重写后会生成很多条件判断语句if…else,其中,判断语句多为简单的不等式.这里需要使用CONV_TAC(ONCE_DEPTH_CONV NUM_LE_CONV)等策略进行自动判断真假来简化目标形式.另外,证明过程中,最后需要多维向量线性性质如VECTOR_ADD_LDISTRIB,VECTOR_NEG_MINUS1,VECTOR_MUL_RZERO等,也可以使用自动策略VECTOR_ARITH`…`,REAL_RING,ARITH_TAC等处理多维向量和实数中简单计算问题.本目标的得证,证实了基于几何代数变换算子对刚体运动建模的有效性,更加挖掘了基于几何代数形式化方法在解决几何问题上的优势和潜力.

6 总 结

本文基于高阶逻辑定理证明器HOL-Light,以文献^[22]为标准,对几何代数Cl_p,q,ρ空间中基本理论提出了一种正确有效的建模和验证方法,主要包括代数运算和几何计算两方面.本文首先针对几何代数的基本数据结构片积和多重矢量进行理论分析和形式化;然后在总结归纳几何代数基本运算规则的基础上对这些运算进行定义,并且验证它们的运算性质,并通过定义几何代数变换算子完善库的内容、表征代数的几何意义;最后,基于Cl_4,1,0空间对三维欧氏空间中刚体运动进行建模与验证,反映几何代数形式化的正确性和实用性.

在对几何代数的形式化过程中,所有定义和性质推理由于高阶逻辑定理证明器HOL-Light自身的完备性和逻辑严密性,可以确保整个几何代数系统代码的高可靠性;同时,证明过程在很大程度上能够检查定义和定理形式化表达的正确性,例如单位正交基的几何积运算(定理10).我们按照数学理论(即公式(1))抽象成待证明的目标,证明过程中需要重写很多之前形式化过的定义及定理,例如几何积定义(定义5),然后反向推导,直到所有子目标成立,最后完成了整个定理的证明过程.定理10在HOL-Light中的验证通过,反过来就能验证之前几何积形式化定义的正确性.形式化方法由于基于数学逻辑、严格按照数学定义来抽象为形式化逻辑语言,所以可避免数值计算方法中由于反复迭代求和造成的结果不精确等问题.例如:setcode函数中,当集合的势数值较大时,该函数必须严格按照形式化定义,故能返回精确值;抽象积定义中嵌套了两个多维矢量求和函数vsum,假设在维数非常高的几何代数空间中,也能保证多重矢量间基本运算的正确性.形式化方法同时也能相对避免符号计算方法中的短板条件遗漏等问题,例如K阶片积的几何逆定义(定义9),若求任意k阶片积的几何逆,必须先利用可逆定义(定义7)证明它是可逆的才能进行几何逆的求解.本文对几何代数的形式化文本代码约4 000行,这些内容都已整理成为定理库,可以在HOL-Light中加载使用.

本文所形式化的是一个大的数学理论框架,比较抽象,但是通过设置p,q,ρ的数值,可以实现具体代数和几何系统的统一与表达.所以本文代码具有通用性和统一性,对后续研究其他代数学和几何学等具有一定的启发性,例如时空代数空间Cl_1,3,0^[28]等.本文的最大难点是:定理证明技术尽管通过内置启动式推导方法、规则重写和化简等方法可以提高定理证明的自动化程度,但是定理的证明过程仍然需要大量的人机交互,工作量较大,时间耗费较长,要求使用者在具备对几何代数理论熟悉的基础上,具有严密的抽象思维和逻辑推理经验进行形式化建模和验证.目前,由于共形几何代数Cl_4,1,0的强大表示和计算能力受到了国内外的瞩目,下一步工作准备用定理证明方法研究共形几何代数的几何结构及其在机器人运动规划方面的应用.