◎李福林 黃利忠

(山西大同大學(xué)數(shù)學(xué)與計(jì)算機(jī)科學(xué)學(xué)院，山西 大同 037009)

幾何代數(shù)也被稱為Clifford代數(shù)，是由Clifford將幾何級(jí)概念引入至代數(shù)中形成的.幾何代數(shù)融入了Grassmann擴(kuò)張代數(shù)和Hamilton四元數(shù)，因此，能夠進(jìn)行高維幾何運(yùn)算與分析.幾何代數(shù)的出現(xiàn)使幾何、數(shù)學(xué)、物理實(shí)現(xiàn)了有機(jī)融合，并能夠?qū)臻g進(jìn)行更加準(zhǔn)確的描述.由此，在最近幾年來，幾何代數(shù)的應(yīng)用發(fā)展領(lǐng)先于其他各學(xué)科，并推動(dòng)了計(jì)算機(jī)視覺、信息編碼以及宇宙論等學(xué)科的發(fā)展.常用的幾何代數(shù)方法包括紙筆演算、數(shù)值計(jì)算、計(jì)算代數(shù)系統(tǒng)三種方法，不過該三種方法計(jì)算結(jié)果的準(zhǔn)確性卻有待提高.對(duì)此，高階邏輯形式化逐步受到理論界的重視.

一、幾何代數(shù)形式化概述

幾何代數(shù)空間是位于矢量空間Vp，q，r之上的一個(gè)2n維的現(xiàn)象空間，維數(shù)n=p+q+r.位于該空間之下的子空間被稱為片積(blades).若ei為矢量空間中第i個(gè)單位的正交基矢量，那么在幾何代數(shù)系統(tǒng)Clp，q，r中對(duì)其進(jìn)行相應(yīng)的表示.p，q，r這三個(gè)參數(shù)分別表示單位正交基取+1，-1與0時(shí)的個(gè)數(shù).幾何代數(shù)形式化中比較著名的模型是由Harison發(fā)明的，Harison等通過HOL-Light形式化驗(yàn)證了歐式幾何代數(shù)Cln的內(nèi)容，并根據(jù)結(jié)果構(gòu)建了Clifford庫，包括了歐式空間下的基本矢量、多重矢量、幾何代數(shù)的核心運(yùn)算、比較簡(jiǎn)單的線性性質(zhì)等內(nèi)容的定義.

以往運(yùn)用Harison幾何代數(shù)不能直接構(gòu)造非歐幾何空間，如球體幾何，但可通過設(shè)置幾何代數(shù)系統(tǒng)內(nèi)Clp，q，r的參數(shù)構(gòu)建非歐幾何空間.由此也可以看出，通過幾何代數(shù)系統(tǒng)Clp，q，r的形式化，一方面，將傳統(tǒng)的幾何空間擴(kuò)展到了非歐幾何空間，同時(shí)，還凸顯了其幾何意義，擴(kuò)展了幾何代數(shù)的工具平臺(tái).另外，在Clifford庫內(nèi)，可以將n維歐式空間中的多重矢量以Rn列矩陣的形式進(jìn)行表示，HOL對(duì)其定義real∧(N)multivector，而且這樣一來還促使n維多重矢量的定義、定理等與2n個(gè)維度空間都具有映射關(guān)系.

二、片積與多重矢量形式化

幾何空間中最重要的兩個(gè)元素便是片積與多重矢量.通常情況下，叉積只有在三維空間中才有效，為了打破這種局限性，便將外積·矢量引入到幾何代數(shù)系統(tǒng)中.如圖所示，a，b兩個(gè)矢量的外積是指空間中有明顯方向和邊界的平面區(qū)域，為了便于記憶，可稱為二重矢量(或二元矢量)，記為a∧b，此時(shí)將a∧b朝著另一個(gè)矢量c的方向延伸，得到的矢量模型便是定向體積元，可稱為三重矢量(或三元矢量)，記為a∧b∧c.

由此，可將k個(gè)不具有線性關(guān)系的多維矢量的外積稱為是k階片積(k-blade)，即

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

在片積中，無線性關(guān)系的向量數(shù)目被稱作片積階數(shù)，而階數(shù)k可用來表示片積空間維度的數(shù)目.而在N維幾何代數(shù)空間內(nèi)，片積數(shù)則為2N個(gè)，分別由0階片積，1階片積，…，N階片積構(gòu)成，以三維幾何代數(shù)空間為例，相應(yīng)的片積組成為{1；e1，e2，e3；e12，e23，e13；e123}(eij=ei∧ej；eijk=ei∧ej∧ek)，在該片積中最高的片積e123則被稱為空間的偽標(biāo)量.

