Labels

A label is the assignment of a name to a piece of mathematical content. This happens in many ways in mathematics. For instance, we might write a theorem as follows.

Theorem 1. The only idempotent element of a group is the identity.

Or we might write an equation with a number to its right, as in $$ \vec{f}(t)=(1-t)^3C_1+3t(1-t)^2C_2+3t^2(1-t)C_3+t^3C_4. \hspace{1in} (1) $$ In the first case, Theorem 1 is the label and the text that follows it is the statement being labeled. In the second case, (1) is the label and the equation to its left is what's being labeled.

Labels are important to steps of work because a step may cite a premise by its label (or one of its labels, if it has many). Note that we will have a separate page to cover Citations, and here we are covering only labels.

Any client is welcome to support more types of labels than just those explicitly added by the user. For instance, a client that auto-numbers section headings in a document may label the sections with those numbers automatically, so that a user can refer to them. Or a client that provides a numbered list environment for use in formal proofs may automatically label each line's statement with the line number, so that users can refer to statements by those numbers. But this page does not specify how any particular client should act, so we simply state these options here to let the reader know that clients are welcome to be helpful to the user in such a way.

Clients that choose to do so are responsible for keeping citations of such numbers up-to-date when the document changes. For instance, if a user has a proof with lines numbered 1 through 10, then when a new line 2 is inserted, any citation of a line in the range 2 through 10 should be incremented by 1 automatically to preserve user meaning. Such tweaking of the user's work is in the domain of the client, not the LDE, so we say no more about it here.

Labels in the OT

We establish the convention that for any OS $X$, when X.hasLabel is defined, it should be a JavaScript function that takes a string $s$ as an argument and returns true or false indicating if $s$ is a label for $X$.

Because this feature is implemented entirely within the hasLabel() function inside existing OSs, we will not need a subclass of OS to represent labels in the OT. Although labels may be represented in the IT as IMs (as described in the following section), they will not be interpreted to any OSs in the OT.

Labels in the IT

In the IT, we often want to support several different representations for the same OS in the OT. In the case of labels, we have the following ways to represent them in the IT.

We can store in any labeled IE a set of simple data instructing the LDE what kind of strings should be considered a match by the hasLabel() function. We can then add to the IE class a convenience function addLabel() that can be called right before interpret() finishes, to read that stored data and use it to build into the interpretation results an appropriate hasLabel() function. The addLabel() function will take as its parameter the set of results that A.interpret() is about to return, and will adjust them according to the data the client placed into $A$.

Here are some conventions we might adopt to support this scheme, but we are not limited to these.

1. If $A$ has an attribute with key "label regex" and value some string $S$, then A.addLabel(results) will place into each OS in results a hasLabel() function that returns true iff its argument matches the regular expression whose code is in $S$.
2. If $A$ has an attribute with key "label regex flags" and value some object $O$, then the fields of $O$ can be used as a set of flags to modify the behavior of item 1 by specifying whether the regular expression matching procedure ignores case, whitespace, punctuation, etc. The UI might place these flags in the IT for any number of reasons, including document settings, application settings, or even expression settings.
3. If $A$ has an attribute with key "label targets" then we could establish a convention by which its value could indicate which of the elements of results should have a label added and which should not. Like item 2, this modifies how item 1 behaves. This feature is not fully specified here, but given as an example of what we could add in the future if we need it.

Note that any of the data referred to in the above list could also be placed into the IE by an IM. Recall the details of modifiers covered in Modification, including the updateDataIn() routine which lets IMs place attributes in IEs.