## Archive for the ‘Uncategorized’ Category

### Installing Isabelle

September 17, 2012

I am recovering from a hardware failure that resulted in the loss of my encrypted home partition, so I had to install Isabelle. Here are quick notes on what is needed on Ubuntu 12.04.

1. Download Isabelle. The installation is just unpacking to the directory of your choice, I unpacked it to ~/bin. That created a directory ~/bin/Isabelle2012.

2. Edit ~/bin/Isabelle2012/etc/settings file to change the default logic to ISABELLE_LOGIC=ZF.

3. Run “build ZF” in the ~/bin/Isabelle2012 directory. This builds the ZF heap image. Isabelle ships with only HOL image precompiled.

4. Install openjdk-6-jre, texlive-latex-base and texlive-latex-extra packages. It’s the first time I am using openjdk instead of Sun Java, but so far I haven’t noticed any issues. The texlive-latex-extra package is for comment.sty file that is needed for LaTeX processing of proof documents.

5. Start Isabelle jEdit interface with  ~/bin/Isabelle2012/bin/isabelle jedit and correct the font size in Utilities/Global Options/jEdit/Text Area/Text font. Isabelle ships with the font size 18.

That’s pretty much all that is needed to have Isabelle ready for IsarMathLib contributions.

Update Aug 10th 2012: Turns out installing Java is not necessary as the bundle already contains a suitable JDK.

January 26, 2012

I haven’t updated this blog for a while, so I decided to try to break the writer’s block by posting a couple of quotes from the formalized mathematics stuff I read recently. (more…)

### The Great Bailout

October 3, 2008

I have not seen such disconnect between the information provided by the media and what can be found out from other sources since I was watching TV news in communist Poland more than twenty years ago.

First of all, failures of financial systems happen often enough that by now there are empirical data that allow to evaluate different ways of resolving them. Government buying of bad assets consistently proves to be the one that is the least effective and the most costly to the taxpayers. There is no dichotomy “either bailout of economic disaster”. There are other alternatives that work better and don’t cost that much money from people who didn’t benefit from the profits of investment banks.

As an angry renter (yes, I know who finances that site) I suggest another data point to consider: inflation adjusted house prices since 1890. And for entertainment the roller-coaster version of that.

### MathWiki conference III

January 13, 2008

Aarne Ranta on Formal Mathematics in Informal Language

This talk considers generating readable prezentations of formalized mathematics as a special case of parsing and generating natural language statements. It looks like the idea is to translate at least formal definitions and statements, and perhaps also proofs, into the GF language, then generate natural language(s) reprezentation from that.

The talk is more about computer-supported linguistics than mathematics so I don’t want to pretend I understand what is on the slides. Some interesting comments from the author can be found on his blog.

Cezary Kaliszyk on teaching logic using web interface for COQ

The slides are actually about a bit more than the title says. Cezary’s web interface to provers is the closest thing to the formalized math wiki that exists. It is quite generic and besides COQ it supports (at least) Isabelle back end. It even supports Isabelle/ZF so it already can be used for learning the prover without having to install it. I was not able to verify IsarMathLib theories though as the interface seems to have problems with mixing formal text, informal text and comments.

### MathWiki conference II

January 5, 2008

Christoph Lüth on PGIP

PGIP is a protocol for communication beween a proof assistant front end (editor) and a theorem prover. It seems that in practice at the moment it is used only by Proof General front-end to talk to Isabelle prover. I am using XEmacs based version of Proof General and I am quite satisfied with it. Through some wizard-level hackery the PG developers managed to coerce Emacs to display subscripts and some mathematical symbols, so it is almost WYSIWYG.

One of the slides from the talk is a screenshot of the new generation of Proof General, based on Eclipse. Eclipse is more known as a platform for software development tools rather than document creation tools, so I was afraid it would be a step back as far as formalized mathematics is concerned. But from the slide I can see that there will be some mathematical symbols support. Hopefully all those gadgets around the main editing frame can be turned off and the new PG will be at least as good as the old one.

I am curious what was the rationale for selecting Eclipse for the Proof General basis, instead of for example creating a GNU TeXmacs PGIP plugin. TeXmacs has excellent support for mathematical typesetting and is specially designed to be a front end to other programs, currently mostly Computer Algebra Systems.

