Implementing Geometric Algebra Products with Binary Trees
详细信息 查看全文
- 作者：Laurent Fuchs (1)
Laurent Théry (2) - 关键词：Geometric algebra ; Grassmann ; Cayley algebra ; formal proof ; binary tree ; Coq
- 刊名：Advances in Applied Clifford Algebras
- 出版年：2014
- 出版时间：June 2014
- 年：2014
- 卷：24
- 期：2
- 页码：589-611
- 全文大小：
- 参考文献：1. / Clados Project [online]. URL: http://clados.sourceforge.net/.
2. / GAlgebra: Sympy Geometric Algebra Package [online]. URL: http://docs.sympy.org/latest/modules/galgebra/.
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.
9. Yves Bertot and Pierre Castéran, / Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Springer, 2004.
10. Sylvain Charneau, / \’Etude et applications des algébres géométriques pour le calcul de la visibilité globale dans un espace projectif de dimension / n ≥?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/.
12. Pablo Colapinto, / The Versor home page [online]. URL: http://versor.mat.ucsb.edu/.
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.
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.
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.
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.
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.
25. Georges Gonthier, / Formal Proof The Four-Color Theorem. Notices of the AMS, 55 (11), (2008).
26. Michael J. C. Gordon and Thomas F. Melham, / Introduction to HOL: a theorem proving environment for higher-order logic. Cambridge University Press, 1993.
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.
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.
30. Dietmar Hildenbrand, / Foundations of Geometric Algebra Computing. Volume 8 of Geometry and Computing. Springer, 2013.
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.
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.
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-62 (2003) CrossRef
37. P. Lounesto, / Clifford algebras and spinors. London Mathematical Society lecture note series. Cambridge University Press, 1997.
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.
40. Christian Perwass, / CLUCal/CLUViz Interactive Visualization [online]. 2010. URL: http://www.clucalc.info/.
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. - 作者单位：Laurent Fuchs (1)
Laurent Théry (2)
1. XLIM-SIC UMR CNRS 7252, Poitiers University, France
2. INRIA Sophia Antipolis, Méditerranée, France - ISSN：1661-4909
文摘
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.