×

Implementing geometric algebra products with binary trees. (English) Zbl 1311.68147

Summary: 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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
11E88 Quadratic spaces; Clifford algebras
15A66 Clifford algebras, spinors
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Clados Project [online]. URL: http://clados.sourceforge.net/.
[2] GAlgebra: Sympy Geometric Algebra Package [online]. URL: http://docs.sympy.org/latest/modules/galgebra/. · Zbl 1047.03010
[3] Objective Caml [online]. URL: http://caml.inria.fr/ocaml/index.en.html.
[4] Why3, where programs meet provers [online]. Referenced on the Coq web site. URL: http://why3.lri.fr/.
[5] Binary tree—wikipedia, the free encyclopedia [online]. 2013. URL: http://en.wikipedia.org/wiki/Binary_tree [cited11-June-2013].
[6] R. Abłlamowicz and B. Fauser, Clifford/bigebra, a maple package for clifford (co)algebra computations [online]. 2011. URL: http://www.math.tntech.edu/rafal/.
[7] Rafal Abłlamowicz, Joseph Parra, and Pertti Lounesto, editors. Clifford Algebras with Numeric and Symbolic Computation Applications. Birkhäuser Boston, 1996.
[8] G. Aragon-Camarasa, G. Aragon-Gonzalez, J. L. Aragon and M. A. Rodriguez-Andrade, Clifford Algebra with Mathematica. ArXiv e-prints, October 2008. URL: http://arxiv.org/abs/0810.2412. · Zbl 1253.15033
[9] Yves Bertot and Pierre Castéran, Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Springer, 2004. · Zbl 1069.68095
[10] Sylvain Charneau, \’Etude et applications des algébres géométriques pour le calcul de la visibilité globale dans un espace projectif de dimensionn ≥ 2. PhD thesis, University of Poitiers, 2007.
[11] Adam Chlipala, Certified programming with dependent types [online]. 2012. Referenced on the Coq web site. URL: http://adam.chlipala.net/cpdt/. · Zbl 1288.68001
[12] Pablo Colapinto, The Versor home page [online]. URL: http://versor.mat.ucsb.edu/. · Zbl 1298.65032
[13] Robert L. Constable, Stuart F. Allen, Walter R. Cleaveland H.M. Bromley, James F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Implementing Mathematics with the Nuprl. Prentice Hall, 1986.
[14] Coq development team. The Coq Proof Assistant Reference Manual, Version 9.3 [online]. 2011. URL: http://coq.inria.fr.
[15] Thierry Coquand and Christine Paulin, Inductively defined types. Volume 417 of LNCS 1988, pages 50-66. · Zbl 0722.03006
[16] L. Dorst, The inner products of geometric algebra. In Joan Lasenby, Leo Dorst, and Chris Doran, editors, Applications of Geometric Algebra in Computer Science and Engineering, Birkh¨auser, Boston, 2002, pages 35-46. · Zbl 1160.51305
[17] Leo Dorst, Daniel Fontijne, and Stephen Mann, Geometric Algebra for Computer Science: An Object-Oriented Approach to Geometry. (The Morgan Kaufmann Series in Computer Graphics). Morgan Kaufmann Publishers Inc., 2007.
[18] Leo Dorst and Stephen Mann, GABLE: A Matlab Geometric Algebra Tutorial [online]. 2007. URL: http://staff.science.uva.nl/ leo/clifford/gable.html.
[19] Ahmad Hosney Awad Eid, Optimized Automatic Code Generation for Geometric Algebra Based Algorithms with Ray Tracing Application. PhD thesis, Faculty of Engineering, Suez Canal University, Port-Said, Egypt, April 2010.
[20] Daniel Fontijne, Efficient Implementation of Geometric Algebra. PhD thesis, University of Amsterdam, 2007.
[21] Daniel Fontijne, Tim Bouma, and Leo Dorst, Gaigen 2.5: A geometric algebra implementation generator [online]. URL: http://staff.science.uva.nl/ fontijne/g25.html.
[22] Daniel Fontijne and Leo Dorst, GAviewer, interactive visualization software for geometric algebra. [online]. URL: http://www.geometricalgebra.net/downloads.html. · Zbl 1213.68649
[23] Daniel Fontijne and Leo Dorst, Efficient Algorithms for Factorization and Join of Blades. In Eduardo Bayro-Corrochano and Gerik Scheuermann, editors, Geometric Algebra Computing, Springer 2010, pages 457-476. · Zbl 1213.68649
[24] Laurent Fuchs and Laurent Theory, A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry.In Automated Deduction in Geometry, volume 6877 of Lecture Notes in Computer Science (2011) pages 51-67. · Zbl 1350.68233
[25] Georges Gonthier, Formal Proof The Four-Color Theorem. Notices of the AMS, 55 (11), (2008). · Zbl 1195.05026
[26] Michael J. C. Gordon and Thomas F. Melham, Introduction to HOL: a theorem proving environment for higher-order logic. Cambridge University Press, 1993. · Zbl 0779.68007
[27] Per-Erik Hagmark and Pertti Lounesto, Walsh functions, Clifford algebras and Cayley-Dickson process. In J.S.R. Chisholm and A.K. Common, editors, Clifford Algebras and Their Applications in Mathematical Physics, volume 183 of NATO ASI Series, Springer Netherlands, (1986) pages 531-540. · Zbl 0595.15022
[28] John Harrison, HOL light: A tutorial introduction. In FMCAD’96, volume 1166 of LNCS (1996), pages 265-269.
[29] Jacques Helmstetter, Minimal algorithms for Lipschitzian elements. Private communication, June 2012. · Zbl 1307.15031
[30] Dietmar Hildenbrand, Foundations of Geometric Algebra Computing. Volume 8 of Geometry and Computing. Springer, 2013. · Zbl 1268.65038
[31] Dietmar Hildenbrand, Patrick Charrier, Christian Steinmetz, and Joachim Pitt, The Gaalop home page [online]. URL: http://www.gaalop.de/.
[32] Eckhard Hitzer, Geometric calculus international [online]. URL: http://sinai.apphy.u-fukui.ac.jp/gcj/gc_int.html#software. · Zbl 1222.53014
[33] C. Kaliszyk and F. Wiedijk, Certified computer algebra on top of an interactive theorem prover. In M. Kauers, M. Kerber, R. Miner, and W. Windsteiger, editors, Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, volume 4573 of Lecture Notes in Computer Science, Springer, June 27-30, (2007), pages 94-105. · Zbl 1202.68382
[34] Matt Kaufmann, Panagiotis Manolios and J Strother Moore, Computer-Aided Reasoning: An Approach. Advances in FormalMethods. Kluwer Academic Publishers, 2000.
[35] Paul Leopardi, GluCat: Generic library of universal Clifford algebra templates [online]. URL: http://glucat.sourceforge.net/.
[36] Li Hongbo, Wu Yihong: Automated short proof generation for projective geometric theorems with Cayley and bracket algebras: I. Incidence geometry. Journal of Symbolic Computation 36(5), 717-762 (2003) · Zbl 1047.03010
[37] P. Lounesto, Clifford algebras and spinors. London Mathematical Society lecture note series. Cambridge University Press, 1997. · Zbl 0887.15029
[38] Mizar, Journal of Formalized Mathematics. http://mizar.org/JFM/.
[39] Lawrence C. Paulson, Isabelle: a generic theorem prover. Volume 828 of LNCS. Springer-Verlag, 1994. · Zbl 0825.68059
[40] Christian Perwass, CLUCal/CLUViz Interactive Visualization [online]. 2010. URL: http://www.clucalc.info/. · Zbl 1242.20060
[41] Neil L. White, Geometric applications of the Grassmann-Cayley algebra. In Handbook of discrete and computational geometry, Boca Raton, FL, USA, 1997, pages 881-892. CRC Press, Inc. · Zbl 0902.15024
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.