The Lurch Core Classes Source Code Documentation

This API documentation covers the core classes underpinning the Lurch application. The navigation menu on the left shows classes and namespaces in alphabetical order, but the overview below is more logically organized.

Tutorials

Probably the easiest way to get familiar with the classes and methods defined in this repository, together with how to use them, is to read the tutorials:

• Constructing LCs
• Methods in each LC subclass
• LC tree hierarchies
• Serialization and attributes of LCs
• Free and bound variables
• Connections among LCs
• Pattern matching
• Lurch Node REPL

Foundational classes

Every symbolic math software needs some data structure for storing trees of mathematical symbols that represent mathematical meaning. In the LDE, the most generic of these is the Math Concept.

Later, complex math concepts will be able to be compiled down to a set of simpler special cases that can be processed by the LDE. We call that simpler subset the Logic Concepts, or LCs for short.

Logic concepts come in three types: Environment, Declaration, and Expression.

Environments are either the base type, Environment, or a subclass called Binding Environment, which can bind symbols, such as when constructing subproofs about arbitrary variables.

Expressions come in three types: Symbol, Application, and Binding Expression.

Other tools

Other basic tools support the classes above, including:

• a class for connecting math concept instances irrespective of tree structure,
• functions for working with JSON and serializing it.

There is also a host of advanced tools for doing pattern matching with Logic Concept instances.

And when working in the test suite, feel free to import the Database module for access to a library of Logic Concept instances written in putdown notation, with corresponding metadata.

GitHub

This repository is for the full Lurch project, not just the core classes documented here.