Clients

We wish to place as few constraints as possible on clients of the LDE, so that the LDE is usable in many contexts. However, we must provide information on the LDE's API, so that clients know how to control the LDE, as well as the types of feedback signals the LDE may generate, so that clients know to listen for them. This page covers those two topics.

LDE API

The LDE exposes the following functions to clients, which they can call to control the IT. Recall that the LDE responds automatically to changes in the IT, processing the IT's content and sending feedback messages about the results of such processing. The LDE initially contains a one-node IT, just an IS node with no children, and the following functions are used to change that initial state.

1. insertChildStructure(parent,child,index) inserts a new child into the IT at the given index of the given parent. We require each newly inserted IS (including each individual node in a subtree) to have an attribute whose key is "id" and whose values are strings that are unique across the IT. (The root that is present in the IT initially will have some standard id, such as "root.")

   parent - must be the id associated with precisely one IS in the IT, which will be the parent of the new node to insert.

   child - must be JSON data that can be deserialized into an IS tree, and when it is deserialized, it must obey the unique id rule given above.

   index - must be a valid integer index into the parent's list of children. That is, if the parent has 3 children, then any index from 0 to 3 is acceptable. Indices 0, 1, and 2 indicate insertion before child 0, 1, or 2, respectively, while index 3 indicates appending on the end of the list of children. Indices below 0 or above 3 are invalid.

   If any of the above requirements on the parameters are not satisfied, the routine does nothing.

2. removeStructure(node) removes an IS from the IT, with all of its descendants. To ensure connection closure of the IT, this routine will first remove all connections involving the structure before it removes the structure itself from the IT.

   node - must be the unique id of an IS already in the IT, but not the root.

   If the parameter requirement is not satisfied, this routine does nothing.

3. replaceStructure(original,replacement) replaces one IS in the IT with a new one.

   original - must be the unique id of an IS in the IT, but not the root.

   replacement - must be JSON data that can be deserialized into an IS tree, and when it is deserialized, it must obey the unique id rule given in the definition of insertChildStructure, above, with the exception that unique ids that appear only in the tree being replaced are acceptable for use in the replacement tree.

   keepConnections - must be a boolean, which defaults to false. To ensure connection closure of the IT, this routine will first remove all connections involving the original structure before it replaces that structure with the new one, unless this parameter is set to true. In that case, all connections in which the original IS participated are transferred from it to the replacement IS.

   If any of the parameter requirements are not satisfied, this routine does nothing.

4. setStructureAttribute(node,key,value) changes one attribute of one IS in the IT.

   node - must be the unique id of one IS in the IT, the node to change.

   key - should be a string that is the attribute key, but if it is not a string it will be converted into one using JavaScripts's String constructor.

   value - should be any JSON data to use as the new attribute value, or the JavaScript value undefined. Using undefined will remove any old key-value pair with the given key from the specified node.

   If the requirement on the first parameter is not satisfied, this routine does nothing. If the requirement on the third parameter is not satisfied, that is, the value is not amenable to JavaScript's JSON.stringify() routine, then it is converted to a plain JavaScript string using the String constructor, and that string used as the value instead.

   As discussed in the attributes section of Ordered Trees, connections among Structures are encoded using attributes. Thus this API function, which gives the client the ability to modify attributes, could inadvertently permit clients to alter the connections among ISs. So we establish the convention that attributes whose keys begin with an underscore (_) are for internal use only, and this API function will prevent clients from using such attribute keys.

5. insertConnection(source,target,data) connects two ISs that are already in the IT. We require each newly inserted connection to have, in its data object, an attribute whose key is "id" and whose values are strings that are unique across the IT.

   source - must be the id associated with precisely one IS in the IT, which will be the source of the new connection to insert.

   target - must be the id associated with precisely one IS in the IT, which will be the target of the new connection to insert.

   data - must be JSON data that will be stored as the third element in the connection triple; note the requirement that it contain an "id" field, given above.

   If any of the above requirements on the parameters are not satisfied, the routine does nothing. Note that the first two parameters' requirements ensure that connection closure of the IT is maintained by this routine.

