Expressions

An expression is a mathematical formula, statement, or any of the other common bits of mathematics we have lying about in our documents. The table below provides some examples, but there are many ways to formulate a mathematical system, and in some other systems, perhaps some other set of content would be called mathematical expressions. Thus we do not give a precise definition here, so as to leave it up to the individual system author. These are just some standard mathematical examples.

Mathematical content	Expressions contained therein
Assume $M$ is a magma and $a\in M$.	$M$ is a magma $\hspace{1cm} a\in M$
Let $x$ be such that $x^2>0$.	$x \hspace{1cm} x^2>0$
But $\frac{k}{k+1}<1$ tells us that $k>-1$.	$\frac{k}{k+1}<1 \hspace{1cm} k>-1$
$\vec Q_2=\vec Q_1+\big(\vec P_1(1)-\vec P_1(0)\big)$	$\vec Q_2=\vec Q_1+\big(\vec P_1(1)-\vec P_1(0)\big)$
If you know $P$ and $Q$, you can conclude $P$.	$P$ and $Q\hspace{1cm}P$

Expressions in the OT

In the OT an Output Expression (OE) is a particular subclass of OS that provides an "OpenMath type" field, which will be one of the standard OpenMath data types (OMBind, OMSym, OMVar, etc.). The OE subclass also provides a function that will convert any instance into the form typically used by the openmath-js library, and vice versa, which is important because that alternate form is used by some of the essential packages on which we wish to build the LDE, including packages for parsing and matching.

If there ever arises a case in which the same mathematical expression might have multiple equivalent forms in the OT, then the conversion from OSs to OpenMath should reduce those to a single, canonical form, to work well with the matching package.

Expressions in the IT

In the IT we define two kinds of subclasses of IE that produce OEs. This is not intended to limit us to using only these two kinds of subclasses, but rather to ensure that we support at least these two, and are aware of the distinction.

Definition (corresponding IE). A corresponding IE will have an attribute with key "OpenMath type" whose value will be one of OMBind, OMSym, etc., as listed above. Its interpretation routine yields a single OE node of the same OpenMath type, and recursively converts its children as well.

Thus the client can input any expression this way without the need for grammar definitions or parsing to expand a single IE into an OT subtree.

Definition (shortcut IE). A shortcut IE is an atomic IE whose interpret() routine produces not necessarily atomic OEs.

If a shortcut IE contains a string to be parsed and the name of a grammar to use to do the parsing, then the natural implementation of its interpret() routine is to apply the grammar to the string. This does not necessarily require a grammar to be encoded into the IT or the OT based on user input (although we certainly aim to support doing so). There may be grammars built into the LDE itself; for instance, it would be useful during testing to have access to the standard OpenMath XML encoding, popcorn, and possibly other simple notations. We do not intend to build into the LDE a default mathematical language, because this disincentivizes the completion of a more robust system for customizing notation.

But there are other ways (besides parsing) to expand an atomic IE into a nonatomic OE. For instance, if the LDE were later to include a CAS, then one might ask it to evaluate, compute, or parse an IE on the LDE's behalf, and the result could be converted back into a nonatomic OE. Also see the NumberedList example given at the end of the Clients page.

To be clear, this wiki page does not imply that expressions are the only type of OSs that will be validated. While we expect they will be the most common type of OS that needs to be validated, there are certainly others, and some are higher-level structures. A common example is a theorem-proof pair. That is, a client may provide the user with a way to state a theorem, then follow it with a proof, and indicate that they are connected. That very connection needs to be validated; does the proof actually proceed from the theorem's assumption(s) to its conclusion(s)? If so, then the theorem-proof pair, as a high-level unit, is valid. Otherwise, it is not (and helpful error messages about why should be available to the user).

(Recall from the end of the Validation page that the validation of one expression cannot depend upon the validity of another. So while we might state a theorem and then follow it with an erroneous proof, so that the theorem-proof pair is marked invalid, users can still cite and use the theorem later in other work and have that work marked valid. For example, a student who cannot prove Theorem 6 on the homework can still get credit for proving Theorem 7 correctly, even if that requires citing Theorem 6.)