Automatic Generation of Loop-Invariants for Matrix Operations

TL;DR

This paper introduces CL1ck, a symbolic system that automatically generates loop-invariants and algorithms for matrix equations, unifying and discovering algorithms in linear algebra.

Contribution

The paper presents a novel automated system that generates and unifies algorithms for matrix operations, including previously unknown solutions, from a target equation.

Findings

CL1ck successfully generates known and new algorithms for matrix equations.

The system unifies multiple algorithms under common frameworks, such as LU factorization.

Automated generation reduces manual effort and reveals novel algorithmic solutions.

Abstract

In recent years it has been shown that for many linear algebra operations it is possible to create families of algorithms following a very systematic procedure. We do not refer to the fine tuning of a known algorithm, but to a methodology for the actual generation of both algorithms and routines to solve a given target matrix equation. Although systematic, the methodology relies on complex algebraic manipulations and non-obvious pattern matching, making the procedure challenging to be performed by hand, our goal is the development of a fully automated system that from the sole description of a target equation creates multiple algorithms and routines. We present CL1ck, a symbolic system written in Mathematica, that starts with an equation, decomposes it into multiple equations, and returns a set of loop-invariants for the algorithms -- yet to be generated -- that will solve the equation. In a successive step each loop-invariant is then mapped to its corresponding algorithm and routine. For a large class of equations, the methodology generates known algorithms as well as many previously unknown ones. Most interestingly, the methodology unifies algorithms traditionally developed in isolation. As an example, the five well known algorithms for the LU factorization are for the first time unified under a common root.