Rule Systems

January 1, 2024

Rule systems are seen in almost every programming languages paper. They are a tool for conveying very precise notions of computation. In general, is not easy to give a succinct definition of a rule system, but one can be described easily by adopting a specific representation.

A rule system consists of a set of statements of the form

\frac{P_{1} \dots P_{n}}{Q}

where $Q, P_{i}$ are propositional schemata. Here, $Q$ is called the conclusion and $P_{i}$ are called the premises.

In an acceptable interpretation that I prefer, $Q$ and $P_{i}$ are schemtata for first order sentences that lack any quantification (i.e. $P_{i}$ is in the form of $x_{i} \in A_{i}$ ), and the above statement logically means

(P_{1} \land \dots \land P_{n}) ⟹ Q .

So a rule can be read: if $P_{1}$ and $\dots$ and $P_{n}$ , then $Q$ .

In essence, rule systems describes the objects of sets. For example,

\frac{}{0 \in N} \frac{n \in N}{S (n) \in N}

are the rules that may be used to describe the set of natural numbers. This shows how an inductive set may be defined via a rule system. Though, here we are interested in the case of relations.

When the set $A$ being described is a relation, that is $A \subseteq R_{1} \times \dots \times R_{n}$ for sets $R_{i}$ , $A$ is essentially the truth set that is inductively defined via the rules. When presented, mixfix notation is almost always used to better convey the meaning of the relation. For example,

\frac{}{(n, S (n)) \in LT} \frac{(n, m) \in LT}{(n, S (m)) \in LT}

where $(i, j) \in LT$ can be denoted as $i < j$ . It is also common for the assumption of a component belonging to a set be omitted from the premises and instead stated elsewhere. So we say $n, m \in N$ and $LT \subseteq N \times N$ .

For ease of reference, we will refere to $(i, j)$ or $i < j$ as the judgement and the values $i, j$ as components. We will also define the truth of a judgment to be equivlent to it belonging to the set that is defined, so $i < j$ is true when $(i, j) \in LT$ . Then we can rewrite this rule system as

\frac{}{n < S (n)} \frac{n < m}{n < S (m)} .

TODO: more examples

Proof System

How do you know if a given judgment is true? A judgment is true when you can derive it from the axioms using the rules in the rule system. A good way to check if judgment is true for a rule system is to start with the conclusion, then attempt to recursively apply the rules by pattern matching on the conclusions, filling out each of the premises. This process results in a proof tree for the original judmgnent, and the truth is known if the leaves of the tree are axioms, and each rule is correctly applied. Check out this article by Daniel.

For an example, here is a proof tree for $2 < 5$

\frac{\frac{}{2 < 3} \frac{\frac{}{3 < 4} \frac{}{4 < 5}}{3 < 5}}{2 < 5}

using the rules

\frac{}{n < n + 1} \frac{n < k k < m}{n < m} .

where $n, m, k \in N$ .

Interestingly, not all rule systems can be checked against in this way, such as propositional logic. The systems for which this proof tree generation process works are called syntax directed rule systems.

Computation

Since a function is just a special kind of relation, it is possible for a function to be defined via a rule system. Computer scientists are mostly interested in rule systems that describe functional relations, as these are often descriptions for how the function is computed.

As an example, suppose $fac : N \to N$ the factorial function $n \mapsto \prod_{k = 1}^{n} k$ , which has the equivelent recursive definition

fac (n) = {\begin{cases} 0 & if n = 0 \\ n \cdot fac (n - 1) & otherwise \end{cases} .

Note that $fac (n) = k$ is equivelent to $(n, k) \in fac$ , for any $n, k \in N$ . Using the recursive definition, we can define $fac$ in via the rules

\frac{}{fac (0) = 1} \frac{fac (n - 1) = m n \cdot m = k}{fac (n) = k} .

So, every judgment that we derive in this system, $(n, k) \in fac$ or $fac (n) = k$ , we have that $k$ is the result of computing the $fac$ function on the input $n$ .