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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
|
<!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>Rewrite Definitions</TITLE>
<META NAME="description" CONTENT="Rewrite Definitions">
<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="node13.html">
<LINK REL="previous" HREF="node11.html">
<LINK REL="up" HREF="node6.html">
<LINK REL="next" HREF="node13.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html271"
HREF="node13.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="/usr/share/latex2html/icons/next.png"></A>
<A NAME="tex2html267"
HREF="node6.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="/usr/share/latex2html/icons/up.png"></A>
<A NAME="tex2html261"
HREF="node11.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="/usr/share/latex2html/icons/prev.png"></A>
<A NAME="tex2html269"
HREF="node4.html">
<IMG WIDTH="65" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="contents"
SRC="/usr/share/latex2html/icons/contents.png"></A>
<A NAME="tex2html270"
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="tex2html272"
HREF="node13.html">Unparsing Definitions</A>
<B> Up:</B> <A NAME="tex2html268"
HREF="node6.html">Input</A>
<B> Previous:</B> <A NAME="tex2html262"
HREF="node11.html">Function Definitions</A>
<BR>
<BR>
<!--End of Navigation Panel-->
<H2><A NAME="SECTION00066000000000000000">
Rewrite Definitions</A>
</H2>
Functional languages are a convenient formalism for expressing functions
over trees.
Another convenient formalism is formed by <EM>rewrite rules</EM>[<A
HREF="node57.html#ehrig:act1">EM85</A>].
For instance, if we have a certain equivalence over terms, then rewrite
rules expressing this equivalence might define a procedure for computing a
normal form of a term.
Another use for term rewriting is as an alternative way of defining functions.
For example to implement the function `plus' on natural numbers one can
define `plus' as an operator and specify the rewrite rules such that the
normal form does not contain a plus.
The result of normalising (term rewriting) then is that the function is
`evaluated'.
(This is all abstract data type theory.)
The notation for term rewrite rules is very simple. For example:
<A NAME="320"> </A>
<PRE><HR><!--lgrindfile: rewrite_rule_general_example.k 12:19 Feb 19 1997-->
Neg(x) -> <: Minus(Zero(), x) >;
<HR></PRE>
In this example <I>x</I>
is a variable, used in the term in the right-hand side.
The meaning of this example is that every occurrence of the operator <I>Neg</I> is replaced
by an equivalent construct.
<P>
In general both sides are terms with variables, where all variables of the
right-hand side also appear on the left-hand side.
Actually, the left-hand side can be the same kind of pattern that is allowed in
function definitions.
To allow `greater control' (a euphemism for hacking...) we allow
arbitrary C functions and string- and int-denotations in the right-hand side (see below).
For the collection of rewrite rules, the system generates a function
<I>rewrite_</I><EM>phylum</EM>
for each phylum, which has the normalised form as its result.
This function can be called in the same way as any other function.
<P>
The rewrite functions have an additional argument of type <I>rview</I>.
Rewrite views can be used to group rewrite rules in separate rewrite systems.
Rewrite rules can be made specific for a set of rewrite
<EM>views</EM><A NAME="328"> </A><A NAME="329"> </A>
(or, added to one or more rewrite systems) by naming
these views between the angle open bracket and the colon of a rewrite rule.
For example:
<PRE><HR><!--lgrindfile: rewrite_views_example.k 12:21 Feb 19 1997-->
Neg(x) -> < view1 view2: Minus(Zero(), x) >;
<HR></PRE>
An omitted view list defaults to all rewrite views.
If no views are specified, the angle brackets and colon may be omitted
(as we usually do),
as we show below for the rewrite rule for <I>Neg(x)</I> that we gave above.
<A NAME="332"> </A>
<PRE><HR><!--lgrindfile: rewrite_rule_example.k 15:00 Sep 28 1992-->
Neg(x) -> Minus(Zero(), x);
<HR></PRE>
This is equivalent to a view list that only contains the view name <I>base_rview</I>.
The type <I>rview</I> is an enumeration type of all view names occurring in the rewrite rules.
It always contains the view name <I>base_rview</I>.
<P>
Rewrite views can be declared as in the following example:<A NAME="337"> </A><A NAME="338"> </A>
<PRE><HR><!--lgrindfile: rewrite_view_declaration_example.k 14:55 Feb 19 1997-->
%rview view1 view2; <I>/* the `%' is part of the keyword */</I>
<HR></PRE>
Rewrite views should be declared.
If the termprocessor input contains one or more rewrite view declarations it
will report errors for all rewrite views that are used and not declared.
The use of view declarations may help to find typing errors in view names -
in term processor input that does not contain view declarations, the misspelling
of a view name may just introduce a new view (with the misspelled name).
<P>
If several rewrite rules share the same left-hand side,
they may be combined by grouping the right-hand sides
(with seperating commas),
provided that all the angle brackets haven't been omitted from the right-hand sides.
If several rewrite rules share the same right-hand side,
they may be combined by grouping the left-hand sides
(with seperating commas).
The general form of a rewrite rule is shown below:
<PRE><HR><!--lgrindfile: rewrite_rule_general.k 12:33 Feb 19 1997-->
pattern1, pattern2, ... -> < v1 v2 ... : ... >, ..., < vn ... : ... > ;
<HR></PRE>
<P>
How we can prove that a rewrite system always yields a normal form
is beyond the scope of this
manual, but informally stated, each rule should bring the term `closer' to
its normal form, and the order in which the rules are
applied (the <EM>rewrite strategy</EM>)<A NAME="342"> </A> should not matter.
Two simple warnings: never ever use a rule in which the right-hand side
is equal to the left-hand side, or a rule that directly expresses a
commutative property.
<P>
The default rewrite strategy is leftmost innermost.
In the case of overlapping patterns<A NAME="343"> </A>, where more than one left-hand side matches,
the <EM>most</EM> specific match is taken.
<P>
Rewrite rules with functional right-hand sides are a bit harder to prove correct.
The first requirement of course is that the arguments and the results
of those functions should have the correct types,
which <I>lint</I> can check.
The second requirement is that the rule is meaningful,
but that is hard to check automatically.
The writer of such rules should convince herself of the correctness
of the rewrite rules.
Here we give some considerations that can be used in doing so.
The `purpose' of a rewrite system is to convert a term to its
<EM>normal form</EM>.
Now let us look closer at a rule with a function in it:
<PRE><HR><!--lgrindfile: rewrite_rule_function_example.k 15:00 Sep 28 1992-->
Operator(x) -> Function(x);
<HR></PRE>
The rewrite system uses this rule when it has a subterm that matches
the left-hand side, and `assumes' that substituting it by the right-hand
side brings it closer to the normal form.
It then continues applying rules on the new term.
The function <I>Function</I> should therefore bring the
expression closer to the normal
form.
Now what about the argument <I>x</I> of <I>Function</I>?
It is not known whether or not it is in normal form already (although the
default strategy, which is leftmost innermost, does guarantee this).
Therefore, <I>Function</I> cannot assume that its argument
is in normal form.
This is not usually a problem, but if it is, the function
<I>rewrite_</I><EM>phylum</EM> can be used in the function definition to guarantee this.
The other side of the picture is that the <EM>result</EM> of <I>Function</I>
does not have to be in normal form, which is convenient for the writer of <I>Function</I>.
<P>
<HR>
<!--Navigation Panel-->
<A NAME="tex2html271"
HREF="node13.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="/usr/share/latex2html/icons/next.png"></A>
<A NAME="tex2html267"
HREF="node6.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="/usr/share/latex2html/icons/up.png"></A>
<A NAME="tex2html261"
HREF="node11.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="/usr/share/latex2html/icons/prev.png"></A>
<A NAME="tex2html269"
HREF="node4.html">
<IMG WIDTH="65" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="contents"
SRC="/usr/share/latex2html/icons/contents.png"></A>
<A NAME="tex2html270"
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="tex2html272"
HREF="node13.html">Unparsing Definitions</A>
<B> Up:</B> <A NAME="tex2html268"
HREF="node6.html">Input</A>
<B> Previous:</B> <A NAME="tex2html262"
HREF="node11.html">Function Definitions</A>
<!--End of Navigation Panel-->
<ADDRESS>
<I></I>
<BR><I>2000-04-17</I>
</ADDRESS>
</BODY>
</HTML>
|
