<div dir="ltr"><div><div><div><div><div>On Wed, Jun 26, 2013 at 3:58 AM, Johannes Hölzl <span dir="ltr"><<a href="mailto:hoelzl@in.tum.de" target="_blank">hoelzl@in.tum.de</a>></span> wrote:<br>> I pushed your bundle to the Isabelle repository!<br>
<br>
Thank you!<br><br></div>> Are you working on a formalization using the linear algebra in<br>> Determinants<font color="#888888">?</font><span class=""><font color="#888888"><br><br></font></span>I described my project in a recent monologue in the isabelle-users list.  My immediate project is, in brief, verification of the algebraic equivalence of an "optimized" implementation of a computation with the published form of that computation.<br>
<br></div>The published formula, in terms of real-valued matrices and vectors, occupies most of one page under simplifying assumptions (significant cases in applications) and goes on for several more pages in the general case.<br>
<br></div>The probability of a correct transformation of that much math without formal verification is pretty close to zero.  Having tried similar, but smaller, projects in Mathematica and Sage I wanted something with a little more muscle.<br>
<br></div>For this project I am going to need to formalize the well-known heuristics regarding blocked interpretation of matrices and some specific sparseness patterns.  Some of that work will probably be application-specific but perhaps some will be more generally useful -- AFP material maybe.  Just finding what is already there is a project!<br>
<br></div><div>Any equivalence predicated on blocking or sparseness, at least for matrices with countable dimensions, is founded simply on partitioning nested summations so there aren't any deep theorems to be proved there.  It's utility stuff.  The challenge is to develop formalizations that facilitate applications work.<br>
</div><div><br></div><div>I like working in the HOL-Multivariate_Analysis world for several reasons.  My first clue that I was in the right place was the Kerzweil-Henstock integral -- the semester after I had my real analysis course our textbook was upgraded and I had a memorable discussion with Professor Richard Redner about its merits.  Also, the Probability theory in the library seems to be founded on parts of the Multivariate_Analysis session and while I don't need Probability for my immediate task I expect to in the future.  For instance, I'd like to prove convergence properties for an iterative distributed in-place order statistics algorithm.<br>
<br></div><div>I am also going to need some kind of a theory of imperative destructive-assignment program semantics in the long run but the algorithm in my current project is factored in such a way that I can model it as a small set of functions and deal with the iterative elements informally.  I know program semantics is a well-trodden path, I just have to choose among the available formalisms and smash up an environment in which both theory stacks can coexist.<br>
</div><div class="gmail_extra"><br></div><div class="gmail_extra">Finally, I make my living in the commercial software world and I do not generally own the intellectual property I work on.  I will often be less than completely open about the details of my work.  I regret that but it's necessary.<br>
<br></div><div class="gmail_extra">-swn<br></div></div>