This document is your guide for the MathLingua language, its structure, design, and syntax.
The MathLingua Language is composed of a structural sublanguage, a statement sublanguage, and a text sublanguage. These languages work together to describe mathematical knowledge.
Before diving deeper into the syntax of MathLingua, the interaction between these sublanguages will be illustrated through the use of an example.
Note that throughout this text MathLingua examples will displayed in a tabbed pane. You can click on the Source and Rendered buttons to switch between the MathLingua source and the associated rendered form.
First we will start with the definition of an integer.
A Defines: is used to define a mathematical entity and specify a signature used to represent that entity. In this case, the \integer signature defines n as one of the numbers $\ldots, -2, -1, 0, 1, 2, \ldots$.
This definition illustrates the use of the text sublanguage. The text sublanguage is used within double quotes. The content between double quotes can be any valid LaTeX (where the amsmath and amssymb package contents are available).
There are more features the text sublanguage provides, but for now, just think of it as a way to specify math knowledge using LaTeX.
Next, to illustrate the statement sublanguage we will describe what it means for an integer to divide another integer.
A Represents: is used to described what a mathematical notation means. Notice unlike an \integer which describes a thing, what it means for integer d to divide an integer n is a concept. Thus a Represents: is used instead of a Defines:.
Next, you will notice the code above has text within single quotes. Such text is part of the statement sublangage. Unlike the text sublanguage which is essentially any valid LaTeX, the statement sublanguage is has a strict syntax. This syntax is inspired by LaTeX but is distinct from it, and is used to describe the meaning of a statement.
Specifically, signatures used in single quotes reference their associated Defines: or Represents:. This association is unique. That is, for any signature, there is at most one Defines: or Represents: associated with it that describes its meaning.
Note there may be no such association yet if the meaning has not yet been defined. This is the case with * above that has not yet been formally defined in a Defines: or Represents:.
Moreover, a Defines: or Represents: specifies how the item it is describing is written, which is used to render the item. For example, from the code above, p \divides q is written as the letter p followed by a vertical line followed by the letter q. Note, that the p is associated with d in the definition and q with n when rendering the p \divides q.
We have actually been using the structural sublanguage this entire time. However, to make it more clear, consider the following definition of a prime number.
The structural sublanguage is the text around the single and double quote items. Specifically the, Defines:means:Metadata:, for:where:then:, and or: are part of the structural sublanguage and form the structure of the mathematical knowledge (a definition in this case).
The structural language uses indentation to align sections of a structure that go together and uses a dot and space to specify arguments to a section that occur on their own line.
The meaning of the definition above can be read from top to bottom following the indentation. That is, it states that a \prime defines a p that satisfies p is an integer, p is greater than one, and for any d, where d divides p then either d equals 1 or d equals n.
Now we can define a theorem that uses the above definitions and representations. Note that the arguments of a section are joined by and. That is the theorem below says for a, b, and p where a and b are integers and p is prime and p divides the product of a and b, then either p divides a or p divides b.
The rest of this document is still a work in progress. Check back regularly for updates.