不同階數(shù)的片積經(jīng)過線性組合后便是N維多重矢量，其最高階仍為N.階數(shù)通常還用來表示片積的空間維度數(shù)，因此，可以將多重矢量理解為以“+”號(hào)連接不同維數(shù)子空間的一種表達(dá)式.由此，若用〈〉i表示維度的提取運(yùn)算符，那么可以由此得到多重矢量A中維度i的片積，記為

由此也可以發(fā)現(xiàn)，對(duì)于空間內(nèi)的基本片積es，其中s必是{1+2+…+(p+q+r)}的子集，如果將片積的下標(biāo)都采用集合的形式表示，那么便可以通過集合運(yùn)算對(duì)幾何代數(shù)的子空間進(jìn)行運(yùn)算，更加便捷也更加清晰.

三、幾何代數(shù)的運(yùn)算分析

在幾何代數(shù)系統(tǒng)中，常用的運(yùn)算主要為幾何代數(shù)空間Clp，q，r中的內(nèi)積、外積與幾何積的運(yùn)算.多重矢量的組成成分為不同階數(shù)的基本片積，所以以上三個(gè)核心運(yùn)算基本都可以進(jìn)行加法分配律，在運(yùn)算過程中可以先將其展開，然后按照基本片積方式進(jìn)行運(yùn)算.不過核心運(yùn)算規(guī)則各不相同，對(duì)于函數(shù)的選擇要區(qū)分對(duì)待，如基本片積可以采用抽象函數(shù)op進(jìn)行操作，而幾何代數(shù)空間Clp，q，r運(yùn)算則需要通過構(gòu)造mult函數(shù).

外積的運(yùn)算采用的是升維運(yùn)算，可廣泛用于維度擴(kuò)充等方面.對(duì)于兩個(gè)無線性關(guān)系的參數(shù)，其外積的結(jié)果維數(shù)與參與對(duì)象之和相等.內(nèi)積的運(yùn)算則與此相反，采用的是降維運(yùn)算.對(duì)于內(nèi)積運(yùn)算，需要注意的一點(diǎn)是，由于內(nèi)積和數(shù)量積(向量代數(shù)中的標(biāo)準(zhǔn)內(nèi)積)互不相同，所以幾何內(nèi)積的運(yùn)算對(duì)象比較廣泛，同維度或不同維度內(nèi)的對(duì)象皆可，所以可以對(duì)不同階數(shù)的片積展開運(yùn)算.

幾何積是幾何代數(shù)中的核心運(yùn)算，該運(yùn)算方式將內(nèi)積與外積相連接，從而可以進(jìn)行不同維度內(nèi)的運(yùn)算.幾何積運(yùn)算是結(jié)合代數(shù)空間運(yùn)算的基礎(chǔ).假設(shè)任意片積A，階數(shù)為s，片積B，階數(shù)為t，那么其幾何積運(yùn)算形式為

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

對(duì)于外積、內(nèi)積與幾何積運(yùn)算的形式化證明，由于都具有雙線性，因此，可以簡(jiǎn)單地通過線性性質(zhì)證明，除此之外，常用的驗(yàn)證方式還有幾何反等.

四、結(jié) 語

本文對(duì)于幾何代數(shù)的高階邏輯形式化進(jìn)行了簡(jiǎn)單分析，介紹了其中的基本概念與運(yùn)算規(guī)則.高階邏輯形式化驗(yàn)證邏輯嚴(yán)密，擴(kuò)展了傳統(tǒng)的幾何代數(shù)空間，但由于證明難度較大，對(duì)于相關(guān)理論，未來還需進(jìn)一步研究.

[1]馬莎，施智平，關(guān)永，等.共形幾何代數(shù)與機(jī)器人運(yùn)動(dòng)學(xué)的形式化[J].小型微型計(jì)算機(jī)系統(tǒng)，2016(3)：555-561.

[2]馬莎，施智平，李黎明，等.幾何代數(shù)的高階邏輯形式化[J].軟件學(xué)報(bào)，2016(3)：497-516.

[3]詹乃軍，王戟，李宣東.軟件形式化方法與應(yīng)用專題前言[J].軟件學(xué)報(bào)，2016(3)：495-496.