几何代数的高阶逻辑形式化研究

◎李福林 黄利忠

(山西大同大学数学与计算机科学学院，山西 大同 037009)

几何代数也被称为Clifford代数，是由Clifford将几何级概念引入至代数中形成的.几何代数融入了Grassmann扩张代数和Hamilton四元数，因此，能够进行高维几何运算与分析.几何代数的出现使几何、数学、物理实现了有机融合，并能够对空间进行更加准确的描述.由此，在最近几年来，几何代数的应用发展领先于其他各学科，并推动了计算机视觉、信息编码以及宇宙论等学科的发展.常用的几何代数方法包括纸笔演算、数值计算、计算代数系统三种方法，不过该三种方法计算结果的准确性却有待提高.对此，高阶逻辑形式化逐步受到理论界的重视.

一、几何代数形式化概述

几何代数空间是位于矢量空间Vp，q，r之上的一个2n维的现象空间，维数n=p+q+r.位于该空间之下的子空间被称为片积(blades).若ei为矢量空间中第i个单位的正交基矢量，那么在几何代数系统Clp，q，r中对其进行相应的表示.p，q，r这三个参数分别表示单位正交基取+1，-1与0时的个数.几何代数形式化中比较著名的模型是由Harison发明的，Harison等通过HOL-Light形式化验证了欧式几何代数Cln的内容，并根据结果构建了Clifford库，包括了欧式空间下的基本矢量、多重矢量、几何代数的核心运算、比较简单的线性性质等内容的定义.

以往运用Harison几何代数不能直接构造非欧几何空间，如球体几何，但可通过设置几何代数系统内Clp，q，r的参数构建非欧几何空间.由此也可以看出，通过几何代数系统Clp，q，r的形式化，一方面，将传统的几何空间扩展到了非欧几何空间，同时，还凸显了其几何意义，扩展了几何代数的工具平台.另外，在Clifford库内，可以将n维欧式空间中的多重矢量以Rn列矩阵的形式进行表示，HOL对其定义real∧(N)multivector，而且这样一来还促使n维多重矢量的定义、定理等与2n个维度空间都具有映射关系.

二、片积与多重矢量形式化

几何空间中最重要的两个元素便是片积与多重矢量.通常情况下，叉积只有在三维空间中才有效，为了打破这种局限性，便将外积·矢量引入到几何代数系统中.如图所示，a，b两个矢量的外积是指空间中有明显方向和边界的平面区域，为了便于记忆，可称为二重矢量(或二元矢量)，记为a∧b，此时将a∧b朝着另一个矢量c的方向延伸，得到的矢量模型便是定向体积元，可称为三重矢量(或三元矢量)，记为a∧b∧c.

由此，可将k个不具有线性关系的多维矢量的外积称为是k阶片积(k-blade)，即

Ak=a1∧a2∧a3∧…∧ak.

在片积中，无线性关系的向量数目被称作片积阶数，而阶数k可用来表示片积空间维度的数目.而在N维几何代数空间内，片积数则为2N个，分别由0阶片积，1阶片积，…，N阶片积构成，以三维几何代数空间为例，相应的片积组成为{1；e1，e2，e3；e12，e23，e13；e123}(eij=ei∧ej；eijk=ei∧ej∧ek)，在该片积中最高的片积e123则被称为空间的伪标量.

不同阶数的片积经过线性组合后便是N维多重矢量，其最高阶仍为N.阶数通常还用来表示片积的空间维度数，因此，可以将多重矢量理解为以“+”号连接不同维数子空间的一种表达式.由此，若用〈〉i表示维度的提取运算符，那么可以由此得到多重矢量A中维度i的片积，记为

由此也可以发现，对于空间内的基本片积es，其中s必是{1+2+…+(p+q+r)}的子集，如果将片积的下标都采用集合的形式表示，那么便可以通过集合运算对几何代数的子空间进行运算，更加便捷也更加清晰.

三、几何代数的运算分析

在几何代数系统中，常用的运算主要为几何代数空间Clp，q，r中的内积、外积与几何积的运算.多重矢量的组成成分为不同阶数的基本片积，所以以上三个核心运算基本都可以进行加法分配律，在运算过程中可以先将其展开，然后按照基本片积方式进行运算.不过核心运算规则各不相同，对于函数的选择要区分对待，如基本片积可以采用抽象函数op进行操作，而几何代数空间Clp，q，r运算则需要通过构造mult函数.

外积的运算采用的是升维运算，可广泛用于维度扩充等方面.对于两个无线性关系的参数，其外积的结果维数与参与对象之和相等.内积的运算则与此相反，采用的是降维运算.对于内积运算，需要注意的一点是，由于内积和数量积(向量代数中的标准内积)互不相同，所以几何内积的运算对象比较广泛，同维度或不同维度内的对象皆可，所以可以对不同阶数的片积展开运算.

几何积是几何代数中的核心运算，该运算方式将内积与外积相连接，从而可以进行不同维度内的运算.几何积运算是结合代数空间运算的基础.假设任意片积A，阶数为s，片积B，阶数为t，那么其几何积运算形式为

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

对于外积、内积与几何积运算的形式化证明，由于都具有双线性，因此，可以简单地通过线性性质证明，除此之外，常用的验证方式还有几何反等.

四、结 语

本文对于几何代数的高阶逻辑形式化进行了简单分析，介绍了其中的基本概念与运算规则.高阶逻辑形式化验证逻辑严密，扩展了传统的几何代数空间，但由于证明难度较大，对于相关理论，未来还需进一步研究.

[1]马莎，施智平，关永，等.共形几何代数与机器人运动学的形式化[J].小型微型计算机系统，2016(3)：555-561.

[2]马莎，施智平，李黎明，等.几何代数的高阶逻辑形式化[J].软件学报，2016(3)：497-516.

[3]詹乃军，王戟，李宣东.软件形式化方法与应用专题前言[J].软件学报，2016(3)：495-496.