Abstract Reduction Systems 4: Termination (Finitely Branching Systems)

We continue from the previous lecture.

Definition: An ARS

$(A,\to )$, or sometimes its relation

$\to$, is called finitely branching if for all

$x$ there are only finitely many

$y$ such that

$x\to y$.

Theorem: Let

$(A,\to )$ be a finitely branching ARS. The ARS is terminating if and only if there is a measure function

$\varphi :A\to \mathbb{N}$ .

Proof: "if" has been discussed in a previous lecture.

"only if:" That is the interesting direction here.

Let us first look at an argument as you might find it in a textbook.^[1]

We have to find a measure function

$\varphi :A\to \mathbb{N}$. Define

$\varphi (a)=|\{b\in A\mid a\stackrel{\ast }{⟶}b\}|$. This is well-defined since

$\{b\in A\mid a\stackrel{\ast }{⟶}b\}$ is finite due to

$A$ being finitely branching and terminating. It remains to show that

$a\to b$ implies

$\varphi (a)>\varphi (b)$. Since

$\stackrel{\ast }{⟶}$ is transitive, we have

$\varphi (a)\ge \varphi (b)$. Now suppose

$\varphi (a)=\varphi (b)$. Then

$b\stackrel{\ast }{⟶}a$ in contradiction to

$(A,\to )$ being terminating.

Sometimes a more concise write-up can be easier to understand than an argument that provides all details. On the other hand, one cannot claim to fully understand an argument without being able to provide all details. I show you how such a more detailed write-up could look like.^[2] It is also an opportunity to learn the patterns that are used in proofs. And it is closer to what we have done in class.

Show: If

$A$ is finitely branching and terminating, then there is a measure function

$\varphi :A\to \mathbb{N}$.

Assume that

$A$ is finitely branching and terminating.
Show that there is a measure function

$\varphi :A\to \mathbb{N}$. ^[3][4]

Define

$\varphi (a)=|\{b\in A\mid a\stackrel{\ast }{⟶}b\}|$. ^[5]
Show that

$a\to b\Rightarrow \varphi (a)>\varphi (b)$.

Assume

$a\to b$.
Show

$\varphi (a)>\varphi (b)$.
This, in turn, means that we have to show the following two statements.^[6]

(One)

$\{c\in A\mid a\stackrel{\ast }{⟶}c\}\supseteq \{d\in A\mid b\stackrel{\ast }{⟶}d\}$ ^[7]
This follows from

$\stackrel{\ast }{⟶}$ being transitive.^[8]

(Two) There is

$x\in \{c\in A\mid a\stackrel{\ast }{⟶}c\}$ and

$x\notin \{d\in A\mid b\stackrel{\ast }{⟶}d\}$.
To show that such an

$x$ exists means to show that
there is

$x\in A$ such that

$a\stackrel{\ast }{⟶}x$ and not

$b\stackrel{\ast }{⟶}x$.

Define

$x=a$.^[9] We need to check two statements.

(First) Show:

$a\stackrel{\ast }{⟶}a$.
This follows because

$\stackrel{\ast }{⟶}$ is reflexive by definition.

(Second) Show: not

$b\stackrel{\ast }{⟶}a$.
We argue by contradiction.^[10]

Assume

$b\stackrel{\ast }{⟶}a$.
Then^[11]

$a\stackrel{+}{⟶}a$.^[12]
Which contradicts that

$(A,\to )$ is terminating.

We showed (Second): not

$b\stackrel{\ast }{⟶}a$.

We showed (First) and (Second).

We showed (Two).

We showed

$a\to b\Rightarrow \varphi (a)>\varphi (b)$.

We showed

$\varphi (a)>\varphi (b)$.

We showed that there is a measure function

$\varphi :A\to \mathbb{N}$.

We showed the theorem.

We will have a look at the logic behind this argument in the next lecture.

---

1. See also Lemma 2.2.3 in Baader-Nipkow. ↩︎

2. I would not normally use indentation as below, but markdown conveniently provides this feature and I thought maybe it helps. ↩︎

3. We need an idea. In class, we drew a picture, picking an element

   $a\in A$, and drawing an example relation
   $\to$. After a while we found the idea that it follows from finitely branching and terminating that there are only finitely many elements reachable from
   $a$. This gave us the idea to define
   $\varphi (a)$ as the number of elements reachable from
   $a$. That is,
   $\varphi (a)=|\{b\in A\mid a\stackrel{\ast }{⟶}b\}|$. ↩︎

4. Defining a function

   $\varphi$ that satisfies
   $a\to b\Rightarrow \varphi (a)>\varphi (b)$ is analogous to implementing a program that satisfies that requirement. But notice how much simpler it is to define
   $\varphi$ in mathematical notaion rather than implementing a function that actually computes the set of reachable elements. This is a nice example of the power of mathematics as a specification language. ↩︎

5. Lemma: If

   $(A,\to )$ is finitely branching and terminating, then
   $\{b\mid a\stackrel{\ast }{⟶}b\}$ is finite for all
   $a\in A$. ↩︎

6. By definition of

   $\varphi$. We use that
   $|C|>|B|$ if and only if
   $C⫌B$ if and only if
   $C\supseteq B$ and
   $\mathrm{\exists }x\in C.x\notin B$. (We assume here that
   $B$ is finite. ) ↩︎

7. In words: Everything reachable from

   $b$ is reachable from
   $a$. ↩︎

8. The general pattern to show a statement of the form

   $D\subseteq C$ is to assume
   $d\in D$ and to show
   $d\in C$. Here, we assume
   $b\stackrel{\ast }{⟶}d$. We also know
   $a\to b$. Then
   $a\stackrel{\ast }{⟶}d$ by transitivity. ↩︎

9. How do we find such an

   $x$? I would suggest to draw a picture of the situation. But also if just make a guess,
   $x=a$ is an obvious one to try. ↩︎

10. The general pattern to prove a negative statement such as "not

    $b\stackrel{\ast }{⟶}a$" is to assume the statement and derive a contradiction. ↩︎

11. We assumed (see further above) that

    $a\to b$ and also assumed that
    $b\stackrel{\ast }{⟶}a$. Now use transitivity. ↩︎

12. The notation

    $a\stackrel{+}{⟶}a$ means exactly that there is cycle from
    $a$ to
    $a$. ↩︎