RRS Overview

Motivation

It would be amazing to have a simpler definition of an algorithm.

In theoretical computer science, we have many computational models. The following is a subjective critique:

• A Turing Machine, the canonical computational model, is formally a 7-tuple. The definition contains special states an symbols. It works on a tape, however there are multiple versions — there are one-tape and many-tape machines, moreover the tapes can be infinite, one-way infinite, or finite with an expansion.

• Lambda Calculus has a mathematical appeal, however the rewrites are non-deterministic, recursion is clumsy, and the model hides that the place to rewrite “needs to be found”.

• Random-Access Machine is useful as a model for actual computers, however as a mathematical definition it is clumsy. Moreover, constant access to integer-indexed registers hides some complexity we’d expect from a mathematical model.

• Recursive Functions I do not uderstand much (yet) 😅

• …and many more.

A common practice to reason about algorithms is to pick a computational model of your choice, and say that “they are all essentially equivalent”. But I find that problematic. The reason is that there is nuance in how equivalent they are. Yes, usually the reduction preserves time complexity classes modulo a constant, or maybe a polynomial factor (hello, one-tape vs. two-tape Turing machine 🙂).

I believe we can do better. That we can reason rigorously about sub-polynomial complexities and do reductions transparently. That, for example, a logarithmic factor pops up when working with unbounded integers.

The hope from a simpler definition would be:

• Proofs about algorithms should be simpler, more transparent, and more intuitive.

• Especially, reasoning about complexity should be simpler.

• Writing programs for the computational model should be simpler.

What Is a Computational Model?

Still on the philosophical, non-rigorous level, what would you say a computational model actually is? It certainly has to do with what we can “compute with finite amount of information”. Here is my proposal, in spirit it is a generalisation of a Turing machine:

A computational model works over a storage. It consists of:

1. One of finitely many of states
2. A view over a finite (bounded) portion of storage
3. A finite transition function for the state and storage

This metadefinition implies:

• We exclude anything that secretely uses infinity (like natural-number addresses in RAM) and nondeterminism (like lambda calculus), however we can simulate both easily.
• We can restrict the storage to be countably infinite, the machine cannot access more sites.
• As with Turing machines, we can get a “constant speedup” by merging several steps together, at the cost of increasing the state size and the storage view window.

My original idea was to define the storage as a graph, and have one or even more heads operating on it. A head could change a symbol at a node, move along an edge, or create a new edge. However, such a model was still quite complex and had some technical issues.

The RRS model definition, which we give in the next section, comes from a few observations:

1. A tree structure has a good tradoff between how complex it is and what it can express. It is more flexible than a tape while still having a simple definition.
2. One head is enough, it can keep track of multiple subheads.
3. The head is not needed if the tree is rooted. The state can be stored in the root node and tree traversal is still possible with tree rotations.

RRS Definition

Terms as Rooted Trees

Let signature be a tuple $\textrm{Sig} = \{\cal C, \textrm{arity}\}$ where $\cal C$ is a finite set, and $\textrm{arity}: \cal C \rightarrow \N_0$. We call the elements of $\cal C$ constructors.

I’ll skip the formal definition of terms. They are defined inductively such that 0-arity constructors (constants) are terms, and more complex terms respect the arity. Note that we understand terms as rooted trees, not as strings.

Similarly, terms with variables are informally terms where zero or more subterms might be replaced with a variable.

Rewriting Rules

A rule is a tuple $(\textrm{lhs}, \textrm{rhs})$ of terms with variables such that:

1. Every variable occurs on both sides at most once
2. Every variable in $\textrm{rhs}$ occurs in $\textrm{lhs}$

A rule matches a term if there exists a variable substitution that makes $\textrm{lhs}$ equal to the term. An application of the rule to the term is $\textrm{rhs}$ with the same substitution.

Note that this definition only allows “matching at the root”, in contrast with the classical aproach in term rewrite systems theory which can rewrite subterms.

Root Rewrite System

For a given signature, a Root Rewrite System (RRS) is defined as a list of rules.

Input of an RRS is a term. In one step, the RRS rewrites the current term with the first rule in the list that matches. If no rule matches, we call the current term the normal form of the input term and return it on the output.

Example

A simple RRS example below adds two natural numbers.

The code below defines three constructors Zero, Succ and Add with arities 0, 1 and 2. We’ll explain the exact syntax later. The machine has two rules, m and n are variables.

Press repeatedly the Step button to simulate the machine. You can also try changing the input line.

Definition Notes

Algebraic Data Types

