Catálogo de publicaciones - libros

In this part of the book we will look at the problem of marking up mathematical knowledge and mathematical documents in general, situate the format, and compare it to other formats like and .

The format is an open markup language for mathematical documents and the knowledge encapsulated in them. The representation in makes the document content unambiguous and their context transparent.

approaches this goal by embedding control codes into mathematical documents that identify the document structure, the meaning of text fragments, and their relation to other mathematical knowledge in a process called . Document markup is a communication form that has existed for many years. Until the computerization of the printing industry, markup was primarily done by a copy editor writing instructions on a manuscript for a typesetter to follow. Over a period of time, a standard set of symbols was developed and used by copy editors to communicate with typesetters on the intended appearance of documents. As computers became widely available, authors began using word processing software to write and edit their documents. Each word processing program had its own method of markup to store and recall documents.

Document markup is the process of adding codes to a document to identify the structure of a document and to specify the format in which its fragments are to appear. We will discuss two conflicting aspects — structure and appearance — in document markup. As the Internet imposes special constraints imposed on markup formats, we will reflect its influence.

In the past few years the XML format has established itself as a general basis for markup languages. As and all mathematical markup schemes discussed here are XML applications (instances of the XML framework), we will go more into the technical details to supply the technical prerequisites for understanding the specification. We will briefly mention XML validation and transformation tools, if the material reviewed in this section is not enough, we refer the reader to [Har01].

Mathematicians make use of various kinds of documents (e.g. e-mails, letters, pre-prints, journal articles, and textbooks) for communicating mathematical knowledge. Such documents employ specialized notational conventions and visual representations to convey the mathematical knowledge reliably and efficiently. The respective representations are supported by pertinent markup systems like TEX/LATEX.

Even though mathematical documents can vary greatly in their level of presentation, formality and rigor, there is a level of deep semantic structure that is common to all forms of mathematics and that must be represented to capture the essence of the knowledge. As John R. Pierce has written in his book on communication theory [Pie80], mathematics and its notations should not be viewed as one and the same thing. Mathematical ideas exist independently of the notations that represent them. However, the relation between meaning and notation is subtle, and part of the power of mathematics to describe and analyze derives from its ability to represent and manipulate ideas in symbolic form. The challenge in putting mathematics on the World Wide Web is to capture both notation and content (that is, meaning) in such a way that documents can utilize the highly-evolved notational forms of written and printed mathematics, and the potential for interconnectivity in electronic media.

In this chapter, we present the state of the art for representing mathematical documents on the web and analyze what is missing to mark up mathematical knowledge. We posit that there are three levels of information in mathematical knowledge: formulae, mathematical statements, and the large-scale theory structure (constructing the context of mathematical knowledge). The first two are immediately visible in marked up mathematics, e.g. textbooks, the third is largely left to an implicit meta-level of mathematical communication, or the organization of mathematical libraries. We will discuss these three levels in the next sections.

Based on the analysis of the structure inherent in mathematical knowledge and existing content markup systems for mathematics we will now briefly introduce basic design assumptions and the development history of the format, situate it, and discuss possible applications.

This part of the book provides an easily approachable description of the format by way of paradigmatic examples of documents. The primer should be used alongside the formal descriptions of the language contained in Part III.

The intended audience for the primer are users who only need a casual exposure to the format, or authors that have a specific text category in mind. The examples presented here also serve as specifications of “best practice”, to give the readers an intuition for how to encode various kinds of mathematical knowledge.

Each chapter of the primer deals with a different category of mathematical document and introduces new features of the format in the context of concrete examples.

In this chapter we will work an example of a stepwise formalization of mathematical knowledge. This is the task of e.g. an editor of a mathematical textbook preparing it for web-based publication. We will use an informal, but rigorous text: a fragment of Bourbaki’s Algebra [Bou74], which we show in Figure 4.1. We will mark it up in four stages, discussing the relevant elements and the design decisions in the format as we go along. Even though the text was actually written prior to the availability of the TEX/LATEX system, we will take a LATEX representation as the starting point of our markup experiment, since this is the prevalent source markup format in mathematics nowadays.

Content Dictionaries are structured documents used by the standard [BCC04] to codify knowledge about mathematical symbols and concepts used in the representation of mathematical formulae. They differ from the mathematical documents discussed in the last chapter in that they are less geared towards introduction of a particular domain, but act as a reference/glossary document for implementing and specifying mathematical software systems. Content Dictionaries are important for the format, since the architecture, and in particular the integration of builds on the equivalence of content dictionaries and theories.

Concretely, we will look at the content dictionary which defines the symbols , , , , , , , , , , , (see [OMC] for the original). We will discuss the transformation of the parts listed below into and see from this process that the content dictionary format is (isomorphic to) a subset of the format. In fact, the 2 standard only presents the content dictionary format used here as one of many encodings and specifies abstract conditions on content dictionaries that the encoding below also meets. Thus is a valid content dictionary encoding.

In Chapter 5 we have seen a simple use of theories in content dictionaries. There, theories have been used to reference symbols and to govern their visibility. In this chapter we will cover an extended example showing the structured definition of multiple mathematical theories, modularizing and re-using parts of specifications and theories. Concretely, we will consider a structured specification of lists of natural numbers. This example has been used as a paradigmatic example for many specification formats ranging from (Common Abstract Specification Language [CoF04]) standard to the theorem prover [ORS92], since it uses most language elements without becoming too unwieldy to present.

In this example, we specify a theory of lists that is generic in the elements (which is assumed to be a totally ordered set, since we want to talk about ordered lists). Then we will instantiate by applying it to the theory of natural numbers to obtain the intended theory of lists of natural numbers. The advantage of this approach is that we can re-use the generic theory to apply it to other element theories like that of “characters” to obtain a theory of lists of characters. In algebraic specification languages, we speak of . Here, the theory has a formal parameter (the theory ) that can be instantiated later with concrete values to get a (in our example the theory ). We call this process theory .

We will now use the technique presented in the last chapter for the elementary algebraic hierarchy. Figure 7.1 gives an overview of the situation. We will build up theories for semigroups, monoids, groups, and rings and a set of theory inclusions from these theories to themselves given by the converse of the operation.

In this chapter we will look at another type of mathematical document: courseware; in this particular case a piece from an introductory course “Fundamentals of Computer Science” (Course 15-211 at Carnegie Mellon University). The documents produced from such courseware can be used as input documents for (see 26.8) and can be produced e.g. by (see Section 26.14).