[isabelle-dev] Smallest contribution ever (trace_mul_sym generalization)

[Stephen Nuchia]

On Wed, Jun 26, 2013 at 3:58 AM, Johannes Hölzl <hoelzl at in.tum.de> wrote:
> I pushed your bundle to the Isabelle repository!

Thank you!

> Are you working on a formalization using the linear algebra in
> Determinants?

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.

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.

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.

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!

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.

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.

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.

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.

-swn
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130626/918e4bf9/attachment-0002.html>