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`);