Exercises on Rewriting (2020)

# Exercises on Rewriting (2020) I collect here exercises to practice the material that will be the subject of the midterms and of the final exam. But remember that there also are exercises throughout the [lecture notes](https://github.com/alexhkurz/programming-languages-2020/blob/master/lecture-by-lecture.md) ... see in particular the sections labelled Homework in the section on Rewriting. The exercises you can hand in to me on pen and paper, send to me via email, discuss in my office hours ... there is no due date and they are not graded, but some engagement with the exercises is indispensable for good grades at the midterm and exam. In the midterm, there will be questions about Lambda Calculus and about String Rewriting similar to the Exercises. Moreover, be prepared to define notions like ARS, normal form, confluence, … --- ## String Rewriting To do the exercises you need to use the material about equivalence relations and abstract reduction systems and termination and invariants  In the exercises in this section, **I give you algorithms, but do not tell you what they are meant to compute**. This is for you to find out ... Here is a roadmap that you may find useful. [^meaning] [^meaning]: If we are able to successfully carry out such an analysis, we have three ways to think about the *meaning* of a word: as its equivalence class, as its normal form, and through its invariant. - The basic question is how many equivalence classes are there and how we can recognise in which equivalence class a given word is. - A good idea with any problem solving task is to collect some basic facts and obervations and then to see what patterns emerge. Are there normal forms? What are they? Do all elements reduce to a normal form? Are normal forms unique? - Can we characterise equivalence classes by unique normal forms? - Can we characterise equivalence classes by invariants? Here it will orten be useful to remember modular arithmetic. - Does the system terminate? The first exercise, SR1, is intended to be easy. If it is not, and assuming that you revised the relevant material, the reason must be that I didn't explain some background you need ... let me know if this is case. #### Exercises (String rewriting) (essential, examinable) In this exercise we rewrite strings over letters `a,b` and write `s -> s'` for a pattern or schema of rules (called ***rewrite rules***) that allows to reduce strings by replacing any occurrence of a substring `s` by the string `s'`. The rewrite rules `s ->` allows us to erase the substring `s` from any word in which `s` occurs. - **(SR 1)** Consider the rewrite rules ab -> ba ba -> ab aa -> b -> - Reduce some example strings such as `abba` and `bababa`. - Why is the ARS not terminating? - How many equivalence classes does $\stackrel{\ast}{\longleftrightarrow}$ have? Can you describe them in a nice way? What are the normal forms? [Hint: It may be easier to first answer the next question.] - Can you change the rules so that the ARS becomes terminating without changing its equivalence classes? Which measure function proves termination of your modified system? - Write down a question or two about strings that can be answered using the ARS. Think about whether this amounts to giving a semantics to the ARS. [Hint: The best answers are likely to involve a complete invariant.] - **(SR 2)** Consider the rewrite rules ba -> bbaa aa -> ba -> ab ab -> ba - Can one reduce `ab` to `aabb`? - Can one reduce `ba` to `abbaababbab`? - Can one reduce `ba` to `abbaababbaba`? - Can you find a nice way of stating which words are in the equivalence class of the empty word `[]` and in the equivalence class of `a`? - Can you list some properties of words that remain invariant under application of rules?[^invariant] - Can you describe all equivalence classes? (That requires some work.) - Can you change the rules so that the ARS becomes terminating without changing its equivalence classes? (This also requires more work. It helps if you answered the previous question first.) Which measure function proves termination of your modified system? - I wrote out a [guided tour](https://hackmd.io/SA-Z-oOAQiKKnlniCQmYkg) for the last to items, but try first yourself. - **(SR 3)** Consider the rewrite rules ab -> a bb -> b aa -> b plus rules saying that the order of letters does not matter. - Think of `a` and `b` as colours and an [urn](https://en.wikipedia.org/wiki/Urn_problem) that has balls of colour `a` ("white") and `b` ("black"). Interpret the rewrite rules as rules about drawing balls from the urn. - If you start with 198 black balls and 99 white balls, what is the colour of the last ball remaining? - Answer the question above with the help of a suitable invariant. - If you start with $n$ black balls and $m$ white balls, what is the colour of the last ball remaining? - **(SR4)** (optional, more difficult). Consider rewrite rules ab -> cc ac -> bb bc -> aa plus rules saying that the order of letters does not matter. Starting from 15 `a`, 14 `b` and 13 `c`, is it possible to reach a configuration in which there are only `a`s or only `b`s or only `c`s? (Actually, once you found a helpful invariant, the problem is not difficult anymore.) --- #### Optional Exercise (ORK) (from Goedel, Escher, Bach) If the last letter is R you may add a K at the end A string of the form Ox may be rewritten to Oxx You may replace any occurrence of RRR by K You may erase any occurrence of KK Above, `x` is a variable that maybe replaced by any string. - Describe an ARS $(A,\to)$ that is given by the 4 rules above. - Give some sample reductions. Can you reduce `OK` to `OR`? - Is it possible to reduce `OR` to `OK`? As it often happens with this kind of exercises, it can be quite tricky until you suddenly see the solution. But trying to understand what is going on pays off in any case. --- ## Other Rewriting Systems The purpose of the next exercise is for you to apply the new technical notions to an example you know well already. (We have done some of this exercise in class already, but it would be good to do it again at home.) #### Exercise (Fractions) (important illustration of confluence and normal form) - To simplify, we only consider positive fractions. Define an equivalence relation $\equiv$ on the set $\mathbb N\times \mathbb N$ such that the set $\mathbb N\times \mathbb N/{\equiv}$ of equivalence classes is in bijective correspondence with positive fractions. In other words, $(a,b)\equiv(c,d)$ if and only if, in mathematical notation, $a/b=c/d$. - Define an ARS $(\mathbb N\times \mathbb N,\to)$ in which two fractions reduce to the same normal form if and only if they are equivalent. - Give a complete invariant for this ARS. - Explain how to add and multiply normal forms.  --- The next exercise illustrates that there is a tight connection between reductions in ARSs and the evaluation of recursive functions. In fact, ARSs are the model of computation behind recursive functions. #### Optional (but interesting) Exercise (The Ackermann function) The A-function has a recursive definition as follows. a(0,n) = n+1 a(m+1,0) = a(m,1) a(m+1,n+1) = a(m, a(m+1,n)) - Write out some recursive computations by hand such as a(1,2). - Challenge: What are the biggest numbers $n,m$ for which you can compute $a(n,m)$? (Hint: Feel free to use a computer to get to bigger numbers.) - Can you find an interpretation of the A-function? What do the functions `a(1,n)`, `a(2,n)`, `a(3,n)`, etc compute? - Bonus question: If you let $n$ in the first equation range not over numbers but over expressions, then the ARS defined by reading the equations from left to right is non-deterministic.[^deterministic] Is it confluent? --- The rewrite system of the next exercise is known as [Combinatory Logic](https://en.wikipedia.org/wiki/Combinatory_logic) and one of the most interesting and important ones. As simple as it is, it is Turing complete! It is also equivalent to $\lambda$-calculus in a fairly straithforward way, even if it looks totally different and does not contain any variables. For a fun introduction and many more exercises see Smullyan's [To Mock a Mockingbird](https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird). #### Optional (but interesting) Exercise (Combinatory Logic) The language is given by all words (also called "combinators") that can be formed from one binary operation, parentheses and symbols `I,K,S`. The equations/rewrite relations of Combinatory Logic are Ix = x (Kx)y = x ((Sx)y)z = (xz)(yz) Some general remarks: - The binary operation, which we write just by putting two terms next to each other, is meant to be similar to application in $\lambda$-calculus. So we can think of `I` as the identity function that, applied to an argument `x` evaluates to `x`. - We use this analogy to drop parentheses according to the same rules as in $\lambda$-calculus. That is we can simplify to `Kxy=x` and `Sxyz = xy(xz)`. Questions: - Show that if `Kx=Ky` then `x=y` (this is a special property of `K`). - From `K` and `S`, can you define a combinator `B` satisfying `Bxyz = x(yz)`?  This combinator is important because it corresponds to sequential composition of programs (usually written as `;` in imperative programming languages). - Can you define `I` in terms of `K` and `S`? - Implement the `IKS`-system using the $\lambda$-calculus. In particular, it must be possible to simulate the reductions `Ix -> x` and `Kxy -> x` and `Sxyz -> xz(yz)`. The converse, namely how to translate $\lambda$-calculus to combinatory logic is interesting. In particular, it shows that programming languages could be implemented without variables, using only combinators. While the translation [is tricky](https://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis), we can do some examples. Questions: - Translate $\lambda x.x$ to combinatory logic. [Hint: Use `I`.] - For $x\not=y$, translate $\lambda x. y$ to combinatory logic. [Hint: Use `K`.] - Translate $\lambda x.x x$ to combinatory logic. [Hint: Use `S`.] I mentioned Smullyan's delightful [To Mock a Mockingbird](https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird) above. Smullyan tells a story about birds living in a wood and singing names of birds. If you call out the name of bird `B` to bird `A`, then `AB` is the name of the bird that `A` calls out in response. `I` is the identity bird (or we could call it the echo-bird). `K` (kestrel) and `S` (starling) are also birds. There are also many more birds. A central role is played by the so-called mockingbird. A *mockingbird* is a bird `M` satisfying the equation Mx = xx In words: For any bird `x`, the mockingbird replies to `x` with the name that `x` would reply to on hearing his own name. - Implement `M` in the $\lambda$-calculus. - Show that `M` can be implemented in combinatory logic using `S` and `I`. - Smullyan says that `A` is fond of `B` if `AB=B`. Show that every bird is fond of some bird. [This is difficult without a hint[^hintCAM], but give it a try first.] In $\lambda$-calculus the last item above is known as "every function has fixed point". Let us follow Smullyan for a bit longer. - `A` is egocentric if `A` is fond of itself. Show that there is at least one egocentric bird. - A bird `A` is agreeable if for all birds `B` there is a bird `x` such that `Ax=Bx`. Is the mockingbird agreeable? - Let `X` be any bird and let `H=CXA`. Since `A` is agreeable, `A` agrees with `H` on some bird `Y`. Show that `X` is fond of `AY`. - ... I stop here, the story goes on in Chapter 9 of the book ... highly recommended ... it is fun and you learn some serious maths about combinatory logic and $\lambda$-calculus on the way. --- **Optional (but interesting) Exercise (Turing machines as rewrite systems)** A [Turing machine](https://plato.stanford.edu/entries/turing-machine/) is a finite state machine moving a head over an infinite tape, reading and writing one symbol at a time. A particular TM can be specified by set of rules of the form $$(q,S,S',M,q')$$ saying that if the TM is in state $q$ reading $S$ on the tape then it replaces $S$ by $S'$, moves the head in direction $M\in\{L,R\}$ and goes to state $q'$. Argue that any TM can be equivalently formulated as a string rewriting system. For example $$(q,S,S',R,q')$$ can be represented by the rewrite rule qS -> S'q' Give some [examples](https://en.wikipedia.org/wiki/Turing_machine_examples) of TMs as rewrite systems and do some simple example computations by pen and paper to check that the traditional definition and the rewriting definition are equivalent. Remark: On the other hand, our notion of ARS is too abstract to obtain the converse: There are ARSs $(A,\to)$ that cannot be simulated by a Turing machine. This is because the notion of ARS does allow sets $A$ and relations $\to$ that are not computable. In fact, every mathematical function, can be represented by some ARS. To capture computability, we need to restrict our attention to particular ARSs, such as TMs, $\lambda$-calculus, combinatory logic, or any other of the many equivalent notions that computer scientists have invented. That all these different attempts at formalising the notion of comutability are equivalent gave rise to the [Church's thesis](https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis). --- The next example is typical for a situation where the elements of the ARS are not mere strings but terms. We encountered this before when we discussed arithmetic expressions. Recall how terms really are trees, even if written in linear (or, as we sometimes say, one-dimensional) notation. #### Exercise (Sorting) (important for general background) Consider the ARS, from [Dershowitz: A Taste of Rewrite Systems](http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=FC8676559B7A991F184EA8DA76458837?doi=10.1.1.31.6812&rep=rep1&type=pdf), given by max(0,x) -> x max(x,0) -> x max(s(x),s(y)) -> s(max(x,y)) min(0,x) -> 0 min(x,0) -> 0 min(s(x),s(y)) -> s(min(x,y)) sort([]) -> [] sort([x | xs]) -> insert(x,sort(xs)) insert(x,[]) -> [x] insert(x,[y|ys]) -> [min(x,y)|insert(max(x,y),ys)] where - operation symbols are - constants: `[]` and `0` - unary: `s` and `sort` - binary: `[-|-]` and `min` and `max` and `insert` - and variables are `x` and `y` and `xs` and `ys` Do the following exercises. - Give small examples of reductions for each of `min`, `max`, `sort`, `insert`. - Discuss the properties of termination, confluence, unique normal forms in this example. - Give an invariant of this rewriting system. - In what sense, if at all, is it appropriate to consider `min`, `max`, `sort`, `insert` as functions? Your answer should make use of what we learned about syntax and semantics. - Compare this example with the implementation of `sort` in Assignment 1. What are the similarities and what are the differences? --- ## Termination **Exercise:** Do, or revise, the termination part of Exercises SR1 and SR2 above. (The following termination exercises are taken from the book by Baader and Nipkow.) **Exercise (T1):** Show that whatever the test `<TEST>` the program below while ub > lb + 1 do begin r : = (ub + lb) div 2; if <TEST> then ub := r else lb := r end terminates. Are there any assumptions you need do make the argument work? **Exercise (T2):** Show that the two programs while m =/= n do if m > n then m := m — n else n := n — m and while m =/= n do if m > n then m : = m — n else begin h :=m; m :=n; n := h end terminate. Are there any assumptions you need do make the argument work? **Exercise (T3):** Take a program with a while loop from on of your other courses and show termination by exhibiting a measure function. ---  [^invariant]: A function $P:A\to B$ is an ***invariant*** for an ARS $(A,\to)$ if $$ a\to b \ \Longrightarrow \ P(a)=P(b)$$ for all $a,b\in A$. [^deterministic]: An ARS $(A,\to)$ is ***deterministic*** if for all $a\in A$ there is at most one $b\in A$ such that $a\to b$. [^alpha]: We take lambda-terms here up to $\alpha$ equivalence, so you may rename bound variables at any point in your computation without explicitely invoking a rule. [^signature]: STOP reading if you do not want to see hints at the solution. - In case of string rewriting, the question is what are the operations that we use to form words such as `aba` from letters `a` and `b`? There are at least three possibilities. 1. Empty word, binary concatenation and constants for the letters. This needs some equations. 2. Unary operations for each letter. This does not need any equations. 3. One $n$-ary operation for each natural number $n$ to construct a lists lenght $n$. - In case of the sorting example, the signature is given by constants `0`, `[]`, unary operation symbols `s`, `sort`, and binary operation symbols `[-|-]`, `min`, `max`, and `insert`. We can also refine this to a "many-sorted signature" by introducing types `nat` and `natlist` and say that operation symbols are typed as follows (in, hopefully, self-explanatory notation) 0 : nat s : nat -> nat max : nat,nat -> nat min : nat,nat -> nat [] : list [-|-] : nat, natlist -> natlist insert : nat, natlist -> nat sort : natlist -> natlist [^hintCAM]: Show that `A(CAM)(CAM)=(CAM)(CAM)` where `C` and `M` are defined as above.