Abstract Reduction Systems 5: (2018 Lexicographic Orderings)

(more or less finished but not polished … feedback welcome)

Aims

• Extend our methodology of proving termination of computational processes and programs

• How to construct an ARS from a program.

• Learning about the discrete maths technology of partial orders, which are of fundamental importance in many areas of computer science and the sciences in general

• On the way we illustrate some more useful programming languages technology (we may come back to those in more detail later)

  • Transforming while loops to recursion and back
  • Dijkstra's guarded commands
  • Transforming ARSs to programs
  • Well-founded induction

This is already quite a lot of material and will be taught over the course of two lectures.

Euclid's Algorithm

What is a good way of proving termination of Euclids algorithm, which is sometimes considered to be the historically first algorithm.^[1]

​​​​int a
​​​​int b
​​​​function gcd(a, b)
​​​​    while a ≠ b 
​​​​        if a > b
​​​​            a := a − b; 
​​​​        else
​​​​            b := b − a; 
​​​​    return a;

Exercise: Write the algorithm recursively.

How to prove termination by exhibiting a measure function

$\varphi$?

From programs to ARSs

If we want to find

$\varphi :A\to \mathbb{N}$, we need to first define

$(A,\to )$.

If you learned about hardware you should relate the following explanations to what you know about program counters and registers, about how the program and the data are stored in memory and about how the CPU accesses the program and the data.

Roughly speaking, when defining an ARS

$(A,\to )$ from a program, the elements of

$A$ correspond to a particular memory, while the relation

$\to$ captures the computations of the CPU.

But we don't need to go down to the machine level to understand what is going on. It is enough to understand some basics about John von Neumann's idea of how computation separates into control and data. ^[2]

The general idea is to introduce locations

$l$ in the program and to pick the relevant data. Locations can be identified by counting lines in the source code. In our case, maybe the first idea is to associate three locations

$l_1,l_2,l_3$ to the three calls of

$gcd$, in the recursive version. So a typical element of

$A$ would look like

$$(l_i,a,b)$$

where

$i\in \{1,2,3\}$ and

$(a,b)\in \mathbb{N}\times \mathbb{N}$. For example

$$(l_1,8,12)\to (l_3,8,4)\to (l_1,8,4)\to (l_2,4,4)\to (l_1,4,4)$$
We see now that in this simple example, we do not need to keep track of the locations after all, that is, we can go to a more abstract ARS where

$A=\mathbb{N}\times \mathbb{N}$ and the reductions above are simplified to

$$(8,12)\to (8,4)\to (4,4)$$

So on order to find a measure function

$A\to \mathbb{N}$ we need to find a function

$$\mathbb{N}\times \mathbb{N}\to \mathbb{N}$$

Exercise: Show that

$+:\mathbb{N}\times \mathbb{N}\to \mathbb{N}$ is a meaure function on the ARS

$(\mathbb{N}\times \mathbb{N},\to )$ where

$\to$ is given by Euclid's algorithm.

While in this case it was not too hard to guess that addition would be a good measure function, there is an easier way. Namely to think of

$\mathbb{N}\times \mathbb{N}$ as an ordered set and then use this order directly.

So our next task is to understand how to build larger orders (such as

$\mathbb{N}\times \mathbb{N}$) from smaller orders (such as

$\mathbb{N}$).^[3]

For this we need to understand we mean by order in general. While we can identify particular orders such as

$\mathbb{N}$, we need to have a general definition of what an order is.

These are the topics of the next section.

Partial orders

We want to define from the order

$>$ on

$\mathbb{N}$ and order

$(a,b)>(a^{\prime },b^{\prime })$ on

$\mathbb{N}\times \mathbb{N}$.

Exercise: Show that a first try of

$$(a,b)>(a^{\prime },b^{\prime })\stackrel{\mathrm{d}\mathrm{e}\mathrm{f}}{\iff }a>a^{\prime }\mathrm{\&}b>b^{\prime }$$ does not define a measure function on the ARS

$(\mathbb{N}\times \mathbb{N},\to )$. Can you repair the definition?

From a mathematical point of view, the reason for the failed try of the previous exercise is that we work with a strict "greater than" relation instead of with the often more useful notion of "greater or equal".

