# Algebraic account of Gaussian elimination?

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....

• I don't know but I bet Pawel Sobocinski does. – Ross Duncan Nov 3 '17 at 17:14
• While I do not know what a giving a categorical account of Gaussian elimination means, your question reminded me of this little essay by Gowers dpmms.cam.ac.uk/~wtg10/meta.doubledual.html. He argues that the arbitrary choice of basis is justified by the fact that there are models of ZF (without choice) in which there exist infinite dimensional vector spaces with a trivial dual. I am sorry if it's not relevant. – Sasho Nikolov Nov 4 '17 at 7:41

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.