IsarMathLib 1.29.0: Modules and vector spaces

This release adds definitions and basic facts about modules and vector spaces defined as ring (or field) actions on abelian groups. I also edited two theory files contributed earlier by Daniel de la Concepción Sáez (Ring_ZF_2 and Ring_ZF_3) so that they are now included at the isarmathlib.org site.

What are ring actions?

Let be an abelian group. We know that endomorphisms (i.e. homomorphisms ) of such a group form a ring. The additive operation of this ring is the pointwise addition lifted from the group operation and the composition of endomorphisms is the multiplicative operation of the ring. Now take another ring . A ring homomorphism is called a ring action on the group . Turns out when we define scalar multiplication as , for then such action defines a module and vice versa – every module can be thought of as a ring action. So this provides a nice and concise definition of what a module is. If the ring of scalars is actually a field, we get a vector space the same way.

Comparison with Lean

A couple of weeks ago Tim Gowers posted on Twitter (or whatever it is called now) an amusing characterization of bijections as functions that preserve complements. Alex Kontorovich responded with a Lean verification script certifying that characterization. Lawrence Paulson quoted the Lean verification script on his Machine Logic blog, adding the corresponding Isabelle/HOL proof. In this release I have added an Isabelle/ZF proof of this to IsarMathLib as another comparison of the syntax and proving style of various formal proof languages. This adds to the comparison of Isabelle/ZF with Mizar and Metamath that I wrote about before.

Variance swaps in a CAS

A couple of years ago I got a task of writing a module for pricing gamma swaps. I found the task quite difficult, as all I got to base on was an Excel spreadsheet with formulas that were clearly wrong and the few sources on the Internet that I found lacked details. This post (and maybe the next) describes things I learned at that time. Please keep in mind that I am not a quant – just a software guy, so it’s possible I got some of this wrong, maybe all. If you think this is the case please enlighten me in the comments.

One technique for solving problems is to find a practice problem – something easier, but similar enough that going through the exercise gives confidence that the method is sound and serves as a stepping stone to the more difficult one. In case of gamma swaps that simpler problem is pricing of variance swaps.

Variance swaps are financial instruments that are bets about the future observed variance of a price of an underlying asset. The parties that enter the contract observe the price of the underlying at regular intervals , i.e. at times

,

where is the life of the contract. Then they calculate the value and settle the bet based on that value as compared to some predetermined “strike” value set in the contract. When pricing such contract the question is what is the fair value of the strike, i.e. what is the best prediction of it in the future based on what market tells us right now.

To answer this question suppose that the underlying price process is the geometric Brownian motion , where , is the risk-free interest rate and is the standard Brownian motion. Substituting that into the formula for yields

Taking the expectation on both sides we get

(recall that ). Since has the same distribution as and hence for all we get

Now there is something I still don’t understand: in the pricing the first component is ignored – assumed equal to zero. Since typically year maybe indeed the value is small enough to not matter.

Anyway, whatever the rationale for ignoring that term is, as it was easy to guess the fair value of the variance swap strike is closely related to . The value of can be obtained from option prices as implied volatility, but the problem is this way we actually get a different one for each strike. However, there is an interesting identity that provides a reasonable way to obtain a single number estimate for from (interpolated) market option prices. Namely suppose that and are the prices of European call and put options with strike price given by the Black-Scholes formula and . Then the following identity holds:

(I)

This way by interpolating (and extrapolating as needed) the actual market values of and we can get estimates of the integrals and after multiplying by we know what we can expect should be.

The rest of this post is about how to verify the identity above with Maxima Computer Algebra System (CAS).

IsarMathLib 1.28.1: Update to Isabelle2023

Following the Isabelle2023 release I have released an updated version of IsarMathLib. This release does not contain new formalized material, but I have edited two old (from around 2013, with some later additions) theory files contributed by Daniel de la Concepción Sáez so that they can be included in the isarmathlib.org site.

The first theory file is about quotient topologies.

