SourceForge.net Logo
project summary

 

Executable Matrix Operations on Matrices of Arbitrary Dimensions

Title: Executable Matrix Operations on Matrices of Arbitrary Dimensions
Author: Christian Sternagel and René Thiemann
Submission date: 2010-06-17
Abstract: We provide the operations of matrix addition, multiplication, transposition, and matrix comparisons as executable functions over ordered semirings. Moreover, it is proven that strongly normalizing (monotone) orders can be lifted to strongly normalizing (monotone) orders over matrices. We further show that the standard semirings over the naturals, integers, and rationals, as well as the arctic semirings satisfy the axioms that are required by our matrix theory. Our formalization is part of the CeTA system which contains several termination techniques. The provided theories have been essential to formalize matrix-interpretations and arctic interpretations.
Change history: [2010-09-17]: Moved theory on arbitrary (ordered) semirings to Abstract Rewriting.
BibTeX:
@article{Matrix-AFP,
  author  = {Christian Sternagel and René Thiemann},
  title   = {Executable Matrix Operations on Matrices of Arbitrary Dimensions},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2010,
  note    = {\url{http://afp.sf.net/entries/Matrix.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: GNU Lesser General Public License (LGPL)
Depends on: Abstract-Rewriting