6. removeConnection(connection) removes an existing connection between two ISs in the IT.

   connection - must be the id associated with precisely one connection inserted earlier into the IT, the id stored in its JSON data, as given during the call to insertConnection().

   If the above requirement on the parameter is not satisfied, the routine does nothing.

7. setConnectionAttribute(connection,key,value) alters the data of an existing connection between two ISs in the IT.

   connection - must be the id associated with precisely one connection inserted earlier into the IT, the id stored in its JSON data, as given during the call to insertConnection().

   key - should be a string that is the key of the attribute to be modified, but if it is not a string it will be converted into one using JavaScript's String constructor. This cannot be the string "id" because that must remain constant throughout the life of the connection.

   value - should be any JSON data to use as the new attribute value, or the JavaScript value undefined. Using undefined will remove any old key-value pair with the given key from the specified node.

   If any of the above requirements on the parameters are not satisfied, the routine does nothing.

We may also create a wrapper around this API that allows the client to create its own tree, which will automatically sync its state to the LDE through API calls. But such a convenience API is not a necessary component of the current design; it is just a "nice to have" for some clients, and is thus not a priority.

LDE Messages

The LDE will use the ordinary event emitting classes in JavaScript (EventEmitter in Node, EventTarget in browsers) to send messages to clients as documented in the Design Overview. Such feedback can come in such a wide variety of flavors that we do not wish to constrain it here more than necessary.

1. The LDE will provide the following guarantees.

   1. Messages from the LDE will always be in JSON form.

   2. Messages from the LDE will always have a type attribute, which will be a string. Documentation for the LDE must provide a finite list of all possible values for this attribute, with a human-readable description of what each one means, and what other attributes the message object will have in each case. See below for reasons why we mandate this type attribute.

      For example, one type of message from the LDE might be to indicate that the LDE has finished validating the user's work. We might stipulate that its type is "Validation has completed." and that feedback messages of this type do not contain any additional data, or perhaps they include the amount of time validation took to run. (This is merely an example.)

   3. When a message contains feedback about the user's work, it will always contain a subject field that indicates which IS in the IT is the subject of the feedback, by mentioning the unique id of that IS.

      Feedback may have an even more precise location than just the subject IS, though this is not guaranteed because it is not possible in some situations. For example, feedback about a syntax error in a formula might indicate the character at which the error was detected.

   4. Feedback does not always include judgments on the correctness of work, though that is the most common type of feedback we intend the application to provide. When feedback does include such judgments, they will be communicated through the validity field of the feedback object, which will have one of three values, "valid", "invalid", or "indeterminate".

2. Every client should satisfy the following constraints.

   1. Clients should use the subject field of any feedback message to show the user which part of the user's work is under discussion. For example, if the feedback was that a step of work was correct, then the client may choose to put a green check mark next to the content of the user's input that generated the IS in question.

   2. When even more precise location information is available (such as the character at which a syntax error was detected), that should be communicated to the user as well.

Messages from the LDE need not always fall into the category of feedback on a user's work. For instance, whenever the LDE recomputes the OT, it will transmit it in its entirety to the client, for use when storing the user's work in a filesystem (if the client supports that). As another example, if the LDE has been asked to do some automatic detection of certain parameters (such as the order in which premises should be provided to a rule of inference, or the instantiation of metavariables), then the results of that automated work can be provided as feedback, so that the client can show it to users who request it. The list above should not be seen as constraining the types of LDE messages; it merely establishes the protocol for message transmittal.

The reason we mandate that each feedback message have a specific type is to ensure that the LDE's messages are somewhat language- and context-agnostic. The first version of Lurch generated feedback by constructing English feedback strings while validating users' work, storing the results in the document so that the UI could display them as needed. This has three problems, which we avoid with this new specification.

1. It hard-codes English into the software, making it harder to localize the software for use by native speakers of other languages.
2. It mixes sentence-building code in among the core logical algorithms, which is distracting when reading them, making them harder to maintain.
3. It hard-codes a specific output format (HTML in the case of desktop Lurch) into the software, making it harder to re-use the code in other contexts (e.g., a command-line interface or $\LaTeX$ package).

By contrast, the requirement of a type attribute on all messages, with clear documentation of the meaning of every possible value of that field and any other fields that will accompany it, gives us flexibility in the following ways.

