Interval arithmetic in groups – pass 2

This is a continuation of the Interval arithmetics in groups: Pass 1 post.

Let be a binary operation on a set . We will write this operation additively as . Such operation defines another binary operation on on the powerset (set of subsets) of in a natural way: for .  The nice thing about is that it inherits interesting properties of : if is commutative, then so is , if is a semigroup, then is also a semigroup, if is a monoid, then is also a monoid, if is a group. then … well, never mind, we don’t need that anyway.

This means that all theorems about adding finite (indexed) collections of semigroup elements (and there are quite a couple in the Semigroup_ZF theory) can be reused for the operation on subsets of at little additional cost.

The setup for adding group subsets in the Gyula Lakos’s paper is different in that it assumes the existence of neutral element and defines how to add an infinite number of subsets of .

b.) More generally, suppose is a countable indexed family of subsets of . Assume that for all except for finitely many. Only in that case we define the algebraic sum as except for finitely many .

We can do something in that spirit for as well. Namely suppose that
is a monoid and is a an indexed collection of subsets of such that all but finitely many contain the neutral element (denoted ). We can split the index set  into two subsets, one called consisting of those for which contains the neutral element, and the rest. Then we can define the sum of the family of subsets of as follows:

where is the set of finite nonempty subsets of and are interpreted as the additive notation for . So what we do is we add all sets that do not contain , but for sets that do contain we sum every finite subcollection and take the union of all sums obtained this way.

This nicely generalizes the concept of adding finite collections of sets of semigroups (where the is empty and there is only the first component of the sum above) and (in contrast to the Lakos’ approach) does not require selecting monoid elements from infinite collections of subsets of , i.e. does not require the axiom of choice.

IsarMathLib version 1.6.7 released

This release includes the new HTML rendering tool that replaces tiddlyisar (which still compiles and works ). I updated all IsarMathLib theories that were not fully updated for Isabelle 2008 removing legacy keywords like constdefs and prems and added missing comments. As a result all IsarMathLib theories except those translated from Metamath are now presented at the FormalMath.org site.

There is no new formalized mathematics in this release.

Goodbye ProofGeneral

Some recent messages on the Isabelle mailing list bring the information that the Isabelle team is working on a new interface for Isabelle and possibly other provers that will replace Emacs based ProofGeneral. The new interface will be written in Scala. Scala is an multiparadigm language (OO and functional) that runs on JVM. This is an interesting choice of technology that suggests something about the design goals (I am speculating again). Applications writen in Scala can run on any platform that has JVM. In particular, one can write applets in Scala that can be run in a browser. Scala is a general purpose language, but seems to be particularly good for web programming. There are a couple of web programming frameworks written in Scala, Lift being the most popular, competing with Rails. So the new interface will be multiplatform and easy to integrate with web applications (wiki?). Hopefully this will make Isabelle proving environment closer to being network transparent – a user interface, possibly running in a browser and sending formalized text for verification to an Isabelle server located (possibly) on a different host with dependencies scattered all over the internet.

Formalmath.org

The new HTML rendering of IsarMathLib is ready.

Creating it was easier than I had expected. The most tricky part of the Isar to HTML translator is the Isar parser, but that was done when creating the TiddlyWiki rendering, and didn’t require any changes. Producing HTML from internal representation was just a simple rewrite of the existing TiddlyWiki markup generator. I had to learn some JavaScript and haXe to implement expanding proofs and reference hints, but not much and it was an interesting experience.The CSS layout was created with an online frameset generator with some minor tweaks.

There is one remaining serious issue that I don’t know how to resolve. Some proofs don’t expand on click. One can see an example of this problem in the proof of lemma func1_1_L12 in the func1 theory. The only subproof there does not change cursor and background color on mouse hover (implemented with CSS) and does not expand on click (haXe and JavaScript). Curiously, TiddlyWiki presentation has a very similar problem, see the proof of prod_list_of_lists in the Semigroup_ZF tiddler. This happens in Firefox 3.0.5 on Ubuntu and IE7 and Firefox on Windows XP. If you have an idea what might be causing this, please let me know.

P.S. This turned out to be a jsMath issue.

What next after Tiddly Formal Math?

The Tiddly Formal Math site presents 28 out of 60 IsarMathLib theories. It looks like the approach based on TiddlyWiki is close to the limits of its scalability. The page loads slowly, renders even slower and Firefox asks frequently if I really want this script to run as it appears to be hanging. In addition I noticed recently that some proofs don’t want to expand and I don’t feel up to the task of debugging the NestedSlidersPlugin internals. The TiddlyWiki approach was good as a proof of concept but putting 617 pages of IsarMathLib proof document in one HTML file is clearly not a good idea.

So what next? It seems that the next step is to render IsarMathLib theories directly to HTML, CSS and JavaScript. This will open up lots of interesting possibilities for the presentation, like highliting the assumption or labeled references when the  mouse hovers over a label. The only problem is that (I am a bit ashamed) I know next to nothing about HTML, CSS and JavaScript. Well, I guess that has to change. It seems that haXe is an interesting way to write JavaScript.

IsarMathLib 1.6.6 released

The release adds about 50 facts leading to a theorem named prod_list_of_sets that can be informally stated as follows:

Suppose is a commutative semigroup, is a linearly ordered set, an indexed collection of elements of and a nonempty list of finite, nonempty and mutually disjoint subsets of the index set . Then we have

In words, we can multiply the elements over each index set for and multiply the results, or we can multiply all elements for and the results are the same.

Interval arithmetic in groups: Pass 1

Gyula Lakos’s paper that I plan to formalize for IsarMathLib uses a natural generalization of interval arithmetic to abelian group setting. In this post I will go over section 2.A “Algebraic sums” in this paper, quoting it as needed and tell how I want to formalize the notions defined there.

Vdash, monotone and ikiwiki

A lot of new stuff appeared yesterday on the Vdash home page. There is a very nice collection of links to information about formalized mathematics. The most interesting however is the roadmap page which states that Vdash will be based on ikiwiki wiki compiler and the monotone version control system. This represents a major shift in the concept.

Formal Proof II

Imagine that a programming guru is asked by a person who wants to learn programming how to start. The guru tells the novice that he should get some nice Linux distribution like Gentoo that has all he needs – vi and gcc. He also shows the novice some Linux kernel code to demonstrate the wonderful things someone with knowledge of programming can do. The n00b is immediately enlightened. Or, more likely, runs away in horror.

Formal Proof I

Formal Proof – Theory and Practice, by John Harrison

Among the four articles on formal proofs in the Notices this is the one I enjoyed most.

John Harrison is the creator of HOL Light, one of the systems for doing formalized mathematics. He got hired by Intel in 1998 after the famous Pentium bug to work on formal verification of algorithms used in Intel chips (AMD hired David Russinoff). Harrison was one of the first people in Western Europe working in formal verification who noticed the value of Mizar’s declarative formal proof style and the existence of Mizar itself. He is a living example that formalized mathematics is relevant now and you can even earn living doing it if you a lucky genius.

I found some paragraphs of the “theory” part a bit too basic. I think explaining that

for example as we write “x+y” to denote mathematical object “x plus y“, we can use to denote the proposition “p and q“

is not needed for the readers of Notices of American Mathematical Society. This stuff is taught in some high schools.