Implementing Geometric Algebra Products with Binary Trees

被引：9

作者：

Fuchs, Laurent ^{[1
]}

Thery, Laurent ^{[2
]}

机构：

[1] Univ Poitiers, XLIM SIC UMR CNRS 7252, Poitiers, France

[2] INRIA Sophia Antipolis, Mediterranee, France

来源：

ADVANCES IN APPLIED CLIFFORD ALGEBRAS | 2014年 / 24卷 / 02期

关键词：

Geometric algebra; Grassmann-Cayley algebra; formal proof; binary tree; Coq; CAYLEY;

D O I：

10.1007/s00006-014-0447-3

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

This paper presents a formalization of geometric algebras within the proof assistant Coq. We aim not only at reasoning within a theorem prover about geometric algebras but also at getting a verified implementation. This means that we take special care of providing computable definitions for all the notions that are needed in geometric algebras. In order to be able to prove formally properties of our definitions using induction, the elements of the algebra are recursively represented with binary trees. This leads to an unusual but rather concise presentation of the operations of the algebras. In this paper, we illustrate this by concentrating our presentation on the blade factorization operation in the Grassmann algebra and the different products of Clifford algebra.

引用

页码：589 / 611

页数：23

共 35 条

[21]

Fontijne Daniel, GAIGEN 2 5 GEOMETRIC

[22]

Fuchs L, 2011, LECT NOTES ARTIF INT, V6877, P51, DOI 10.1007/978-3-642-25070-5_3

[23]

Gonthier Georges, 2008, NOTICES AMS, V55

[24]

Gordon M., 1993, Introduction to HOL: a theorem proving environment for higher order logic

[25]

Hagmark Per-Erik, 1986, CLIFFORD ALGEBRAS TH, V183, P531

[26]

Harrison J, 1996, LECT NOTES COMPUT SC, V1166, P265, DOI 10.1007/BFb0031814

[27]

Helmstetter Jacques, 2012, COMMUNICATION

[28]

Hitzer Eckhard, GEOMETRIC CALCULUS I

[29]

Kaliszyk C, 2007, LECT NOTES ARTIF INT, V4573, P94

[30]

Kaufmann Matt, 2000, ADV FORMAL METHODS

← 1 2 3 4 →