1. We can delegate to each UI the responsibility of providing an algorithm that creates natural-language feedback, and thus that algorithm can output a format suitable to the UI (plain text, HTML, $\LaTeX$, etc.).
2. The algorithms that create natural-language feedback can rely on sets of string templates, different for each natural language and output format, thus making it much easier to localize the software to a new language, by creating just a new set of templates.
3. Keeping the previous two items independent of the core LDE code makes it easy for non-experts to update or improve or extend Lurch's feedback messages without knowing how to edit anything as complex as core validation algorithms.
4. Our first implementation can be completed sooner if we use placeholder templates that output stilted or technical English, then later rewrite them smoothly, with good pedagogy and student readers in mind.
5. We are not limited to just one style of output for each language. For example, we might provide brief and verbose versions, or beginner and advanced versions, for each natural language and output format, and users can choose among them.

The reader may note that the example type given earlier in this section was "Validation has completed.", which is an actual English sentence. Rather than index the validation types by codes such as "feedback type 17" or even suggestive phrases like "validation complete", we will use very short English sentences. This makes it so that in case any template set is missing an important entry, the feedback still has a chance of being usable. For instance, if the translation into, say, Russian for novice users, didn't have an entry for the "Validation has completed." type, then having a potentially understandable simple English fallback is better than having an error code or a cryptic phrase.

Client features and the main Lurch application

Any client may provide any number of conveniences to users, as long as it can convert them into the IT using the LDE's API.

The foremost client in the designers' minds is always the web-based Lurch application that will be built on TinyMCE. That client will contain many (largely independent and usually small) features for communicating the user's intended meaning to the LDE via the LDE's API. These include conventions for processing groups (sometimes called bubbles), arrows among groups, numbered lists, section headings, finding meaning in text through regular expressions, and the meanings of various $\LaTeX$-like \shortcuts. (These features are not defined here, because this document covers the LDE, not clients.)

But higher-level conveniences are possible; here is one example: In many formal systems, a proof line has a certain standard form--a statement, then a reason name, then premise numbers. A client supporting numbered lists could include an option for interpreting all numbered list items using this statement-reason-premises convention; it would do so by placing the content of each numbered list item in the IT, each one in an IS that parses its contents in statement-reason-premises form. If the client did so, the LDE would handle the rest. This would bring about a very nice user experience in which the user just types proofs and they are graded without the user's having to indicate any additional details of how to interpret their work.

While a good client should provide the user much flexibility in choosing which of these conveniences to enable and how they should behave, some types of flexibility are undesirable. For example, the main application will probably let the user construct mathematically-named sections of the document (e.g., "proof" or "definition") which have broadly-accepted meanings that it would be educationally counterproductive to alter. Clients are discouraged from doing so for this reason.

The Lurch team may choose to follow a specific set of conventions throughout the standard dependencies that we will distribute with the Lurch application, to show best practices and help users with consistency and predictability. We may choose to enshrine those conventions in document-level settings in the standard dependencies themselves.

Division of Responsibility

This section covers some heuristics to use when considering a new feature, and whether it is the purview of the LDE or of (some subset of) its clients.

Given a particular feature or form of mathematical input, ask, "Is the feature conceptually independent of the client that inspired it?" That is, could someone who has never heard of the client in which the feature was invented still understand the feature and find it useful? If so, it is a concept that could be used with several clients, and thus probably belongs in the LDE.

If such a feature is implemented as a new type of node in the IT, this helps us ensure that its name is client-independent. For example, if the browser-based client inspired the creation of an IS class to support HTML OL elements, it should not be named using HTML terminology, but with a name that reflects the fact that it transcends browser-based clients--for example, NumberedList.

Implementing features in the LDE rather than in specific clients has some advantages, which we list here.

1. The LDE will be implemented in pure JavaScript, with no requirement for a browser context, so that it can be used in a WebWorker and in a command-line-based unit testing suite.
2. Therefore the bigger the LDE is, the higher the percentage of our code that is covered by unit tests.
3. And the bigger the LDE is, the higher the percentage of the main application's work that gets done outside the main browser thread, thus making that application more responsive.