Home

Under Construction

This project is undergoing a revision, starting in this documentation, which is still in progress.

While much of the content of this wiki will still apply after the revision, much of it will not.

In short, you should ignore the wiki for now. It will be updated later once the revision has made more progress.

Abstract

The Lurch Deductive Engine (LDE) will be the computational system at the heart of Lurch. It processes whatever mathematical meaning the user has communicated to the application. We call that application the client or the user interface (UI). The primary client will be the browser-based application Lurch, in which the LDE will run in one or more background threads. This wiki specifies how the LDE will function, with some necessary comments about the surrounding client.

Status

The current state of affairs is as follows:

• A very old desktop app is available here. It works fine but doesn't do nearly as much as we eventually want it to be able to do. It does not follow the UI/LDE separation paradigm described here; it was written before this new design.
• A new web version is planned. This repository will implement its internals, and is still being developed. Its UI is mostly complete, and can be found here.
• The existing documentation for this repository precedes an important redesign and will soon be superceded by this wiki. Much of the old code will be re-used, but not all.
• This wiki will become the new and definitive documentation, but that documentation-writing process has only recently begun, so this wiki is far from complete.

Summary

This section summarizes the entire rest of the wiki content extremely briefly. To read full details about any bullet point, click the link within it.

• Project Goals: This repository is about only the deductive engine inside of Lurch, an engine whose input and output data structures are hierarchical (trees). We strive for simplicity and elegance of design.
• Design Overview: The client of the LDE provides an Input Tree, which is syntactic in nature. Through two processes called Modification and Interpretation, it is converted into an Output Tree, which is semantic in nature. The Input Tree may import entire other documents as subtrees through a feature called Dependencies.
• Ordered Trees: The nodes in these trees are called Input Structures and Output Structures, which are further divided into specific subclasses not mentioned here. Each Structure can have attributes and connections to other Structures. We define three relations among structures: "is accessible to," $X\prec Y$; "appears before", $X\ll Y$; and "is connected to," $X\to Y$.
• Clients: The LDE exposes a specific API to clients, permitting them only to modify the Input Tree. It guarantees certain messages will be emitted from the LDE at certain points in its processing of the Input and Output Trees, for which clients can optionally listen, in case they need to react. While there may be many clients, the main one we plan for is the Lurch web application itself, to be built after the LDE.
• Algorithms: Upon a change to the Input Tree, the LDE first runs Modification, computing which Input Structures impact the meanings of which other ones. It then runs Interpretation, which creates the Output Tree by processing the Input Tree, usually in $\ll$ order. It then runs Scoping, which determines the scopes of all variables. Finally, it runs Validation, "grading" the user's meaning, as represented in the Output Tree.
• Steps of Work: A step of work is an individual piece of reasoning that can be graded on its own. Each is typically a mathematical Expression, often using Citations to refer to other Expressions that have Labels, and often citing a Rule such as a theorem or rule of logic.

(More to come as this wiki grows.)