Herman Geuvers on Wiki for formalized mathematics

I think this was the most important talk on the conference. Herman Geuvers discussed the plan for getting the EU taxpayers money to finance the development of a formalized mathematics Wiki.

I really want this project to succeed. Writing formalized mathematics is fun, but I imagine doing it in a collaborative Wikipedia-like environment would be much more fun.

In my opinion one of the main obstacles for such Wiki is that most theorem provers don’t support generating readable presentations of formalized text.

“Readable” means different things to different people. For some people “readable” means “looks like Lisp”. Here by “readable proof” I mean one that uses standard mathematical notation and terminology and anyone with some mathematical education is able to follow it without having to learn a new language with words like “constdefs” and “assms”.
The author seems to realize the problem, but the solution that is suggested in the slides is wrong. The idea for the solution is that the formalized math Wiki would contain lots of nicely typeset informal math content so that it can compete with Wikipedia or MathWorld. Then, as soon as an unsuspecting visitor gets lured to the site she would be flashed with a formal proof that looks like this:

intros k l H; induction H as [|l H].

intros; absurd (S k <= k); auto with arith.

destruct H; auto with arith.

(this is taken from Freek Wiedijk’s slides).

I am not against informal text. In fact, most of the volume of IsarMathLib proof document is informal. Just like a standard math paper needs more than just definitions, theorems and proofs, formalized math text needs some informal text to dilute content, explain motivation, mention other people’s work or simply provide keywords to make searching easier. However, this should not be the main ingredient. The approach that reduces formalized text to an optional comment on the informal content misses the point. If a prover does not feature generating readable presentations, it is simply not suitable for formalized math Wiki.

I certainly hope that I am misunderstanding Geuvers’ vision. My opinion is mostly based on a (mockup?) slide with screenshot of a prototype of such Wiki that is included in the talk, so this is very little information. I really wish this project to be a success.

To be continued …

### MathWiki conference I

January 1, 2008

To my delight I have found that the all presentations from the TYPES topical workshop “Math Wiki” that took place in Edinburg, Oct 31 – Nov 1, 2007 have been posted on the web. This is a lot of interesting reading on formalized mathematics. I will discuss some of my impressions here.

Klaus Grue on LogiWeb

This is a description of LogiWeb – a system for … I don’t really know. My first impression was that it is kind of like Hilbert II – another project building infrastructure for formalized mathematics that asymptotically approaches the difficult part in its lifetime – actually formalizing the math and creating libraries. However after looking at the objectives (fundationally agnostic) and an example proof (very low level with no prover support) I started to think that this is how Metamath would look like if Norman Megill had spent all these years writing software for formalizing math instead of creating formalized math.

As I was reading the presentation trying to understand what LogiWeb is I had more and more problems in putting some bounds on what LogiWeb can do. It has a built-in version control (or rather package management) that allows to maintain consistency of changing interdependent knowledge representations (very good idea). It can output (“render”) files in .html, .xml, .lisp, .exe formats and in fact any other format. It can create “Logiweb machines” that are Turing-complete and support input/output capabilities, interrupt handling, distinction between supervisor and user-mode and non-preemptive scheduling. Logiweb machines can run real-time, safety critical software. As for formalized mathematics, LogiWeb can support Peano Arithmetic as well as mainstream theories like FOL, PA, ZFC, NGB and so on. That’s all great but I have a feeling that Klaus Grue uses the word “can” in a rather metaphoric way. He should really be saying “potentially can” to be more clear.

To me software for doing formalized mathematics becomes interesting when:

1. it supports ZF set theory or something similar (really, now, not potentially),

2. some work has been done on formalizing a bit more than foundations so that I can evaluate how readable the proofs can be made and how easy they are to write.

It looks like LogiWeb is not at this point yet.

Mizar is still the best tool for a mathematician to do formalized mathematics. Online interface? Mizar has had it for a while now.

Too bad Mizar is not free.

Carsten Schürmann on Logosphere

Logosphere is a formal digital library project developed (mostly) by Department of Computer Science of Yale University.

Logosphere’s approach reminds me a bit of Sage – a very succesful mathematical software project which is based on integrating existing tools rather than inventing new ones, as they call it “Building the Car Instead of Reinventing the Wheel”. Similarly Logosphere tries to serve as a common platform for translation between different theorem provers.

