Title: |
Executable Matrix Operations on Matrices of Arbitrary Dimensions |
Authors:
|
Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and
René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
|
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://isa-afp.org/entries/Matrix.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
GNU Lesser General Public License (LGPL) |
Depends on: |
Abstract-Rewriting |
Used by: |
Matrix_Tensor, Polynomial_Factorization, Polynomials, Transitive-Closure |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|