# MathLingua

The best way to understand MathLingua is to start with an example. We will create a small collection of a theorem, a couple definitions, and a book. First we will describe the theorem:

Theorem:
.for:G := (X, *, e),a,b,c
where:
.'G is \group'
.'a, b, c \in X'

then:
.if:
.'a*b = a*c'

then:
.'b = c'

.concept:"This result shows that the $\textbf{left cancellation law}$ is true in a group."
.reference:
.source:"@AbstractAlgebraTheoryAndApplications"
page:"47"

This example describes a proven mathematical result that states that the left cancellation property holds in groups.

Read out loud, the result says for any G that is a tuple of (X, *, e) and any a, b, and c where G is a group and a, b, and c are elements of X, then if a*b = a*c then b = c.

Notice that reading the result out loud essentially amounts to reading the result top to bottom and left to right ignoring indentation. The MathLingua code above, and the previous paragraph describing it, might have been both equally easy for you to read and understand.

But for a computer, the indentation and layout in MathLingua code conveys meaning that is easy to understand, while the same meaning in the paragraph above is much more difficult to understand.

This illustrates an explicit goal of MathLingua. It is designed to be just as easy to understand as traditional mathematical literature for a person, but can also be understood by a computer (in particular the MathLingua command line tool mlg or Visual Studio Code extension).

To the MathLingua tooling, MathLingua isn't just text (like it is in LaTeX), but has meaning. And if it can understand MathLingua, it can automate updating your collection of knowledge as you grow it.

Next, notice that our result precisely describes that cancellation can occur in groups but also has a concept section that makes this clear. Thus, if the precise statement is not immediately clear, the concept section allows you to give an easier to understand summary of the result, describe why the result is important, or describe how it is related to other results.

Further, the result has a reference to something called AbstractAlgebraTheoryAndApplications page 47. However, what is this reference$?$

This reference is just another item recorded using MathLingua as:

[AbstractAlgebraTheoryAndApplications]
Resource:
.type:"Book"
.name:"Abstract Algebra Theory and Applications"
.author:"Thomas W. Judson"
.date:"August 15, 2014"
.offset:"10"

.tag:"Abstract Algebra"

We won't go into details about this item. The point at this time is that using MathLingua, you can describe not just mathematical results, but also describe books and other resources that can be read for further information about results.

Now notice that the left cancellation result references the definition of a Group, but what is a Group$?$ The following shows how to encode this definition in MathLingua:

[\group]
Defines:G := (X, *, e)
assuming:
.'X is \set'
.'* is \binary.operation:on{X}'
.'e \in X'

means:
.for:a,b,c
where:
.'a, b, c \in X'

then:
.'(a * b) * c = a * (b * c)'

.for:a
where:
.'a \in X'

then:
.'a * e = e * a = a'

.for:a
where:
.'a \in X'

then:
.exists:b
suchThat:
.'b \in X'
.'a * b = b * a = e'

.written:"\textrm{group}"
.concept:"The integers have a nice property that zero is an integer and any integer $x$ has a negative $-x$ such that $x + -x = 0$, along with the fact that addition is $\textbf{associative}$. A $\textbf{group}$ abstracts this notion of a set and an operation with these nice properties."
.note:"$*$ is said to be $\textbf{associative}$ because $a*(b*c) = (a*b)*c$ for any $a,b,c \in X$."
.reference:
.source:"@AbstractAlgebraTheoryAndApplications"
page:"43"

The definition details the specifics of what a group is as well as a concept and note that provide additional information. Further, the definition uses an indentation style similar to the Theorem: above to convey meaning. Also, note that the command \group is used to specify a group, and a group is a tuple of the form G := (X, *, e).

Next notice that the definition of a group refers to a \binary.operation:on{X} and a \set. In MathLingua, you don't need to define everything that you use, but it is good to do so. The following are those definitions:

[\binary.operation:on{A}]
Defines:*
assuming:
.'A is \set'

means:
."$*?$ is a function that assigns to each pair $(a?, b?) \in A? \times A?$ a unique element $a? *? b? \in A." Metadata: .written:"A?? \times A?? \mapsto A??" .name: ."binary operation" ."law of composition" .reference: .source:"@AbstractAlgebraTheoryAndApplications" page:"42" [\set] Defines:X means: ."A well defined collection of distinct objects." Metadata: .written:"\textrm{set}" Notice that the above definitions use double quotes instead of single quotes. In MathLingua, text in single quotes are statements that refer to definitions. Text in double quotes are instead interpreted as LaTeX. This allows us to provide a textual definition in LaTeX if a structural description is not needed. In particular, the knowledge in our collection can be as precise as we need it with the ability to add precision later. Further notice that the definitions have a written: section. For the \binary.operation:on{A} the written form is A?? \times A?? \mapsto A??. This is used by the MathLingua tooling render MathLingua code similar to how LaTeX code is rendered into math symbols. In particular, what the written form says is that a \binary.operation:on{A} command should be displayed to look the same as how A?? \times A?? \mapsto A?? is rendered in LaTeX. The ?? states that A is a parameter to the \binary.operation:on{A} and that parameter should have parentheses written around it if it is a complex expression. For example the expression \binary.operation:on{X + Y} would be rendered as (X + Y) \times (X + Y) \mapsto (X + Y) At this point, we have a theorem with related definitions, but they are hard to visualize as plain text. The MathLingua tooling has the ability to render MathLingua code. The result for the code above is as follows. Notice the way \binary.operation:on{X} is rendered. Theorem: .for:$G := (X, *, e)$,$a$,$b$,$c$ where: .$G$is$\textrm{group}$ .$a, b, c \in X$ then: .if: .$a * b = a * c$ then: .$b = c$ Metadata: .concept:This result shows that the$\textbf{left cancellation law}$is true in a group. .reference: .source:@AbstractAlgebraTheoryAndApplications page:47 [AbstractAlgebraTheoryAndApplications] Resource: .type:Book .name:Abstract Algebra Theory and Applications .author:Thomas W. Judson .date:August 15, 2014 .url:http://abstract.ups.edu/download/aata-20140815.pdf .offset:10 Metadata: .tag:Abstract Algebra [\group] Defines:$G := (X, *, e)$ assuming: .$X$is$\textrm{set}$ .$*$is$X \times X \mapsto X$ .$e \in X$ means: .for:$a$,$b$,$c$ where: .$a, b, c \in X$ then: .$(a * b) * c = a * (b * c)$ .for:$a$ where: .$a \in X$ then: .$a * e = e * a = a$ .for:$a$ where: .$a \in X$ then: .exists:$b$ suchThat: .$b \in X$ .$a * b = b * a = e$ Metadata: .written:\textrm{group} .concept:The integers have a nice property that zero is an integer and any integer$x$has a negative$-x$such that$x + -x = 0$, along with the fact that addition is$\textbf{associative}$. A$\textbf{group}$abstracts this notion of a set and an operation with these nice properties. .note:$*$is said to be$\textbf{associative}$because$a*(b*c) = (a*b)*c$for any$a,b,c \in X$. .reference: .source:@AbstractAlgebraTheoryAndApplications page:43 [\binary.operation:on{A}] Defines:$*$ assuming: .$A$is$\textrm{set}$ means: .$*$is a function that assigns to each pair$(a, b) \in A \times A$a unique element$a * b \in A.

.written:A \times A \mapsto A
.name:
.binary operation
.law of composition

.reference:
.source:@AbstractAlgebraTheoryAndApplications
page:42

[\set]
Defines:$X$
means:
.A well defined collection of distinct objects.