Validation

This is the fourth of the four main algorithms discussed on the Algorithms page.

Once Interpretation is complete, the OSs in the OT are ready for the final phase of work shown in the bottom row of the figure on the Design Overview page, validation. In this process, the mathematical and/or logical validity of the steps of work in the user's document are judged, and feedback is provided on that validity. But we do not simply loop through the OT and validate each of its OSs one after the other, because that could be inefficient, for the reasons given below.

What Needs to be Validated?

First, not all types of OSs can be validated. For example, an OS that defines a new rule of logic can't be judged semantically invalid as a step of work. It could have been judged syntactically invalid in the interpretation phase, but in that case it would not have appeared in the OT at all. It might be an unsound rule of logic, which the user can demonstrate by using it to draw conclusions that a human recognizes as false. But the declaration of the rule itself is not an incorrect step of reasoning. In fact, it's not a step of reasoning at all; it's a tool the user is declaring to support zero or more later steps of reasoning.

Second, among those types of OSs that can be validated, not every instance needs to be validated. For example, a user may have a large document with many steps of reasoning. If he or she edits the final line in the document, there is typically no reason to revalidate everything that came before. It may be that only the line that was changed (by the user in the client, which propagated the change to the IT, which then propagated it to the OT) needs to be validated, and the validation of every other step of work in the document is still up-to-date.

Consequently, we would like an efficient way to determine precisely the set of OSs that need to be validated. Thus in every newly constructed OS, we include a "dirty" flag and set it to true, meaning that the OS was recently created (which happens only in the interpretation phase). Consequently, an OS that is re-used from a previous interpretation pass may get placed into the OT already marked clean, while OSs that have been added or replaced during that same interpretation pass will be dirty.

But this does not completely solve the problem, because it is not true that an OS needs validating iff it was just created. We know that the OSs that need validating may be a proper subset of the ones just created, for the reasons given above. But there may also be OSs that did not change during the most recent interpretation pass, and yet still need to be revalidated.

For example, if a rule of logic was edited, then any step of reasoning that cited that rule of logic will need to be updated. Or if a label was edited, then any step of reasoning that referred to that label as a reason or premise (either in its former state or its new state) will need to be updated. The interpretation phase terminates with OSs marked dirty iff they recently changed, but that is not the same as the set of OSs that need to be validated. We must therefore, at the start of the validation phase, compute the set of OSs that need to be validated.

The LDE will maintain a global priority queue $V$ of OSs that need to be validated. Immediately after interpretation completes, the validation phase begins by looping through just those OSs $X$ whose dirty flag is set to true (because $X$ changed during interpretation) and calling X.justChanged(), which should do the job of adding to $V$ anything that must be validated because of the recent changes to $X$.

Each subclass of OS may define X.justChanged() to meet class-specific needs as in the examples above. But the base OS class's implementation of justChanged() will handle the most common needs, including the following.

1. Add $X$ to $V$ iff X.validate is a function.
2. Add any $Y$ in the scope of $X$ to $V$ iff $Y$ cites $X$ in any way. (For this item and the next one, see Citations for details if needed.)
3. Add any $Y$ in the scope of $X$ to $V$ iff, up until the most recent interpretation of the IT, $Y$ had cited $X$ in any way, but now no longer does (perhaps because $X$ had a label added or removed, for example).
4. Whenever any OS is added to $V$, emit a feedback message saying that its validation is being recomputed. Clients who wish to communicate this to the user (for example, by showing the validation result as an ellipsis or other temporary indicator) can make use of such feedback.
5. The default priority assigned to any OS added to $V$ is zero, but the client is free to attach to ISs a validation priority attribute, which interpretation should copy into OSs, and which will be used to override this default. (The default justChanged() respects this convention.)
6. If an IS has its validation priority set to null, this indicates that the client does not want that IS validated right now; its validation is disabled until the user changes that validation priority. Do not enqueue such OSs into $V$. (The default justChanged() respects this convention.)
7. Whenever any OS has its validation skipped because its validation priority is set to null, emit a feedback message stating that such validation is being skipped. Clients should listen for this message and be sure that they are not displaying outdated validation feedback in such cases, but rather that any old feedback has been removed.

Interpretation is free to place a validate function in whatever subset of the OSs in the OT it likes. There are several cases to consider here.