Schürmann prezentation contains a very informative picture on different logical frameworks and provers that support them. This brings up the question – which foundation is the best for a community based formalized mathematics wiki project? In other words, which foundation has a best chance to attract a significant number of contributors?

I think there is a big difference beween the view on foundations of mathematics among mathematicians and computer scientists. If someone made a survey at a math department asking faculty a question on what mathematical foundation their work is based on, I am sure most would answer “ZFC”. The majority of the remaining ones would say that they don’t care because it does not play any role in their work or say something generic, like “logic and set theory”, just because they are not even aware there is something else than ZFC. The majority of the remaining ones would declare that they work in category theory or maybe something more exotic like that they are constructivists.

Over at the computing science department the situation would be quite different. ZFC is not good for formal software verification or modeling computation. As a result there is much greater variety of logics and type theories that count as foundations for computer scientiststs. Theorem provers are typically created at computing science departments. No wonder that so few provers (Isabelle and Mizar) support ZFC.

Another reason support for ZFC is rare is that funding for formalized mathematics projects is often obtained by promising something like “the production of mathematically proved programs” (Cornell, NuPrl, grant from the Office of Naval Research). Once your stated goal is formally verified software, ZFC is gone from the picture, together with a chance for a larger participation of people with standard mathematical education .

I am a mathematician by training and I have tried to use Isabelle/HOL. It was weird and I felt like I was writing software rather than mathematics. I could do it, but it was not fun. Isabelle/ZF, on the other hand was easy and natural. That’s why IsarMathLib is a library for Isabelle/ZF, not Isabelle/HOL.

To be continued…

### How to build a library of formalized mathematics

December 29, 2007

Freek Wiedijk has posted the slides from his talk “How to build a library of formalized mathematics” on the MathWiki Workshop in University of Edinburgh that took place in October. The slides present Freek’s view on the main reasons why there is no large scale effort to create a good and comprehensive library of formal mathematics. What I find striking is no mention of Metamath among “interesting” or even “not in the top five” category. I understand that one can not mention every project (although, are there that many that have been active for more than ten years?), but Metamath is the only formalized mathematics project that managed to build community and attract contributors working without any expectation of reward. There are other formalized mathematics projects that people contribute to, but the contributions are either work of graduate students getting their degrees this way or faculty doing research for which they get their salaries. Freek mentions Linux and Wikipedia as succesfull projects based on “benevolent dictatorship”, but not the only formalized mathematics project in this category.

Unfortunately the slides are rather sketchy and only illustrate the main points, so it is hard to guess what was actually said. I would be happy to find out what was discussed under “formalization for communication of mathematics” and “looks do matter”. I think the most important feature needed for attracting contributors is the ability to produce readable presentations that attract readers.

### IsarMathLib and Isabelle/ZF

December 22, 2007

My impression that the new Isabelle 2007 does not break anything related to ZF was a bit premature. It turns out that the interpretation of locales has changed. There is a locale (context) in IsarMathLib called MMIsar0 that is used for Metamath to Isabelle/ZF translation. This locale has twenty five assumptions corresponding to Metamath’s axioms for complex numbers. The MMIsar_valid theorem in Metamath_interface.thy shows that if we take a model of real numbers (i.e. a completely ordered field) and construct the complex numbers from it in the standard way, then all Metamath axioms about complex numbers are satisfied. The problem is that those assumptions in MMIsar0 are interpreted by Isabelle 2007 not as a flat conjunction, but are grouped with parentheses into a complicated structure nested up to four levels deep in some places. It is not a show stopper, but it will take me some time to reflect this nesting structure in the proof.

This is a symptom of a deeper, architectural problem. When verifying a proof written in Isar Isabelle searches for a low-level proof and once it finds one it considers the Isar proof verified, so it discards the low-level proof. This causes problems every time the proof searching algorithm is changed – that is with every new Isabelle release. Some proofs that were successfully verified before don’t check any more. The only solution to this is to design a system so that the low-level proof is not discarded. Once the low-level proof corresponding to high-level source constructs is found, it can serve as the basis of verification and does not need to be generated again. I think while Isar is great for a high-level proof language, something like Metamath would be great as the underlying low-level language.

### Folding in ZF

December 17, 2007

