Simon Willison’s Weblog

Formal systems

25th September 2002

Formal Systems

These notes cover the first lecture in Dr Dan Richardson’s Formal Systems, logic and semantics lecture. I missed the lecture so these notes are being made with the help of the course notes from Dr Richardon’s homepage (which can be viewed using DVI Viewer for Windows).

In this course, a Formal System is a set of possible configurations (or arrangements) of a system and a set of rules governing the transitions that can be made between these arrangements. Configurations can be represented by data structures, and will be referred to as set D. Rules will be referred to as set R. An example of a formal system is chess—the configuration is the arrangement of pieces on the board (and the information on who’s turn it is) while the rules are the possible moves that can be made following the rules of the game. An alternative discussion of the definition of formal systems can be found here.

If X and Y are configurations within the set D, X =>_R Y means that there is a rule in the set of rules R that will allow the transition from X to Y to be made in one step.

Similarly, X =>_^*R Y means that X can be transformed in to Y using a finite sequence of transitions defined by the rules in R.

A Derivation in the formal system (D, R) is a finite sequence of rules that can be applied to an object in D. Derivations of length 0 are allowed, so X =>_^*R X is always true.

X =>_R Y must be decdable—it must be easy to determine if the transition is permitted by the rules. R is formal and must not be ambiguous—it must depend only on X and Y and not on any information outside those data structures.

While X =>_R Y is simple, X =>_^*R Y can be very complex, and forms the core problem solving activity when dealing with formal systems.

Design principles of formal systems

A formal system’s specification is a statement defining what a formal system should do, for example “the system should model the rules of chess”. The following criteria are used to judge how well a formal system meets its specification:

1. Completeness—it must do everything the specification requires
2. Correctness—it must not do anything that the specification prohibits
3. Simplicity (also called the Occam’s razor condition). This is discussed here, and is paraphrased as Simple explanations are preferred to complex ones
4. Naturalness—the system should be intuitive.

Confluence and termination

A formal system is terminating if it does not contain any infinite derivations, so no matter what choices are made the derivations will eventually stop. The best way of working out if a formal system is terminating is to check for possible loops in the set of rules.

A formal system is confluent if whenever A =>^* B and A =>^* C there exists D so that B =>^* D and C =>^* D—the computations, once separated, can always be brought back together again. A system is locally confluent if the above is true but for A => B and A => C (i.e a single level decision can be reverted).