Abstract

This document describes a web based system to support development and sharing of algebraic theories. The system should help users to:

Especially, the documents they write should be as readable as possible by themselves, i.e., not clobbered by extensive markup like LaTeX or HTML.1

Introduction

Modern mathematics strongly adheres to rigorous formalisms, especially where algebraic approaches are concerned. This formality should enable the use of computers to support the mathematician in realizing his main aims. Consequently, several kinds of computer systems like automatic provers and computer algebra systems have been developed. The work of any mathematician, however, still mainly consists of the following two tasks:

  1. read the works of others and transfer useful parts into the own approach
  2. develop theories and write documents about them

The aforementioned tools support the scientist in various aspects of developing his theory. There is still a gap, however, where one of the main objects of his work are concerned: the documents describing mathematical theories that have to be read and written.

Consider, for example, the common case that an algebraist wants to integrate pieces of a fellow scientist's work into an own theoretic framework. Not only does he need to give a summary of the notions and theorems he wants to use by copying them symbol by symbol. More often than not this process also involves a painful transcription into the notation used within his own framework. As a result of this process his readers, which are familiar with his notation, may now notice the result of his fellow, eventually for the first time. But if they get so interested that they want to read the original work, they first have to get used to an unfamiliar notation. And what about those readers who were used to the old notation? Will they take the strain to learn the new notation and notice the further development done in the work of our algebraist?

It is conventional to say that syntax does not matter. The reasoning behind this saying is: It is unimportant for the content whether it is presented in this notational system or in that. But what does matter is the familiarity with a notational system. When a person is forced to constantly switch between different systems, syntax matters because it cannot be blinded out as easily as with one familiar system (no matter which of the different systems that is).

Some people would even argue that syntax does matter.2 It is like the "user interface" of a theory (or a programming language). Just like some people think that there can be beauty in a proof, there might also be a beauty inherent to a concrete system of notation. And, in contrast, there is such a thing like inherently ugly and unreadable syntax.3

But moving from syntax to semantics, our algebraist realizes some time later that he would need a slight change in one of his fellow's definitions. But will his fellow's theorems still hold with this change? Often, the answer to such a question is so hard to find that the advantage of finding the usable theory of his fellow is revoked.

We would like to describe the idea for a system which supports scientists like the algebraist of our example in several ways. One of the main ideas is to allow the user to define the notational system he would prefer. All of his formula input is structured with regard to his definitions. This makes it possible that a simple transcription table will transfer his formulas into a different setting, instead of transcribing each definition and each theorem separately. Should the user adhere to a rigorous style of proving, the system could reward him with automatically checking these proofs. This process would support the user well in his aim to eliminate mistakes. In addition, the task of later trying a slight change in a basic definition would also be supported by proof checking. The algebraist of our example could try his change and let the system check whether the theorems he is interested in are still valid.

A System to Share Algebraic Theories

The remainder of these pages contain a description of the basic ideas with regard to the various aspects of the proposed system. Naturally, such a system should not be developed from scratch but build on a host of existing ideas and tools (see the sections on mix-fix operators and on "email"-syntax). After that, although unusual for a scientific project, we will consider some aspects of "marketing" (see the section on convincing people to use the system).

Mix-Fix, Unicode and Precedences

Notational conciseness is the particular strength of algebraic approaches. There are three main ideas to support this strength in the project:

  1. Use the range of unicode characters. Support the user by defining ASCII shortcuts for these characters. Optionally allow the declaration of LaTeX macros. For example, the operator could be inserted whenever the user hits space after typing "\|/" and it may have the associated macro \Downarrow.

  2. Allow the user to define mix-fix operators as flexibly as possible. For example, the system should allow the definition of an operator (_ : _ ⇓ _ : _) with 4 arguments (here denoted by the "_" placeholder signs).

  3. Do not employ a total order of precedences like by numbering. Rather allow the user to define arbitrary precedences on a one-by-one base. For example, the user might specify that the operator _ | _ ← _ binds stronger than (_ : _ ⇓ _ : _) such that the expression (Γ|x ← e : x ⇓ Γ : v ) parses such that Γ|x ← e is the first argument of (_ : _ ⇓ _ : _). The system can then derive a partial order from precedence declarations. Using a total order, or even numbers, however, makes such a system of precedences less modular and the resulting notations cannot be reused as conveniently.

There are several papers on the subject of parsing the expressions resulting from such declarations to build on, e.g., a recent one by Danielsson and Norell.

"Email Syntax"