I have finally finished the tool for converting Isabelle verified IsarMathLib source to a blog entry. Writing a parser with Haskell’s Parsec library was a pleasure as usual. The post below was generated from the Fold_ZF.thy theory file that will be included in the next (1.6.2) release of IsarMathLib.

Having a parser opens the possibility of exporting the IsarMathLib source to different formats. I have been thinking what my next target should be and decided it should be TiddlyWiki.

Why TiddlyWiki?

There are two most important features that a good presentation of formalized mathematics should have.

1. Mathematical notation including mathematical symbols.

You can not effectively communicate mathematics without mathematical symbols. Most theorem provers designers seem not to understand this. It is a mystery for me why the designers of programming languages are stuck at the set of symbols that were present on those typewriters that people used to talk to IBM mainframes in the sixties. It obviously wastes the bandwith of human visual cognition channel that can recognize thousands of symbols easily and fast. Fortunately Isabelle is an exception to this – it allows to define any number of custom symbols and specify how they should be typeset in the proof document. As for TiddlyWiki the jsMath plugin allows beautiful display of LaTeX math notation, much better that what you can see in this blog.

2. Ways to deal with excessive verbosity of formalized math

Formalized proofs contain much more details than informal ones. It is good in some way that a machine will not accept proofs written in style “using methods similar to those in [1] modified in a way analogous to [2] we can show that …” . On the other hand having too much detail can make it difficult to see the main idea and the big picture of a proof. Isabelle’s Isar language allows to write structured proofs where the proofs of the main points can be can be separated in the whole proof text so they can be skipped by the reader if the fact is obvious to him/her. TiddlyWiki’s NestedSlidersPlugin would allow to expand such sub-proofs only on demand, so that they don’t obstruct the flow of the main proof.

Another aspect of verbosity of formal proofs is that they typically reference many more other theorems than a typical informal proof. It is sometimes difficult to see which of the referenced theorems are essential to understanding of the proof and which ones are only the glue logic. Isabelle allows to add some theorems to the simplifier where they effectively become the background knowledge that is not necessary to reference directly in proofs. The NestedSlidersPlugin does something even better – it can make the theorem reference clickable, so that the reader can easily examine what the referenced theorem is saying in a window floating over the main text.

And now some formalized mathematics about folding in ZF set theory.

theory Fold_ZF imports InductiveSeq_ZF

begin



Suppose we have a binary operation $P: X\times X \rightarrow X$ written multiplicatively as $P\langle x, y \rangle= x\cdot y$. In informal mathematics we can take a sequence $\{ x_k \}_{k\in 0.. n}$ of elements of $X$ and consider the product $x_0\cdot x_1 \cdot .. \cdot x_n$. To do the same thing in formalized mathematics we have to define precisely what is meant by that “$\cdot .. \cdot$“. The definitition we want to use is based on the notion of sequence defined by induction discussed in InductiveSeq_ZF. We don’t really want to derive the terminology for this from the word “product” as that would tie it conceptually to the multiplicative notation. This would be awkward when we want to reuse the same notions to talk about sums like $x_0 + x_1 + .. + x_n$.
In functional programming there is something called “fold”. Namely for a function $f$, initial point $a$ and list $\left[ b, c, d\right]$ the expression fold(f, a, [b,c,d]) is defined to be f(f(f(a,b),c),d) (in Haskell something like this is called foldl). If we write $f$ in multiplicative notation we get $a\cdot b \cdot c\cdot d$, so this is exactly what we need. The notion of folds in functional programming is actually much more general that what we need here (not that I know anything about that). In this theory file we just make a slight generalization and talk about folding a list with a binary operation $f:X\times Y \rightarrow X$ with $X$ not necessarily the same as $Y$.

Folding in ZF

Suppose we have a binary operation $f : X\times Y \rightarrow X$. Then every $y\in Y$ defines a transformation of $X$ defined by $T_y(x) = f\langle x,y\rangle$. In IsarMathLib such transformation is called as Fix2ndVar(f,y). Using this notion, given a function $f: X\times Y\rightarrow X$ and a sequence $y = \{y_k\}_{k\in N}$ of elements of $X$ we can get a sequence of transformations of $X$. This is defined in Seq2TransSeq below. Then we use that sequence of tranformations to define the sequence of partial folds (called FoldSeq) by means of InductiveSeqVarFN (defined in InductiveSeq_ZF theory) which implements the inductive sequence determined by a starting point and a sequence of transformations. Finally, we define the fold of a sequence as the last element of the sequence of the partial folds.