1. Some things, such as rules of inference and variable declarations, require syntactic validation only and will therefore not need a semantic validation routine.
2. Expressions that cite a rule require a simple validation routine only, one that delegates validation to the cited rule, passing the conclusion expression as parameter. (See Rules for more information.)
3. Expressions with no cited reason will be treated in accordance with the document settings.
   1. Some documents may stipulate a default reason that will be attached to all such otherwise-unjustified expressions. (See Validation Features for details about this and related features.)
   2. Some documents may stipulate that no validation should take place in that case. This is what happens in desktop Lurch, and should perhaps be the default here.
   3. Other documents may stipulate that such expressions should receive validation feedback indicating that the user marked the expression as meaningful but did not justify it, and should verify that they actually want Lurch to pay attention to the expression.

Asynchronous Validation

Whenever Modification and Interpretation are neither running nor pending, the LDE is using that time to dequeue OSs from $V$ (respecting their validation priorities) and validate them. This is done by calling the validate() routine in the OS. (The LDE will not permit adding to $V$ any OS that does not have a validate() routine defined.) Validation is complete when $V$ is empty and no validate() routine is still running.

There is no default implementation for validate(), but we do specify the function signature and style. The function is asynchronous and thus accepts as its one parameter a single callback function, which is to be called with no parameters when validation completes. No parameters are needed because any success or failure messages should be dispatched using the global feedback mechanisms of the LDE itself, rather than the callback.

Validation feedback need not be strictly text. For example, if premises were auto-discovered by the validation process, the chosen premises might be included among the validation feedback, so that a UI could (for example) show connections from the conclusion to the auto-discovered premises, enabling the user to verify that their intent was captured.

For extremely fast validate() implementations, it is acceptable to avoid asynchronicity and just do the task and immediately call the callback. But the LDE will also provide tools for making it easy to push computations into a background thread, so that many validation tasks can be run in parallel on architectures with multiple cores.

Those OS subclasses who implement validate() in a background thread should also implement a stopValidation() function that terminates the background thread. This function will be called iff, while a call to validate() is still running in the background, the OS in question was marked dirty for validation again due to the completion of another interpretation pass, which updated the OT and necessitated a new set of calls to justChanged().

Constraints and Consequences

The validation process implemented in X.validate() is permitted to use only certain information: While we permit X.validate() to depend upon the content of any OS $Y\prec X$, we restrict it to content that was originally given at the construction of $Y$. In particular, X.validate() may not depend upon any attributes computed during validation about any OS $Y\neq X$. Validation feedback itself is an attribute of each OS, and is thus a part of what is forbidden by this restriction.

This is a reasonable restriction, because whether or not your first step of reasoning in a proof is correct should typically not impact whether your second step of reasoning is correct. (It might impact whether the second step is useful, but not whether it is correct.) Furthermore, if we permitted errors to cascade through subsequent steps, it would be harder for students to see precisely which points in their work have errors.

Now, whether you have expressed what you expected to express on line 5 of a proof certainly impacts any later line that cites line 5. But what you expressed on line 5 is precisely the results of the interpretation of line 5, and is thus permissible for later lines to use when validating themselves. However, whether or not line 5 follows from lines 1 through 4 does not impact the correctness of lines after line 5.

Consider, for example, a subproof that begins with "Let $x\in\mathbb{R}$ be arbitrary" and proceeds to do several correct steps of inference based on that declaration. But somewhere earlier in the proof, you have already assumed that $x$ is an even integer. The step "Let $x\in\mathbb{R}$ be arbitrary" should be marked incorrect, but the remainder of the subproof should not. If the user realizes their error and changes the declaration to "Let $y\in\mathbb{R}$ be arbitrary," and all free $x$s in the subproof into $y$s, then the declaration could become correct (if $y$ was not declared), but some later lines in the subproof may then become incorrect (if they relied on $x$'s being an even integer). This is exactly how it ought to be graded.

A significant and beneficial consequence of these restrictions is that the order in which OSs are removed from $V$ and validated is irrelevant. This is because X.validate() cannot depend on the output of Y.validate() for $Y\neq X$, and thus which of the two gets run first does not matter.

Because validation order is independent and Interpretation is a separate phase from validation, we gain another beneficial consequence: Once Interpretation is complete, before validation even begins, the content of a document is in a form that can be used by that document's dependencies. So if a user loads, types, creates, or edits a document, then saves it while validation is still only partially complete, he or she can still import that document into other documents as a dependency, because Interpretation is sufficient to provide all the semantics relevant for exporting to dependencies.