Suppose we have a topology and is a an equivalence relation on . Let be the set of equivalence classes of this relation and be the projection that maps to it’s equivalence class i.e. . Then a natural way to define a topology on is to take . Note that is the strongest topology on in which is continuous.

A slightly more general approach is to start not with an equivalence relation but a surjection , where is any set. Then the collection is a topology on , which might be called the quotient topology in by . Again is the strongest topology on which makes continuous.

These two approaches can be unified by noticing that if we define relation as then is an equivalence relation on and the quotient topology defined by that relation is homeomorphic to the quotient topology in by . So, in a way, all quotient topologies arise from an equivalence relation given by a quotient function.

The second theory added to isarmathlib.org in this release is about group homomorphisms. Results formalized include the fact that endomorphisms of an abelian group form a ring and that any homomorphism between groups and induces an isomorphism between and the image .

IsarMathLib 1.28.0: Binomial theorem

This release adds the binomial theorem to IsarMathLib. Binomial theorem is an elementary result stating that in commutative rings .
The assertion of the theorem as it is presented on the isarmathlib.org site actually reads which probably requires some explanation.
The first question a reader may have is: Why the summation sign does not have limits like in the standard mathematical notation? I guess setting up such notation in Isabelle/ZF would be possible, perhaps with some Standard ML code, but I don’t know how to do that. Instead, the symbol is defined as an operator that expects a list as its argument (see the ring3 locale). A list in IsarMathLib is a function whose domain is an initial segment of the set of natural numbers, like where is a natural number. Functions in ZF set theory are sets of (argument,value) pairs, hence that syntax. Now what does that mean that ? The natural numbers in ZF set theory are defined so that zero is the empty set and for we have . Hence, the notation means that .

IsarMathLib 1.27.0: Spectrum of a quotient ring, Finite State Machines

This release is again mostly based on contributions by Daniel de la Concepción Sáez in algebraic topology (or is it algebraic geometry? I am not sure), automata theory and formal languages.

The content in ring theory provides results on the spectrum of a quotient ring and reaches the result that the spectrum of a quotient ring is homeomorphic to a closed subspace of the spectrum of the original ring (in Zariski topology).

I have to say Daniel’s new theory on Finite State Machines was quite a surprise for me as the subject is quite far away from what I associate with mathematics that is easy to formalize is set theory. The material reaches the proof that non-deterministic finite state automata determine the same languages as deterministic finite state automata.

IsarMathLib 1.26.0: Ring ideals and Zariski topology

This is a relatively large release with new material on algebra and algebraic topology contributed by Daniel de la Concepción Sáez. The full list of topics covered and not covered (yet) is in this GitHub issue. It will take some time before the new theory files are presented on the isarmathlib.org site, in the meantime they can be viewed in the standard Isabelle generated HTML presentation, the outline (definitions and assertions only) or the full proof document with proofs.

What is Zariski topology?

Let be the set of ideals of some commutative ring and be the set of prime ideals (i.e. the spectrum) of that ring. As it turns out the collection is then a topology, called Zariski topology. The carrier of this topology is and the closed sets are of the form for . So this notion belongs to algebraic topology but unlike for the topological groups or rings the topological structure is completely derived from the algebraic structure. Each ring has its Zariski topology.

IsarMathLib 1.25.0: Comparison with Metamath

Around 2007 at the beginning of the project I got an idea to speed up the development of the IsarMathLib library by importing theorems from Metamath’s set.mm. The theorems and proofs translated then are still a part of IsarMathLib and a small sample is presented at the isarmathlib.org site. After translating about 2000 proofs I decided to stop doing that as the work was repetitive and boring and the resulting proofs were not readable.

Metamath is considered a “low level” language and proof assistant, so I recently got curious how the Metamath proofs would compare with similar proofs written in the Isar dialect used in IsarMathLib. In this release I manually translated the Metamath’s utopreg theorem together with a couple of dependencies, taking advantage of Isabelle automation features to the extend I usually do in IsarMathlib. The following table compares verbosity of the original and translated proofs for the theorems whose proofs expressed similar ideas:

Theorem	Steps Metamath	Lines IsarMathLib	Factor
utopreg	95	52	1.8
utopsnneip	15	14	1.1
ustex3sym	25	11	2.3
imasncls	64	28	2.3
utop3cls	103	27	3.8

On average IsarMathLib proofs were about 2.3 times shorter. I have to say I expected that factor to be somewhere between 3 and 4.

The original Metamath utopreg theorem states that all Hausdorff uniform spaces are regular. After I translated the proof I was surprised to notice that the IsarMathLib’s version does not reference the hypothesis that the uniform space is Hausdorff. So, the IsarMathLib version shows that all uniform spaces are regular. I am not sure how it happened. To be honest I was not able to follow the Metamath proof exactly – it’s just too many small steps for me to put in my head at the same time. I was translating the proofs by first showing the steps marked green in Metamath Proof Explorer (I understand this indicates that the theorem referenced in the step is recent and hence close to the one being shown). Then I looked at facts made available this way and tried to figure out how one can get to the thesis of the theorem from them. It is possible that the Metamath proof does not make real use of this hypothesis as well, it’s just easier to spot that in Isar.

IPC with F# and Fable.Remoting

Consider the following programming exercise:
We have a server and some unknown number of clients, possibly on different hosts. The clients send messages to the server, some of them only to say “Hi”. The server responds with a message containing an integer which says how many times the server received the “Hi” message so far. What is the minimal amount of F# code one can write to implement this (i.e. both server and client)?

There are a couple of ways to do IPC (Inter Process Communication) in F# (or C#). One can use named pipes or gRPC, but in this post I want to present Fable.Remoting.

IsarMathLib 1.24.0: Update to Isabelle2022

A new version of Isabelle got released a couple of days ago and this version updates IsarMathLib to Isabelle2022. The Isabelle/ZF logic that IsarMathLib is based on is not actively developed, which has a good side that there are no changes and upgrades like this are easy and problem-free.

There is a little bit of formalized mathematics added in this IsarMathLib release as well. I added a couple of results from general topology that I always considered neat and elegant: a characterization of Hausdorff spaces as those for which the diagonal is closed in the product topology on , the fact that the graph of a function into a Hausdorff space is closed in and that two continuous functions into a Hausdorff space are equal on a closed set.

Another theorem added is related to abstract neighborhood systems. IsarMathLib had had a formalization of the fact that if one has a neighborhood system on one can construct a topology on and vice versa: starting from a topology we can define a natural neighborhood system. In this release I added a theorem asserting that if we start from a neighborhood system, create a topology from it, then create it’s natural neighborhood system, we get back the original neighborhood system.

IsarMathLib 1.23.0: Rewrite of the presentation layer in F#

I wrote the original isar2html tool 13 years ago in Haskell as a way to learn the language. Since then I was extending it and fixing bugs. Coming back once or twice a year to a language that I was not using professionally had quite a bit of overhead just to recall how the things worked and reconstruct the development environment. As it happened I changed jobs in April this year and the new job required F#, so I decided to rewrite isar2html in F#, again as a way to learn the language. Of course as usual with that type of “big rewrite” (well, not that big here really) projects I underestimated the effort needed so I finished only about a week ago. Now I have exactly the same application implemented the same way in Haskell i F#.

	Haskell	F#
lines	2026	1692
words	10334	9239
characters	72006	79320

Basic verbosity statistics

The F# syntax is not as clean as Haskell’s so it was a surprise for me that the number of lines required was about 16% less in F# than in Haskell. Still, I would say that F# is slightly more verbose as the total number of characters was 10% higher in F#. Translating the parser of the subset of the Isar formal proof language that is used in IsarMathLib was almost mechanical and boring thanks to FParsec, which is the F# clone of Haskell’s Parsec parser library. I am especially happy with the result of that part of the project – the parsing errors were difficult to debug in Haskell. FParsec has better diagnostics built in – in case of failure it shows the backtracking information which helps a lot to pinpoint the problem in the text being parsed.

On the mathematics side in this release I have added a theorem stating that an ordered loop valued metric space is T₂.