Project Goals

Lurch aims to be a piece of software that can read students' mathematical reasoning and quickly give them feedback that helps them learn to do such reasoning better.

For more details on this goal, see a chapter in Beyond Lecture, a 2017 paper on the UI, a 2013 paper on the desktop version, a 2013 paper on how that version uses OpenMath, some project-wide GitHub documentation, the current desktop version, and that version's Advanced Users' Guide.

This goal motivates the following requirements for the deductive engine. Each goal will be justified in this wiki.

Feature Requirements

The LDE must be able to do several things.

1. It must receive an ordered tree as input, from which it attempts to deduce the user's mathematical meaning.

   This is because the LDE supports mathematical content and document structure content, both of which are, by nature, hierarchical data.

2. It must construct a tree representing the user's mathematical meaning and generate syntactic feedback about the success and/or failure of the attempt to do so.

   The LDE constructs meaning in a tree separate from the input tree so that there is flexibility in how the input is interpreted or altered as its meaning is constructed. For example, one input node might be a single mathematical expression represented as text, whose meaning is an entire hierarchy in its own right.

   We refer to the collective activity of item 2 as interpretation. All syntactic feedback is constructed as a result of interpretation, and includes, for example, syntax errors in mathematical notation.

3. It must process the constructed meaning and generate semantic feedback about the results.

   This is the educational purpose of the entire project.

   Because one of our main uses of this feature is to generate feedback about the validity of steps of work in a proof, we will refer to the collective activity of item 3 as validation. All semantic feedback is constructed as a result of validation.

4. It must return all feedback to the client, referencing any relevant node or nodes in the input and output tree in a way that is helpful to the user, so the client can report it to the user.

   If the feedback were not shown to the user by the client in a way that enables the user to identify which part or parts of the user's input or which meaning that was constructed from that input the feedback is discussing, or the user cannot benefit from the feedback. So we stipulate that the LDE will usually associate each piece of feedback with one or more input nodes and/or meaning; this is a client-agnostic way of telling the client the locus of the feedback.

Other forms of feedback can also expose the inner workings of the LDE (such as which modifiers were applied to which input nodes, which premises were auto-detected, which metavariable instantiations were auto-provided, etc.). Feedback in each of these cases can be classified as either syntactic or semantic depending on whether it is generated via item 2 or item 3, respectively.

Design Style

In addition to feature-oriented goals, we also have stylistic goals: elegance and simplicity of design. There are several reasons for these two stylistic goals.

• They make Lurch easier to explain to students or in other documentation,
• they make Lurch easier to test because it has fewer unusual corner cases or special circumstances,
• they make Lurch easier to implement for the same reason, and
• a design that's easier to contemplate in one's head as a whole gives us greater confidence in it.