Rules

Definition (rule, ROI). In Lurch, a rule (or rule of inference, rule of logic, or ROI) is any method for judging whether a step of work is valid.

The prototypical rules of inference are those given by the ancient Greeks, such as modus ponens, modus tollens, the hypothetical syllogism, reductio ad absurdum, and so on, each of which corresponds to a template for propositional logical inference in modern systems (e.g., from $P\vdash\bot$ conclude $\vdash\neg P$). But in Lurch, we extend this notion to include many other types of rules, a partial list of which is given here.

1. Rules that, while expressible using templates with metavariables, like the rules of logic, use some other notation, and possibly even a different scheme for matching metavariables to instances, such as the rules of Hofstadter's MIU system (i.e., $xI\to xIU$, $Mx\to Mxx$, $xIIIy\to xUy$, $xUUy\to xy$).
2. Rules that are not expressible with templates and metavariables, such as an algorithm that uses truth tables to validate propositional inferences without proof, or an algorithm that asks a CAS whether a statement is true.
3. Axioms, which can be thought of as rules of inference with no premises.
4. Theorems, which can be thought of as rules of inference that have been demonstrated to be merely shortcuts that could be expanded into much lengthier proofs if requested.

We implement all of these types of rules using the following framework.

Rules in the OT

A Rule Declaration (OR, for Output [Tree] Rule) is a subclass of OS that provides a validateStep(S) implementation. Naturally, ORs can be labeled and cited just like any other Structure in the OT.

Definition (step of work). A step of work is any OS that cites an OR.

Any interpretation routine that creates a step of work should embed within it a validate() routine that finds the cited rule and hands off validation to that rule's validateStep() function, passing the step as the argument. The LDE should provide a global validate function that takes this common default action, so that interpretation can easily install that default in most steps of work. Let us call that default validate routine basicValidate(), so that any interpretation that outputs a step of work can install validation with the following single line of code.

myStep.validate = LDE.basicValidate

The OR base class provides a simple implementation of validateStep(S), which simply returns feedback about $S$ indicating that the rule has validated nothing. Subclasses of OR will override that base implementation to do something more useful, replacing it with any algorithm they choose, such as the propositional logic or CAS algorithms in the list of examples, above.

A very important detail here is that validateStep(S) should not actually send feedback about $S$ using the ordinary LDE feedback mechanisms, but should rather merely return that feedback to its caller. The reason for this is that the Validation Features page will introduce many reasons to call validateStep(S) other than checking the user's work. For example, we might have code that explores to find reasons that might work in a given circumstance, and to do so, it needs to see if they would validate a certain step of work. Such exploration should not transmit feedback to the user, because the validation being done is not about the user's work at all. Thus we expect validateStep() to return feedback and validate() (and in particular basicValidate()) to transmit that feedback using the ordinary LDE feedback channels described in the Messages section of the Clients page and shown in the figure on the Design Overview page.

The LDE will contain subclasses of OR for the most common types of rules, including template-based rules that require matching metavariables. Such rules in the OT are subtrees whose descendants represent the rule's premises and conclusions; in our primary validation paradigm, FIC, such rules are typically Formulas. They can have options, such as whether pattern-matching is based on expression trees (as in mathematics) or strings (as in toy systems like MIU), whether the rule is one-way (if) or two-way (iff), and so on.

The Validation Features page explains how this basic formulation of ORs can be extended with a wide variety of additional features that clients can make available to users.

Rules in the IT

The most common IT representation of rules will be using corresponding nodes, one IE subclass for each of the OR subclasses, so that rules can be entered using nested structures, as we currently do in the desktop implementation of Lurch.

The Parsing page will extend this design to allow the IT to include definitions of new grammars, a feature that can be used to define grammars whose expressions parse into ORs. In this way, rule definitions in the IT are just a special kind of IE as described on the Expressions page.