As noted in the abstract, the documents the users write should be as readable by themselves as possible. With the development of "Wiki" systems and similar web sites, which need to be editable by many people without a steep learning curve, the emphasis on intuitive syntax has become stronger. One of the recent developments in this regard is the Pandoc tool which can convert documents in a very readable style to other formats like LaTeX or HTML. For an example, have a look at the source code of this document and at the HTML document generated from the same source. The only LaTeX ingredients added to generate a PDF version of this document were the \author, \title, \date, \maketitle tags as well as unicode character declarations. Everything else was written in an intuitive and readable syntax which is inspired by the way many people use in their Emails. A syntax in this spirit is what we would like to use for the proposed system as well. Indeed, mathematical formulas might be integrated in Pandoc as special parts of the source code.

Why Should People Use the System?

Just like syntax, marketing matters although people frequently think otherwise (if they think about marketing at all).

In this regard it is not enough to convince people that it would be good for the whole scientific community if only many people would use such a system. It is important that each and every use of the system is rewarding in itself. The additional advantages coming with a growing user community may then work like a catalyser for the intended comprehensive effect. Hence, there are some points to keep in mind:

There is a connection between the last two points. By connecting to existing (and well-proven) tools, for, e.g., PDF generation, theorem proving, versioning, visualization, etc., the system can concentrate on its own strengths. And, additionally, the connection to other tools can also induce new system usage. Just like people begin to use the tool Pandoc to generate a PDF, even when they are not interested to also get an HTML or ODF etc. version, people might begin to use the system as as a frontend to, e.g., a theorem prover, which does not have a comparably nice syntax.

Features Rewarding the Single User

The system should aid the user by supplying means to check his proofs. The purpose of this feature is not to provide a complete theorem prover.4 Rather, the checking procedure should be an optional means to minimize errors in the document. Toward this end it is important to keep this feature simple. A support of substitution with given axioms or theorems and then checking equality could be enough to be worthwhile for the user. For example, proofs in the following style could be easily checked by the system if the according axioms (here "absorption" and "commutativity" from lattice theory) were provided.

  a ⊔ a = a ⊔ ((a ⊔ a) ⊓ a)          absorption
        = (a ⊓ (a ⊔ a)) ⊔ a          commutativity
        = a                           absorption

Especially, the number of times an axiom is applied in a proof step, like "commutativity" above, could be bounded by a fixed number for simplicity.

Along the same line of supporting error elimination, the system should feature a type system. Type inference in this system should be kept to a minimum such that, for instance, the user should provide types for variables. After all, the documents written in the system are mainly meant to be read by other people. And for this purpose it can be considered good style to let a given variable always range over the same set of entities. For a simple example, a,b might range over lattice elements of a lattice L while M,N range over sets. With this the system should accept a ⊔ b and M ∪ N but reject a ⊔ M and a ∪ M (unless L is, e.g., a power set lattice as a concrete assignment for L.

The type system should allow sub sorting like the Maude system but with the possibility to add polymorphism.

Sharing and Collaboration (or Why "Web"?)

When the system has proven to be rewarding enough to attract more users (or the same user frequently), the long term benefit of the system begins to emerge. Whenever a user "publishes" one of his documents, all other users can base their work on it. Sharing one's work with others has several advantages. Having many other people build their theories on one's original document can, e.g., become a measure of quality (and could eventually replace measures like citation index) and can therefore provide valuable feedback. Additionally, having many readers will improve the quality of a document as they will provide feedback if they find an interest in the work. Naturally, users (and to a less extent readers) will prefer to build on documents which are completely proof-checked.

Using the works of colleagues in this way, on the other hand, has the obvious advantage of being able to concentrate on the essential work. The system could support this step by, e.g., providing means to translate between notations as described in the introduction. Also, PDF files generated from a document could contain a section with (preliminaries) which only contain the definitions and theorems which were actually used in the document.

Conclusion

There are many automatic tools to support different aspects of a mathematician's work. Preparing his theories to be processed by such a tool, however, is still a separate step from his main work flow: the reading and writing of mathematical documents. Therefore, using these tools is often seen as an annoying and even superfluous step, which is to be avoided when possible.

In this document we have proposed a system which could close the gap between the different parts of the work flow. We have also argued that from the use of such a system new forms of more efficient work flows and collaboration might emerge. Please feel free to contact me if you find this project proposal interesting or if you know any related tools or projects.


  1. We recommend the PDF version of this document as words in this style represent pointers to, e.g., related work: http://www-ps.informatik.uni-kiel.de/~bbr/WebOfProofs.pdf

  2. Including, e.g., Simon Peyton-Jones in slides 12-15 of this talk or in this interview.

  3. To get an example just look at the longest formula in your latest LaTeX file and compare it to the resulting PDF document.

  4. As noted above, existing theorem provers should be connected to the system with only a small effort whenever the given document contains sufficient specification.