幾何代數的高階邏輯形式化研究

◎李福林 黃利忠

(山西大同大學數學與計算機科學學院，山西 大同 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.