Abstract Reduction Systems 3: Termination

Proving termination is of practicial significance to the programmer. Windows was known for crashing so often that serious programmers or computer scientists would not touch it. One of the reasons was that device drivers would go into an infinite loop. This problem has been sorted out thanks to formal methods that could automatically detect such problems.

Think of a while loop? How do you know that it terminates? Or maybe it doesnt? … The technique that we learn now in order to show termination of ARSs will also apply to showing termination of loops in general.

The basic idea to prove termination of an ARS $(A,\to)$ is:

Find a measure function $\phi: A \to \mathbb N$ such that $a\to b$ implies $\phi(a)>\phi(b)$.

Why does this prove termination?

Recall our examples, listed for convenience again below.

Examples:

$A$ is the set of integers $> 1$ and $m\to n$ is defined to hold if $m>n$ and $n$ divides $m$.
A is the set of finite lists (aka words) over $\{a,b\}$, $wbav\to wabv$
- maybe first sth easier:
- what if we have only one rule allowing to rewrite $abb\to aa$ in every word?^[1]
- or what if have only one rule allowing to rewrite $a\to b$ in every word?^[2]
- or what if you have both rules above?^[3]
- what now about the first question where we have one rule allowint to rewrite $ba\to ab$? ^[4]
A is the set of multisets over $\{a,b\}$, $aa\to a$, $bb\to a$, $ab\to b$, $ba\to b$
Langton's Ant is an example of an interesting ARS that is not termintating. But it nevertheless reaches some kind of stability that, even though not a normal form in the technical sense, has some resemblance with it. A point worth thinking about.

Def: Let $(A,\to)$ be an ARS. The function $\phi: A \to \mathbb N$ is called a measure function if $a\to b$ implies $\phi(a)>\phi(b)$.

Fact: If an ARS has a measure function, then it is terminating.

We have seen examples of how to use measure functions to prove termination.

What about the converse? Can we always find a measure function if the ARS is terminating?

Let us look at the following example. Working out some reductions (eg write down all reductions starting from $(4,3)$) leads us to the firm belief that it is termintatin. But what is the measure function?

Example: Let $A=\mathbb N\times \mathbb N$ and $(i,j+1)\to (i,j)$ and $(i+1,j)\to (i,i)$. Does it terminate? What is the measure function? ^[5]

References:

Baader, Nipkow. Term Rewriting and All That. 1999

  Chapter 
  	2.3 termination

Count the number of letters. More formally, you can implement a function
$l e n g t h$ and then define
$ϕ_{1} (w) = l e n g t h (w)$ . ↩︎
Count the number of "a"s. More formally, you can implement a function
$n u m b e r$ and then define
$ϕ_{2} (w) = n u m b e r (a, w)$ ↩︎
Add the two measure functions above. More formally, define
$ϕ (w) = ϕ_{1} (w) + ϕ_{2} (w)$ . ↩︎
Leaving this as an exercise for now, will see a simpler solution later when we learned about lexicographic orderings. ↩︎
Answer:
$ϕ (i, j) = i^{2} + j$ . ↩︎

Syntax	Example	Reference
# Header	Header	基本排版
- Unordered List	Unordered List
1. Ordered List	Ordered List
- [ ] Todo List	Todo List
> Blockquote	Blockquote
Bold font	Bold font
Italics font	Italics font
~~Strikethrough~~	~~Strikethrough~~
19^th^	19^th
H~2~O	H₂O
++Inserted text++	Inserted text
==Marked text==	Marked text
[link text](https:// "title")	Link
![image alt](https:// "title")	Image
`Code`	`Code`	在筆記中貼入程式碼
```javascript var i = 0; ```	`var i = 0;`	在筆記中貼入程式碼
:smile:		Emoji list
{%youtube youtube_id %}	Externals
$L^aT_eX$	L^aT_eX
:::info This is a alert area. :::	This is a alert area.