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.

BibTeX

@incollection{CSRT-AFP10b,
  author      = "Christian Sternagel and Ren{\'e} Thiemann",
  title       = "{E}xecutable {M}atrix {O}perations on {M}atrices of
                 {A}rbitrary {D}imensions",
  booktitle   = "The Archive of Formal Proofs",
  editor      = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher   = "\url{http://afp.sf.net/entries/Matrix.shtml}",
  year        = 2010,
  month       = Jun,
  note        = "Formal proof development"
  ISSN        = "2150-914x", 
}