Applications of the Gauss-Jordan algorithm, done right

Jesús Aransay; Jose Divasón

Home/Archive/arXiv

arXiv · 1401.5910

Applications of the Gauss-Jordan algorithm, done right

Jesús Aransay·Jose Divasón

View original source ↗Read source document ↗Export metadata ↓

Abstract

Computer Algebra systems are widely spread because of some of their remarkable features such as their ease of use and performance. Nonetheless, this focus on performance sometimes leads to unwanted consequences: algorithms and computations are implemented and carried out in a way which is sometimes not transparent to the users, and that can lead to unexpected failures. In this paper we present a formalisation in a proof assistant system of a \emph{naive} version of the Gauss-Jordan algorithm, with explicit proofs of some of its applications, and additionally a process to obtain versions of this algorithm in two different functional languages (SML and Haskell) by means of code generation techniques from the verified algorithm. The obtained programs are then applied to test cases, which, despite the simplicity of the original algorithm, have shown remarkable features in comparison to some Computer Algebra systems, such as Mathematica\textsuperscript{\textregistered} (where some of these computations are even incorrect), or Sage (in comparison to which the generated programs show a compelling performance). The aim of the paper is to show that, with the current technology in Theorem Proving, formalising Linear Algebra procedures is a challenging but rewarding task, which provides programs that can be compared in some aspects to \emph{state of the art} procedures in Computer Algebra systems, and whose correctness is formally proved.

Explore related subjects

cs.LO cs.SC

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Jesús Aransay, Jose Divasón. 2014-01-24. Applications of the Gauss-Jordan algorithm, done right. https://arxiv.org/abs/1401.5910

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory

The verification of liveness conditions is an important aspect of state-based rigorous methods. This article addresses the extension of the logic of Event-B to a powerful logic, in which properties of traces of an Event-B machine can be expressed. However, all formulae of this logic are still interpreted over states of an Event-B machine rather than traces. The logic exploits that for an Event-B machine $M$ a state $S$ determines all traces of $M$ starting in $S$. We identify a fragment called TREBL of this logic, in which all liveness conditions of interest can be expressed, and define a set of sound derivation rules for the fragment. We further show relative completeness of these derivation rules in the sense that for every valid entailment of a formula $φ$ one can find a derivation, provided the machine $M$ is sufficiently refined. The decisive property is that certain variant terms must be definable in the refined machine. We show that such refinements always exist. Throughout the article several examples from the field of security are used to illustrate the theory.

cs.LO↗

arXiv2026

Scenes: A Meta-Logical Algebra for Mutable State

Modelling of mutable state spaces and precisely describing how variables are manipulated in a program is a fundamental problem in compositional verification. Though we can make use of the embedded abstract syntax of a program for such analysis, this runs contrary to the shallow-embedding approach, and hampers efficient proof automation. On the other hand, lenses and prisms provide an elegant algebraic foundation for modelling state, which provide sufficient structure to provide meta-logical program analysis, but without requiring a deep embedding. Nevertheless lenses, as complex algebraic objects, cannot easily be combined, complemented, or collected in sets. In this paper we contribute an accompanying algebraic structure called the scene, which allows us to characterise the set of variables, or coordinates, in a state space. Scenes intuitively correspond to sets of lenses, but like lenses they are purely semantic algebraic objects. We demonstrate that scenes provide us with sufficient structure to characterise the lens-based meta-logical properties, like independence and equivalence. Moreover, we introduce the notion of a scene space, analogous to a vector space, which allows us to recover a set-like algebraic structure. Finally, we show how scenes allow us to characterise the free and bound variables of expressions and programs, without any need for syntax, and demonstrate their use for reasoning about programs by deriving reasoning principles for the parallel composition operator.

cs.LO↗

arXiv2026

Completeness of Kozen's Axiomatization for the Modal mu-Calculus: A Simple Proof

The modal mu-calculus, introduced by Dexter Kozen, is an extension of modal logic with fixpoint operators. Its axiomatization, Koz, was introduced at the same time and is an extension of the minimal modal logic K with the so-called Park fixpoint induction principle. It took more than a decade for the completeness of Koz to be proven, finally achieved by Igor Walukiewicz. However, his proof is fairly involved. In this article, we present an improved proof for the completeness of Koz which, although similar to the original, is simpler and easier to understand. Keywords: The modal mu-calculus, completeness, omega-automata.

cs.LO↗