The following example illustrates an abstract data type (ADT) style of programming functions.
The data type defined here is the type of natural numbers.
In ADT theory there is usually no difference between *constructors*, which make up a term
in normal form, and *functions*, which can be applied to terms.
The difference between these two is only a property of the rewrite system.
In the phylum, both of them are operators.

/* the abstract data type of natural numbers */nat: zero() | s(nat) | plus(nat nat) | mul(nat nat) | ack(nat nat) ;

/* rewrite rules for addition, multiplication, and Ackermann's function */plus(x, zero())-> x; ack(zero(), x) -> s(x); plus(x, s(y))-> s(plus(x, y)); ack(s(x), zero())-> ack(x, s(zero())); mul(x, zero())-> zero(); ack(s(x), s(y)) -> ack(x, ack(s(x),y)); mul(x, s(y)) -> plus(mul(x, y), x);

Here is the program to call the function.
We build a term corresponding to the application of *ack*, and then rewrite this into
normal form.

#include`"k.h"`

#include`"rk.h"`

nat n2, n3;

voidmain() { n2 = s(s(zero())); n3 = s(n2); print_nat(rewrite_nat(ack(n3, s(n3)), base_rview)); }