Algebraic account of Gaussian elimination?

Question

For fun, I've been looking at the interpretation of linear logic in terms of finite-dimensional vector spaces, and ran into an interesting question about the interpretation of double-negation-elimination in this category.

As is well-known, vector spaces have a natural notion of dual space -- given a vector space $V$,(over a field $R$) the dual space $V^\ast$ is just the set of linear functions into $V \multimap R$. Furthemore, it is well-known (indeed, so well-known that I don't know who proved it) that every finite-dimensional vector space is isomorphic to its double-dual.

One direction of the isomorphism $V \to V^{\ast\ast}$ is easy (it's just the map $f : V \to V^{\ast\ast} \triangleq v \mapsto \lambda k.\;k(v)$). The other direction is trickier. The usual proof goes something like this:

1. The dimension of a dual space $V^\ast$ is the same as the original space $V$.
2. So the double-dual $V^{\ast\ast}$ has the same dimension as the original space $V$.
3. So if we can show that $f$ has a zero kernel, then we know that $f$ has a range of all of $V^{\ast\ast}$, and so is (one half of) an isomorphism.

But the only way I know of actually computing the inverse $f^{-1}$ requires choosing a basis and then inverting the matrix.

What I'd really like is an algebraic or categorial account of Gauss-Jordan matrix inversion (or Gaussian elimination or LU decomposition or whatever), so that I can give a syntactic theory of inversion (and hence an operational semantics for double-negation elimination in FD vector spaces).

This seems like the sort of thing that must have been studied before, but my Google skills are apparently not up to the task....

Answer 1

You really should read Gowers' essay carefully - it cleanly details the reasons why you need a basis in general. So if there is going to be an algebraic account of Gauss-Jordan, it will necessarily involve some additional conditions. You can get an idea of the kinds of conditions by reading the n-lab page on dual vector spaces. There it shows that there are a lot of spaces which are isomorphic to their double duals.

As you mention, this is related to double-negation elimination. But let's spell that out. The isomorphism is linear CPS transform, as it is the set of functions $\left(V\multimap R\right)\multimap R$. You are seeking `unCPS'. Which highlights how miraculous the structure of $V$ must be for this to be feasible at all. The page on the n-lab gives some of these miracles. [Turns out that, syntactically, this works for the duality measure $\leftrightarrow$ linear functional on programs if you choose your programming language "just right"; if you're curious, see my work with Chung-chieh Shan at PADL 2016, where we implement $\texttt{unCPS}$].

Another way, more computational, to look at this is to look at more general versions of LU decomposition. For LU with full pivoting, you can decompose $A$ as $PAQ = LDU$ with $P$ and $Q$ as permutation matrices, $D$ diagonal, $L$ unit lower triangular and $U$ unit upper triangular. You can generalize even more to various kinds of rings (see Fraction free factors by Zhou and Jeffrey). The point is that $P$ and $Q$ are arbitrary, but $L,D,U$ depend on them -- another way to see the base dependence. Clever choices of $P$ and $Q$ allow you to deal with whatever defects the expression of $A$ in the original basis were, and 'rotate' things in better position -- be it for stability, sparsity, expression size blowup, etc.