Citations

A citation is any way that the user might, at one point in his or her input to Lurch, refer back to some other mathematical content already defined or provided. This is common in mathematics. For instance, on the Labels page, we defined Theorem 1 and equation (1), which I can now refer to (or "cite") by those names. The actual mathematical objects are on that other page and the citations of them are in this paragraph. In mathematical documents, we often cite entire sections, as in "Section 3.5."

Because citations typically refer to an earlier piece of mathematical content by name, they are contingent upon the concept of Labels. The LDE also supports citing something without a label, as we will see below. (One can do this in mathematics as well, by saying something like, "the first statement on page 5," but that is less common.)

Citations in the OT

In the OT, if one OS $X$ cites another OS $Y$, then that citation will be stored in $X$ (and optionally also in $Y$). A citation can come in either of two forms.

1. a string $S$ containing the name (or symbol) the user used when creating the citation, stored in an attribute of $X$ that indicates that it is a citation, and which must be tested in A.hasLabel(S) for all OEs $A$ accessible to $X$ to know which of them the string cites, if any
2. a connection (as introduced in the attributes section of the Ordered Trees page) from $X$ to $Y$ whose type indicates that the connection is to be interpreted as a citation of $Y$ by $X$

In both forms, the type of citation may also be included with the citation, so that validation might tell whether the thing being cited is intended to be used as a premise, a rule, a language for parsing, etc., but not all types of validation require this.

We further establish the convention that any OS may implement a getCitations() function, with the intention that its citations have not been precomputed and stored using either of the two forms above, but they can be computed (and then stored) if the getCitations() function is run. Thus during validation, if any validation routine is inspecting an OE $X$ with a getCitations() routine, it should run X.getCitations() before assessing what $X$ cites. This can be used to defer time-consuming premise-finding procedures until validation, rather than trying to have them happen during interpretation.

The downside to the getCitations() function is that it is expensive: A change in some OS $X$ necessitates calling Y.getCitations() in every OS $Y\succ X$. Therefore when interpretation is able to compute a static citation string or connections, as defined above, it should prefer that method over adding a getCitations() function. If interpretation is creating an OS $Y$ whose class provides a default getCitations() function that $Y$ does not need, then that interpretation procedure should set Y.getCitations to null, removing the inefficiency.

Because a single string may satisfy the hasLabel() function for more than one accessible IE, a citation does not always imply a unique cited target. This could be used to permit users to cite something vaguely, which is interpreted as a hint that reduces the search space of the validation procedure. For example, perhaps all of the rules of propositional logic are labeled with the word "logic," so that if a user cites "logic" as the reason, then the validation engine might check all of those rules of logic to see if any one of them can be used to justify the step. (Or it might reject the citation as too vague; this sort of behavior should be adjustable with settings.)

Citations in the IT

Citations in the IT will be similar to Labels, but sort of in the reverse direction.

One way to store citation data in an IE is using a set of JSON objects that at least have string keys and optionally type keys, such as these examples:

    { "string": "Theorem 1", "type": "rule" }

    { "string": "(1)" }

IEs who have such data should copy them over faithfully to corresponding OSs during interpretation.

This method of storing citations in an IE could also be brought about by an IM's placing the data into the IE. Recall the details of Modification, including the updateDataIn() routine which lets IMs place data into IEs.

But a user may construct a step of work $W$ that cites premises $P_1,\ldots,P_n$ and might directly connect $P_1\to W,\ldots,P_n\to W$ in the client, to show that relationship, in clients that support such an interface. The client would then naturally record those connections in the IT, which is a second way to store citation data in the IT. Interpretation should faithfully copy such data into the OT.

This second method of storing citations could not be brought about by an IM's creating it, unless the IM applied to both the source and target of the connection to be created. This is because IMs are allowed to modify attributes only of their targets. To be specific, if we had an IM $M$ and IEs $A$ and $B$ with $M\to A$ but $M\not\to B$, we could not have $M$ create a connection $A\to B$, because that would illegally alter $B$.