next up previous contents index
Next: Rewrite Systems and Functions Up: Cookbook Previous: Attribute Grammars

Abstract Data Types and Rewrite Systems

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;
void main() { n2 = s(s(zero())); n3 = s(n2); print_nat(rewrite_nat(ack(n3, s(n3)), base_rview)); }


next up previous contents index
Next: Rewrite Systems and Functions Up: Cookbook Previous: Attribute Grammars

2000-04-17