__Term rewriting__

G.J. Bex

**Example: simple arithmic**

The natural numbers can be represented in the following way: 0 = 0, 1 = s(0), 2 = s(s(0)), 3 = s(s(s(0))),...

Below are the definitions for the addition of natural numbers:

`> `
**define(`&++`,
&++(0,Y::anything) = Y,
&++(s(X::anything),Y::anything) = s(&++(X,Y)));**

The definitions for multiplication are given below:

`> `
**define(`&**`,
&**(0,Y::anything) = 0,
&**(s(X::anything),Y::anything) = &++(&**(X,Y),Y));**

`> `
**s(0) &++ s(s(0) &** s(s(0)));**

`> `
**s(0) &++ 0;**

`> `
**s(0) &++ s(0);**

`> `
**s(0) &++ s(s(0));**

`> `
**s(0) &++ s(0) &++ s(0);**

`> `
**s(0) &** 0;**

`> `
**s(0) &** s(0);**

`> `
**s(s(0)) &** s(s(s(0)));**

`> `
**s(0) &** s(s(s(0)));**

`> `
**unassign(`&++`,`&**`);**

**Example: Fibonnaci**

Using the same representation for natural numbers and the addition as in the example above,

`> `
**define(`&++`,
&++(0,Y::anything) = Y,
&++(s(X::anything),Y::anything) = s(&++(X,Y)));**

the Fibonnaci function can be defined as follows:

`> `
**define(`f`,
f(X::anything,Y::anything) = &->(X,f(Y,X &++ Y)));**

`> `
**define(`nth`,
nth(0,&->(Y::anything,Z::anything)) = Y,
nth(s(X::anything),&->(Y::anything,Z::anything)) = nth(X,Z));**

`> `
**nth(s(0),f(s(0),s(0)));**

Error, (in tablelook) too many levels of recursion

This example illustrates clearly that not all rewrite systems terminate and hence that care should be taken in defining as well as implementing them.

`> `
**unassign(`&++`,`f`,`nth`);**