<p>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 <a href="https://ncatlab.org/nlab/show/dual+vector+space" rel="noreferrer">dual vector spaces</a>.  There it shows that there are a lot of spaces which are isomorphic to their double duals.</p>

<p>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}$].</p>

<p>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 <a href="http://www.cecm.sfu.ca/~mmonagan/MITACS/papers/FFMatFacs08.pdf" rel="noreferrer">Fraction free factors</a> 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. </p>

CC BY-SA 3.0
2017-11-04T14:11:31.660Z
2017-11-04T14:11:31.660Z
Jacques Carette
<p>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.</p>

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

<p>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:</p>

<ol>
<li>The dimension of a dual space $V^\ast$ is the same as the original space $V$.</li>
<li>So the double-dual $V^{\ast\ast}$ has the same dimension as the original space $V$.</li>
<li>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.</li>
</ol>

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

<p>What I'd really like is an <em>algebraic</em> 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).</p>

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

CC BY-SA 3.0
2017-11-03T17:14:27.870Z
I don't know but I bet Pawel Sobocinski does.
Ross Duncan
CC BY-SA 3.0
2017-11-04T07:41:44.187Z
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 https://www.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
<lo.logic><linear-algebra><matrices><ct.category-theory><linear-logic>
Algebraic account of Gaussian elimination?
Neel Krishnaswami
# Algebraic account of Gaussian elimination?

(Asked by: username_0 on 2017-11-03)

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

**Tags:** lo.logic, linear-algebra, matrices, ct.category-theory, linear-logic
> **Comments:**
> **username_1**: I don't know but I bet Pawel Sobocinski does.  
> **username_2**: 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 https://www.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.  

---

## 1 answers

### Answer by username_3 on 2017-11-04. Score: 5

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](https://ncatlab.org/nlab/show/dual+vector+space). 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](http://www.cecm.sfu.ca/~mmonagan/MITACS/papers/FFMatFacs08.pdf) 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.


---