So what is an order? It is time to make some definitions. We need what we learned about relations.

Definition: A pre-order

$(P,\le )$ is a relation

$\le \subseteq P\times P$ that is reflexiv and transitive. A partial order is a pre-order that is anti-symmetric.^[4] A linear order (sometimes called total order) is a partial order which is linear, that is,

$a\le b$ or

$b\le a$ for all elements

$a,b\in P$.

This axiomatises the intuitive notion of "less-or-equal".^[5]

Examples:

• The natural numbers, rationals, real numbers are linear orders.
• The most important partial order is the
  $\subseteq$ relation. More precisely, let
  $A$ be a set an`d
  $\mathcal{P}A$ be the set of subsets of
  $A$. Then
  $(\mathcal{P}A,\subseteq )$ is a partial order. Many kinds of constraints can be formulated as subsets, so this example is important in a wide range of different application areas. It also the foundation of logic (remember Venn diagrams?).
• Voter preferences are pre-orders: Voters typically have various constraints on candidates, say
  $\{A,B,C,D\}$, such as, say
  $A\le B$ and
  $C\le D$, but do not necessarily order them linearly. They also do not necessarily break ties, so it may be that a voter has preferences
  $A\le B$ and
  $B\le A$ for different candidates
  $A,B$.^[6] So while we may not insist that preferences are linear or even partial, we almost certainly want them to be transitive.

Exercise: The points in the plane are not linearly ordered. Define at least two different ways of making them into a pre-order or partial order.

We can also axiomatise the notion of strict "less-than":

Definition: A strict partial order, or just strict order,

$(P,<)$ is a relation

$<\subseteq P\times P$ that is transitive and irreflexive.^[7]

To ease notation we make the following

Convention: Let

$(P,\le )$ be a partial order. We define relations on

$P$ as follows:

$$\begin{array}{rl}a\ge b& \iff b\le a\\ a<b& \iff a\le b\mathrm{\&}a\ne b\\ a>b& \iff b\le a\mathrm{\&}a\ne b\end{array}$$
Let

$(P,<)$ be a strict order. We define relations on

$P$ as follows:

$$\begin{array}{rl}a>b& \iff b<a\\ a\le b& \iff a<b\mathrm{o}\mathrm{r}a=b\\ a\ge b& \iff b<a\mathrm{o}\mathrm{r}a=b\end{array}$$

The definitions above already suggest that it doesn't matter whether we define a relation as a partial order or a strict order. We can always go back and forth. Indeed, whether we start with

$(P,\le )$ or

$(P,<)$ or

$(P,>)$ or

$(P,\ge )$, once we defined all the others relations, it doesn't matter which of the 4 forms we used to begin with.

We formulate this as a proposition.

Proposition: For every partial order

$\le$ there is a strict order

$a<b$ and for every strict order

$<$ there is a partial order

$\le$, the correspondences being defined as in the convention above. These correspondences constitute bijective functions from partial orders to strict orders, and from strict orders to partial orders and are inverse to each other.

Exercise: It is interesting at this point to think about whether a similar correspondence can be found for pre-orders instead of partial orders.

While the second definition (strict partial order) is closer to our application (proving termination), the first definition is often easier to use. For example, the product of two partial orders is easily defined in the obvious way:

Definition: Let

$(P_1,{\le }_1)$ and

$(P_2,{\le }_2)$
be partial orders. Define the product partial order

$$(P_1\times P_2,{\le }_1\times {\le }_2)$$

where, abbreviating

${\le }_1\times {\le }_2$ to

$\le$

$$(a,b)\le (a^{\prime },b^{\prime })\stackrel{\mathrm{d}\mathrm{e}\mathrm{f}}{⟺}a{\le }_1{a}^{\prime }\mathrm{\&}b{\le }_2{b}^{\prime }$$

Exercise: Go back to the previous exercise. Show that you get a useful notion of strict order on

$\mathbb{N}\times \mathbb{N}$ if you take the definition of product of partial orders above and then use the proposition above to translate this into a description of the product of strict orders.

Exercise: Show termination of the ARS of the Euclidean algorithm with a measure function into

$\mathbb{N}\times \mathbb{N}$ without using addition of numbers.

By the way, in order to justify the use of measure functions into

$\mathbb{N}\times \mathbb{N}$, or other strict partial orders

$(P,>)$ we need to make sure that on can go down in

$P$ only finitely many times. This property is called the well-foundedness of

$P$.

Definition: A partial order

$(P,\le )$ is well-founded if there are no infinite descending chains

$a_1>a_2>a_3>\dots$.

Remark: It is the same to say that

$(P,>)$ is terminating and to say that

$(P,\le )$ is well-founded.

Fact: Let

$(A,\to )$ be an ARS and let

$(P,\le )$ be a well-founded partial order. Then the ARS is terminating if there is a measure function

$\varphi :A\to P$, that is, a function such that

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

Remark: To summarise, from the point of view of our application, partial orders are interesting because the product of linear orders is not linear but only partial in general.

This finishes the first lecture on the topic

More examples

Example: We talked about The Ackermann function, see also the Wikipedia article for more information. If you implemented the Ackermann function, you know that termination is not experimentally observable even for quite small inputs. This shows that what happens computationally is not straight-forward. But the termination argument that we are going to see is. This is a good example for the power of abstraction: Complicated computations can be understood, at least to some extend, by simple abstractions.

Let us go back another example that we have seen already and which I quote again below.

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?

We can also write this as a program, where the -> notation is much like an if ... then ... but allows to choose non-deterministically between the two branches as long as the condition (the "guard") is satisfied. This is called Dijkstra's guarded commands.

​​​​function example(i,j)
​​​​    j>0 -> example(i,j-1)
​​​​    i>0 -> example(i-1,i-1)

Exercise: This program only shows control flow. No actual data is computed. Can you add some data to the program?

Activity: Recall how to prove termination of this programm using a measure function into

$\mathbb{N}$.

Finding the measure function

$(i,j)\mapsto i^2+j$ is not straight-forward.

In the following, we will define a way of ordering

$P_1\times P_2$ that makes arguing for termination in the examples above much easier.

Lexicographic orders

We have already seen how to define the product of two partial orders. But this order requires us to get small either in the first or in the second component while keeping the other constant.

The lexicographic ordering allows the second component to behave arbitrarily as long as we get smaller on the first component. Only if we stay the same in the first component, the second component needs to get smaller.

In other words:

Definition: Let

$(P_1,{\le }_1)$ and

$(P_2,{\le }_2)$. Define the lexicographic product

$$(P_1\times P_2,{>}_1{\times }_{lex}{>}_2)$$

where, abbreviating

${>}_1{\times }_{lex}{>}_2$ to

${>}_{lex}$

$$(a,b){>}_{lex}(a^{\prime },b^{\prime })\stackrel{\mathrm{d}\mathrm{e}\mathrm{f}}{⟺}a{>}_1{a}^{\prime }or(a=a^{\prime }andb{>}_2{b}^{\prime })$$

We denote the lexicogrphic product by

$P_1{\times }_{lex}{P}_2$.

Fact: If

$P_1$ and

$P_2$ are well-founded, then

$P_1{\times }_{lex}{P}_2$ is well-founded. If

$P_1$ and

$P_2$ are linear, then

$P_1{\times }_{lex}{P}_2$ is linear.

Example: Let

$Teams$ be the set of teams in a soccer competition that ranks teams by points and goal difference. The table ranking all the teams is a function

$$\varphi :Teams\to Pts{\times }_{lex}GD.$$

The lexicographic product captures exactly the idea that the goal difference does not matter if one team has more points than the other, but that the goal difference decides if two teams have the same number of points. Btw, this ranking is only a preorder if two teams have the same number of points and the same goal difference.

Exercise: Model the program

​​​​function example(i,j)
​​​​    j>0 -> example(i,j-1)
​​​​    i>0 -> example(i-1,i-1)

by an ARS

$(A,\to )$ with

$A=\mathbb{N}\times \mathbb{N}$. Show that the identity function is a measure function

$A\to \mathbb{N}{\times }_{lex}\mathbb{N}$.

Example: Let us apply the same technology to the program

​​​​a(0,n) = n+1
​​​​a(m+1,0) = a(m,1)
​​​​a(m+1,n+1) = a(m, a(m+1,n))

We immediately that each recursive call either makes the first argument smaller or leaves the first the same and makes the second argument smaller. This seems taylored for the lexicographic ordering. So let us take again

$A=\mathbb{N}\times \mathbb{N}$ and define

$$\begin{array}{rl}(0,n)& \nrightarrow \\ (m+1,0)& \to (m,1)\\ (m+1,n+1)& \to (m,a(m+1,n))\end{array}$$

where

$a(m+1,n)$ stands for the value of the function

$a$ on arguments

$(m+1,n)$. There is a circularity here, though, because to be sure that

$\to$ above defines a relation of the right type, I already need to know that the computation of

$a(m+1,n)$ terminates. On the other hand, this should be clear, because the arguments

$(m+1,n){<}_{lex}(m+1,n+1)$. The difficulty lies in the fact that my definition above of

$\to$ did not completely abstract away from computational details: When writing the expression

$a(m+1,n)$, I need to first do compute

$a(m+1,n)$. But there is a possibility to make the argument more abstract and avoid this difficulty via well-founded induction.

The principle of well-founded induction states that to prove that a property

$P$ holds of a partial order

$(A,\le )$ if for all

$a\in A$ we can show that

$$(\mathrm{\forall }b<a.P(b))\Rightarrow P(a)$$

Let us see how this plays out in our example.

$A$ consists of pairs of numbers. We define

$P(m,n)$ to mean that

$a(m,n)$ terminates. According to the principle of well-founded induction, we have to show

$$ if

$a(m^{\prime },n^{\prime })$ terminates for all

$(m^{\prime },n^{\prime }){<}_{lex}(m,n)$, then

$a(m,n)$ terminates.

There are three cases to check.

First,

$(m,n)=(0,0)$. But we know that

$a(0,0)$ terminates.

Second,

$(m,n)=(m,0)$ with

$m>0$. We may assume that

$a(m-1,1)$ terminates since

$(m-1,1){<}_{lex}(m,0)$. But if

$a(m-1,1)$ terminates, so does

$a(m,0)$.

Third,

$(m,n)$ with

$m>0$ and

$n>0$. We may assume that

$a(m,n-1)$ and

$a(m-1,k)$ for all

$k$ terminate. But then

$a(m,n)$ terminates.

Summary

• Extended our methodology of proving termination of computational processes and programs

• Constructed ARSs from a programs.

• Learned about the discrete maths technology of partial orders, which are of fundamental importance in many areas of computer science and the sciences in general

  • partial order
    • generalise linear (or total) orders
    • preferences or constraints are usually partially ordered bu not linear
    • two ways of defining partial orders
  • constructing new orders from old
    • th product of partial orders
      • the product of linear orders is partial
    • lexicographic orderings

• On the way we illustrated some more useful programming languages technology

  • Transforming while loops to recursion and back
  • Dijkstra's guarded commands
  • Transforming ARSs to programs
  • Well-founded induction

Solution to some exercises

​​​​int a
​​​​int b
​​​​function gcd(a, b)
​​​​    if a = b  
​​​​        return a 
​​​​    else 
​​​​        if a > b
​​​​            gcd(a−b, b)
​​​​        else
​​​​            gcd(a, b-a)

---

1. Given the astonishing amount of science we inherited from the ancient greeks, it should not come as a surprise that we honour them by using Greek letters such as

   $\alpha ,\beta ,\gamma ,\dots \varphi ,\psi ,\dots ,\omega$ ↩︎

2. For the historically interested, why not look at John von Neumann's First Draft Report on the EDVAC. ↩︎

3. Notice that this is analogous to building bigger data types from smaller data types (like you build eg a Java class from more basic types such as int or bool or char etc). ↩︎

4. $\le$ is anti-symmetric if
   $a\le b\mathrm{\&}b\le a⟹a=b$. ↩︎

5. We switched from "greater than" to "less than" because this is more common in general. Of course, it does not really make a difference. ↩︎

6. More generally, preferences in economics (such as which goods are prefered by consumers) are preorders. This also applies to all areas of decision making. ↩︎

7. A relation

   $<$ is irreflexive if not
   $a<a$ for all
   $a$. ↩︎