Definition that specifies how to convert a sequence $a$ of elements of $Y$ into a sequence of transformations of $X$, given a binary operation $f :X\times Y \rightarrow X$.

definition


$Seq2TrSeq(f,a) \equiv \{ \langle k,Fix2ndVar(f,a(k))\rangle .\ k \in domain(a)\}$

Definition of a sequence of partial folds.

definition


$FoldSeq(f,x,a) \equiv$
$InductiveSeqVarFN(x,fstdom(f),Seq2TrSeq(f,a),domain(a))$

Definition of a fold.

definition


$Fold(f,x,a) \equiv Last(FoldSeq(f,x,a))$

If $X$ is a set with a binary operation $f:X\times Y \rightarrow X$ then Seq2TransSeqN(f,a) converts a sequence $a$ of elements of $Y$ into the sequence of corresponding transformations of $X$.


lemma seq2trans_seq_props:
assumes A1: $n \in nat$  and
A2: $f : X\times Y \rightarrow X$  and
A3: $a:n\rightarrow Y$  and A4: $T = Seq2TrSeq(f,a)$
shows $T : n \rightarrow (X\rightarrow X)$  and
$\forall k\in n.\ \forall x\in X.\ (T(k))(x) = f\langle x,a(k)\rangle$
proof -
from $a:n\rightarrow Y$ have D: $domain(a) = n$
using func1_1_L1
with A2 A3 A4 show $T : n \rightarrow (X\rightarrow X)$
using apply_funtype fix_2nd_var_fun ZF_fun_from_total Seq2TrSeq_def
with A4 D have I: $\forall k \in n.\ T(k) = Fix2ndVar(f,a(k))$
using Seq2TrSeq_def ZF_fun_from_tot_val0
{
fix $k$
fix $x$
assume A5: $k\in n$,   $x\in X$
with A1 A3 have $a(k) \in Y$
using apply_funtype
with A2 A5 I have $(T(k))(x) = f\langle x,a(k)\rangle$
using fix_var_val
}
thus $\forall k\in n.\ \forall x\in X.\ (T(k))(x) = f\langle x,a(k)\rangle$
qed



Basic properties of the sequence of partial folds of a sequence $a = \{y_k\}_{k\in \{0,..,n\} }$.


theorem fold_seq_props:
assumes A1: $n \in nat$  and
A2: $f : X\times Y \rightarrow X$  and
A3: $y:n\rightarrow Y$  and A4: $x\in X$  and
A5: $Y\neq 0$  and A6: $F = FoldSeq(f,x,y)$
shows $F: succ(n) \rightarrow X$,   $F(0) = x$  and
$\forall k\in n.\ F(succ(k)) = f\langle F(k), y(k)\rangle$
proof -
let $T = Seq2TrSeq(f,y)$
from A1 A3 have D: $domain(y) = n$
using func1_1_L1
from $f : X\times Y \rightarrow X$ $Y\neq 0$ have I: $fstdom(f) = X$
using fstdomdef
with A1 A2 A3 A4 A6 D show II: $F: succ(n) \rightarrow X$  and $F(0) = x$
using seq2trans_seq_props FoldSeq_def fin_indseq_var_f_props
from A1 A2 A3 A4 A6 I D have $\forall k\in n.\ F(succ(k)) = T(k)(F(k))$
using seq2trans_seq_props FoldSeq_def fin_indseq_var_f_props
moreover    {
fix $k$
assume A5: $k\in n$
hence $k \in succ(n)$
with A1 A2 A3 II A5 have $(T(k))(F(k)) = f\langle F(k),y(k)\rangle$
using apply_funtype seq2trans_seq_props
}
ultimately show $\forall k\in n.\ F(succ(k)) = f\langle F(k), y(k)\rangle$
qed



A consistency condition: if we make the list shorter, then we get a shorter sequence of partial folds with the same values as in the original sequence. This can be proven as a special case of fin_indseq_var_f_restrict but a proof using fold_seq_props and induction turns out to be shorter.