The terms as defined above are untyped - there is no restriction which constructors can occur at which slots. It is practical to restrict the allowed terms.

We adopt the algebraic data types approach. Skipping the formal definition, the syntax

type MyType:
    Cons1(type11, type12, ...)
    Cons2(type21, type22, ...)
    ...

defines a type MyType which is a sum (a union) of two anonymous product types with constructors Cons1, Cons2, etc. The first type is a product type with components of types type11, type12, etc.

We introduce a shorthand notation for convenience:

type MyProdType(type1, type2, ...)
# is a shorthand for:
type MyProdType:
    MyProdType(type1, type2, ...)

type MyConstType
# is a shorthand for:
type MyConstType:
    MyConstType()

You can think of a type as a set of terms, defined by rules above.

Connections to Existing Systems

Term Rewrite Systems: The theory is almost the same, the differences are that 1) rewrites happen only at the root; 2) the rules are linear (no double variables); and 3) the first matching rule is applied.

Functional Programming: Algebraic data types come from functional programming languages. Matching is also a paradigm widely used.

Exercises

We’d like to be able to traverse data structures. We’d also like to be able to call subroutines. Without spoiling the fun, try solving the following exercises.

Exercise 1: Reverse a List

We need some data structures. Let us define Bit and List:

type Bit:
    B0
    B1

type List<'t>:
    Nil
    L(head: 't, tail: List<'t>)

The browser language syntax (working name RRS3 language) is limited. The identifiers consist of alphanumeric characters and underscores, the leading character cannot be a number. Lowercase leading characters denote variables, capitals constructors and types. Therefore we use B0 and B1 for the bit values.

The List definition takes a type variable. The compiler does monomorphisation — it discovers which types are used and creates a separate version of the List type for each variant. This is however only a typing consideration, the terms will simply use L and Nil. The constructor name L is non-standard, shall I rename it to Cons? Note that parameter names are allowed, they don’t have a function beyond documentation.

The RRS3 language has syntax sugar a :: b for L(a, b).

Task: Write an RRS that reverses a list of bits.

Exercise 2: Compute Xor of Tree Leaves

The code below defines a binary tree data structure with bits in its leaves. Compute xor of the leaf values. Note that you can add new types.

Exercise 3: Non-destructive Tree Xor

The task is the same as before, however this time besides the xor result, also return the original tree intact. Additionally, we define the types more properly.

RRS Properties

RRS Can Simulate a Turing Machine

The core reduction is extremely simple. The root types would be State(List<Alphabet>, List<Alphabet>) for every state of the TM, and the components are the tape to the left, and tape to the right of the head. There is technical work in dealing with extending the tape when needed and the halt state.

Two Constructors Are Enough

Any RRS can be simulated with an RRS with these two constructors with at most a constant factor slowdown:

type Tree:
    E
    T(Tree, Tree)

Note that this is the smallest possible — there has to exist a constant (0-arity) constructor, and we need at least one other constructor. It is easy to prove that unary is not enough. We skip why a binary one is enough, there is a strong hint in the Universal RRS section below.

Note also that the claim can be made very rigorous after we define the universal RRS - then we can write the reduction program and reason about the complexity of both the reduction and the transformed machine.

Limited Amount of Variables and Limited Rule Depth Is Enough

This gets more nuanced, and starts to be a mathematical self-gratitifation in trying to push the limits as low as possible, ideally both limits at the same time.

On the high level though, it is a corollary of the existence of a universal machine.

Note that is also follows from the fact that RRS can simulate a Turing machine. The reduction is as follows: Take the RRS, write a TM that simulates it, and then simulate that TM in RRS as explained above. All rules of the resulting RRS will have at most 3 (or 4?) variables and depth at most 3 (or 4, depending on the construction).

Note however that going through a TM can slow the machine down. The existence of a universal RRS guarantees at most a constant factor slowdown.

Universal RRS

TODO

• The repo contains a full implementation
• Explain encoding
• Explain stack

Complexity and Reductions

TODO

More Exercises

Just for fun.

Exercise 4: Is a Palindrome?

Decide if the list on the input is a palindrome. You can use B0 for false and B1 for true (or define your own Bool type if you fancy).

Exercise 5: Binary Integers

So far, we have used the Nat type for numbers:

type Nat:
    Zero
    Succ(Nat)

The issue is that certain operations would be slow on Nat, e.g. addition of would be linear in one of the operands. Come up with an alternative representation for non-negative numbers and implement addition which takes only logarithmic time.

You can use the Playground tab in the top menu.