1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 98.1p1 release (March 2nd, 1998)
originally by Nikos Drakos (nikos@cbl.leeds.ac.uk), CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>Abstract Data Types and Rewrite Systems</TITLE>
<META NAME="description" CONTENT="Abstract Data Types and Rewrite Systems">
<META NAME="keywords" CONTENT="tpman">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<LINK REL="STYLESHEET" HREF="tpman.css">
<LINK REL="next" HREF="node33.html">
<LINK REL="previous" HREF="node31.html">
<LINK REL="up" HREF="node28.html">
<LINK REL="next" HREF="node33.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html523"
HREF="node33.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="/usr/share/latex2html/icons/next.png"></A>
<A NAME="tex2html519"
HREF="node28.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="/usr/share/latex2html/icons/up.png"></A>
<A NAME="tex2html513"
HREF="node31.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="/usr/share/latex2html/icons/prev.png"></A>
<A NAME="tex2html521"
HREF="node4.html">
<IMG WIDTH="65" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="contents"
SRC="/usr/share/latex2html/icons/contents.png"></A>
<A NAME="tex2html522"
HREF="node58.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="/usr/share/latex2html/icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html524"
HREF="node33.html">Rewrite Systems and Functions</A>
<B> Up:</B> <A NAME="tex2html520"
HREF="node28.html">Cookbook</A>
<B> Previous:</B> <A NAME="tex2html514"
HREF="node31.html">Attribute Grammars</A>
<BR>
<BR>
<!--End of Navigation Panel-->
<H2><A NAME="SECTION00094000000000000000">
Abstract Data Types and Rewrite Systems</A>
</H2>
<P>
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 <EM>constructors</EM>, which make up a term
in normal form, and <EM>functions</EM>, 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.
<P>
<A NAME="1140"> </A>
<PRE><HR><!--lgrindfile: nats_newer.k 11:36 Jan 23 1997-->
<I>/* the abstract data type of natural numbers */</I>
nat: zero()
| s(nat)
| plus(nat nat)
| mul(nat nat)
| ack(nat nat)
;
<BR>
<I>/* rewrite rules for addition, multiplication, and Ackermann's function */</I>
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);
<HR></PRE>
<P>
Here is the program to call the function.
We build a term corresponding to the application of <I>ack</I>, and then rewrite this into
normal form.
<PRE><HR><!--lgrindfile: natsmain.c 15:05 Feb 20 1997-->
<B>#include</B> <code>"k.h"</code>
<B>#include</B> <code>"rk.h"</code>
nat n2, n3;
<BR>
<B>int</B> main() {
n2 = s(s(zero())); n3 = s(n2);
print_nat(rewrite_nat(ack(n3, s(n3)), base_rview));
}
<HR></PRE>
<P>
<HR>
<!--Navigation Panel-->
<A NAME="tex2html523"
HREF="node33.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="/usr/share/latex2html/icons/next.png"></A>
<A NAME="tex2html519"
HREF="node28.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="/usr/share/latex2html/icons/up.png"></A>
<A NAME="tex2html513"
HREF="node31.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="/usr/share/latex2html/icons/prev.png"></A>
<A NAME="tex2html521"
HREF="node4.html">
<IMG WIDTH="65" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="contents"
SRC="/usr/share/latex2html/icons/contents.png"></A>
<A NAME="tex2html522"
HREF="node58.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="/usr/share/latex2html/icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html524"
HREF="node33.html">Rewrite Systems and Functions</A>
<B> Up:</B> <A NAME="tex2html520"
HREF="node28.html">Cookbook</A>
<B> Previous:</B> <A NAME="tex2html514"
HREF="node31.html">Attribute Grammars</A>
<!--End of Navigation Panel-->
<ADDRESS>
<I></I>
<BR><I>2000-04-17</I>
</ADDRESS>
</BODY>
</HTML>
|