lemma foldseq_restrict:
assumes $n \in nat$,   $k \in succ(n)$  and
$i \in nat$,   $f : X\times Y \rightarrow X$,
$a : n \rightarrow Y$,   $b : i \rightarrow Y$  and
$n \subseteq i$,
$\forall j \in n.\ b(j) = a(j)$,   $x \in X$,   $Y \neq 0$
shows $FoldSeq(f,x,b)(k) = FoldSeq(f,x,a)(k)$
proof -
let $P = FoldSeq(f,x,a)$
let $Q = FoldSeq(f,x,b)$
from assms have $n \in nat$,   $k \in succ(n)$,   $Q(0) = P(0)$  and
$\forall j \in n.\ Q(j) = P(j) \longrightarrow Q(succ(j)) = P(succ(j))$
using fold_seq_props
then show $Q(k) = P(k)$
by (rule fin_nat_ind)
qed



A special case of foldseq_restrict when the longer sequence is created from the shorter one by appending one element.


corollary fold_seq_append:
assumes $n \in nat$,
$f : X\times Y \rightarrow X$,   $a:n \rightarrow Y$  and
$x\in X$,   $k \in succ(n)$,   $y\in Y$
shows $FoldSeq(f,x,Append(a,y))(k) = FoldSeq(f,x,a)(k)$
proof -
let $b = Append(a,y)$
from assms have $b : succ(n) \rightarrow Y$,   $\forall j \in n.\ b(j) = a(j)$
using append_props
with assms show $thesis$
using foldseq_restrict
qed



What we really will be using is the notion of the fold of a sequence, which we define as the last element of (inductively defined) sequence of partial folds. The next theorem lists some properties of the product of the fold operation.


theorem fold_props:
assumes A1: $n \in nat$  and
A2: $f : X\times Y \rightarrow X$,
$a:n \rightarrow Y$,   $x\in X$,   $Y\neq 0$
shows $Fold(f,x,a) = FoldSeq(f,x,a)(n)$  and $Fold(f,x,a) \in X$
proof -
from assms have $FoldSeq(f,x,a) : succ(n) \rightarrow X$
using fold_seq_props
with A1 show $Fold(f,x,a) = FoldSeq(f,x,a)(n)$  and $Fold(f,x,a) \in X$
using last_seq_elem apply_funtype Fold_def
qed



The next theorem tells us what happens to the fold of a sequence when we add one more element to it.


theorem fold_append:
assumes A1: $n \in nat$  and
A2: $f : X\times Y \rightarrow X$  and
A3: $a:n \rightarrow Y$  and
A4: $x\in X$  and A5: $y\in Y$
shows $FoldSeq(f,x,Append(a,y))(n) = Fold(f,x,a)$  and
$Fold(f,x,Append(a,y)) = f\langle Fold(f,x,a), y\rangle$
proof -
let $b = Append(a,y)$
let $P = FoldSeq(f,x,b)$
from A5 have I: $Y \neq 0$
with assms show thesis1: $P(n) = Fold(f,x,a)$
using fold_seq_append fold_props
from assms I have II: $succ(n) \in nat$,
$f : X\times Y \rightarrow X$,   $b : succ(n) \rightarrow Y$,
$x\in X$,   $Y \neq 0$,   $P = FoldSeq(f,x,b)$
using append_props
then have $\forall k \in succ(n).\ P(succ(k)) = f\langle P(k), b(k)\rangle$
by (rule fold_seq_props)
with A3 A5 thesis1 have $P(succ(n)) = f\langle Fold(f,x,a), y\rangle$
using append_props
moreover
from II have $P : succ(succ(n)) \rightarrow X$
by (rule fold_seq_props)
then have $Fold(f,x,b) = P(succ(n))$
using last_seq_elem Fold_def
ultimately show $Fold(f,x,Append(a,y)) = f\langle Fold(f,x,a), y\rangle$
qed

end



The formal part of this blog post has been generated from IsarMathLib’s Fold_ZF.thy theory file, see the relevant pages of the IsarMathLib proof document.

Update Sept. 19 2008: See also the TiddlyWiki rendering of this post.

### Hello world!

September 22, 2007

This blog will be devoted to formalized mathematics.

Formalized mathematics is the craft of writing mathematical proofs in a formal proof language so that they can be verified by a machine.