f8a62d39250e58a33db9285651a4b65faf51a930
[nofib.git] / real / rx / doc / rxuser.lit
1 \chapter{$RX$ User Manual} %%%%%%%%%%%%%%%%%%%%%%%%%%
2 \label{chapter:rxuser}
3 \label{chap:rxuser}
4
5 \section{Introduction}
6 This chapter describes the program $RX$, 
7 written within the framework of this thesis.
8 $RX$ handles rational tree languages in term algebras with
9 arbitrary signatures. $RX$ performs the usual operations on
10 rational languages. 
11
12 $RX$ has been used to guess, and later verify,
13 a lot of the relations between languages that are used in the
14 decision procedure for $CL S$,
15 and the grammar for normalizing terms,
16 given in chapters \ref{chapter:termin} and \ref{chap:predN}
17 of this thesis.
18
19 Furthermore, $RX$'s input and output behaviour can be customized so
20 that it integrates smoothly with a typesetting system, much in the
21 spirit of a \emph{literate programming} tool.  $RX$ input may be
22 contained in a text document, and $RX$ output may be embedded in such
23 a document.  Additionally, $RX$ output can contain formatting
24 instructions to the typesetter.  In fact $RX$ is used to format the
25 very thesis you are now reading.
26
27 \newpage
28 \section{$RX$ internals} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
29
30 $RX$ internally represents rational tree languages by
31 finite tree automata. They can be non-deterministic
32 (bottom-up or top-down) or deterministic (bottom-up).
33
34 For details of the underlying theory, see chapter \ref{chapter:rxtheory}.
35
36 The external form, used for input and output,
37 is a non-deterministic top-down automaton
38 that could also be called a rational grammar.
39
40
41 %% \section{$RX$ implementation} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
42 \medskip
43
44 $RX$ is written entirely in the pure, lazy functional programming
45 language Haskell. It uses Haskell-1.3 features. $RX$ is known to
46 work with these compilers/interpreters: hugs, ghc-2.02, hbc-0.9999.4.
47 It does not depend on compiler-specific extensions or libraries.
48
49 $RX$ uses publically available libraries for
50 \begin{enumerate}
51 \item Finite Maps and Sets
52 \item Parsing
53 \item Pretty Printing
54 \end{enumerate}
55 (Copies of these are included with the $RX$ source code distribution.)
56 These libraries helped me a lot when programming $RX$,
57 as they provide tried and tested and optimized solutions for standard tasks,
58 and allowed me to focus on finite automata programming.
59
60 %% \section{$RX$ availability} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
61
62 \medskip
63
64 The source code of $RX$, and some additional information,
65 is available under terms of the GNU public license
66 \index{GNU}
67 from \verb+http://www5.informatik.uni-jena.de/~joe/rx/+.
68
69
70 \newpage
71 \section{$RX$ syntax} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72
73 $RX$ lexically and syntactically borrows 
74 from the Haskell programming language.
75
76 \subsection*{$RX$ lexic}
77
78 $RX$ code consists of lines of characters.
79
80 The input may contain comments. A comment extends from 
81 \verb+--+ to the end of the line, or it is enclosed in
82 between \verb+{-+ and \verb+-}+.
83
84 $RX$ has these lexical tokens:
85 \begin{enumerate}
86 \item number (a sequence of digits)
87 \item name (an alphabetic character, 
88   followed by a sequence of alphanumeric characters)
89 \item operator (a sequence of non-alphanumeric non-blank characters)
90 \item string (enclosed in double quotes)
91 \item group symbols 
92   \verb+(+, \verb+)+, \verb+[+, \verb+]+, \verb+{+, \verb+}+
93 \item group separator \verb+,+ (comma).
94   Note that \verb+;+ (semi-colon) is not a separator but an operator.
95 \end{enumerate}
96 The names \verb+arity+ and \verb+form+ are reserved.
97
98 A name may contain characters \verb+"_"+, \verb+"^"+, and \verb+"'"+,
99 and they'll have their expected interpretation when
100 the output is embedded in a \LaTeX\ document.
101
102 Names and operators together are called \emph{identifiers}.
103
104 A name enclosed in back-quotes behaves as if it were an operator.
105 From now on, \emph{operator} encompasses that meaning.
106
107 An operator enclosed in parentheses behaves as if it were a name.
108 From now on, \emph{name} encompasses that meaning.
109
110 %%% \newpage
111 \subsection*{$RX$ syntax}
112
113 $RX$ code is a sequence of \emph{declarations} and \emph{expressions}.
114
115 A \emph{declaration} declares one of these things:
116 \begin{enumerate}
117 \item
118   the form of an identifier (see below),
119 \item
120   the arity (number of required arguments) of names.
121
122   Example: \verb+arity 2 power, times+
123 \item
124   the precedence and associativity of operators.
125   
126   Example:
127 \begin{verbatim}
128 infixl 7 *
129 infixl 5 +
130 \end{verbatim}
131 \end{enumerate}
132
133 An \emph{expression} is a sequence of \emph{clauses}
134 separated by operators.
135
136 A \emph{clause} is a name followed by a sequence of \emph{atoms}.
137
138 An \emph{atom} is a name or a \emph{group}.
139
140 A \emph{group} is a sequence of expressions,
141 separated by group separators, enclosed in group symbols.
142 The group \verb+(x)+, where \verb+x+ is an expression,
143 is semantically equivalent to \verb+x+ alone.
144
145 \subsection*{$RX$ special syntax}
146
147 In $RX$, there is no partial application and there are no
148 higher order functions. In a function application, the function
149 must get exactly the number of arguments that its arity requires.
150
151 Arities that have not been explicitly declared (see above)
152 are implicitly set to 0 for names and 2 for operators.
153
154 This is more restrictive that Haskell but it allows for 
155 a nice shorthand notation: the operator \verb+@+ (called \emph{apply})
156 is implicitly inserted whenever a function has \emph{more}
157 arguments than necessary. Let \verb+f+ have arity 2,
158 then \verb+f x y b c+ is parsed as \verb+((f x y) @ b) @ c+.
159 This corresponds to the convention used in combinatory logic 
160 and lambda calculus.
161
162 This behavior can be controlled 
163 by the switch \verb+implicit+ and by the option \verb+apply+.
164 If \verb+implicit+ is \verb+on+,
165 then the binary operator that is the value of the option \verb+apply+
166 is inserted. Normally, this is \verb+@+.
167
168
169 \newpage
170 \section{$RX$ semantics}
171
172 In $RX$, the semantics of each identifier is a function from
173 state \(\times\) sequences of values to 
174 state \(\times\) values. The length of the sequence
175 is the arity of the identifier. 
176
177 Currently, the values are finite tree automata,
178 but this could be extended to a wider range of types.
179
180 The state is just the mapping
181 from identifiers to their meaning (semantics).
182 The pair (identifier, meaning) is called binding.
183
184 The state map can be extended by new bindings, 
185 but existing meanings cannot be overridden.
186
187 The operator \verb+=+ adds a new binding.
188 Examples:
189 \begin{verbatim}
190 q = 0
191 f a b = a + b * b
192 \end{verbatim}
193 If the arity of the bound identifier is 0 (a constant declaration), 
194 then the value of the whole expression is that of the right hand side.
195 If the arity is more than 0 (a function definition),
196 then the value of the whole expression is undefined.
197
198 The operator \verb+;+ combines the evaluation of two expressions
199 sequentially.
200 In \verb+a; b+, first \verb+a+ is evaluated, 
201 then \verb+b+ is evaluated in the state that resulted from the
202 evaluation of \verb+a+. The value of \verb+b+ is the
203 final result.
204
205 \subsection*{$RX$ special semantics}
206
207 So far, the description does not contain any hint on the range of values
208 that $RX$ operates on. This modularity is intentional, and could
209 be explored when extending $RX$ or re-using parts of it for other
210 purposes.
211
212 But we are going to use $RX$ for tree automata. The will be input and
213 output as rational tree grammars. 
214
215 First we need to specify the term algebra we're working in.
216 This happens implicitly.
217
218 Each expression has a term algebra associated with it
219 that consists of the \emph{constructors} that happen to be contained
220 in the expression's value. 
221
222 A \emph{constructor} is an identifier that is not bound.
223
224 Example:
225 \begin{verbatim}
226 arity 0 S
227 infixl 60 @
228 \end{verbatim}
229 This declares two constructors, one nullary, one binary.
230
231
232 A grammar is built by the
233 name \verb+grammar+ that gets two arguments: a start expression and
234 a set of rules. Example:
235
236 \begin{verbatim}
237 grammar x { x -> S, x -> S x + S x x }
238 \end{verbatim}
239 Remember that this is in fact \verb,x -> S @ x + (S @ x) @ x,
240 by the rule of implicit application.
241
242 Each rule has a variable on the left 
243 and an \emph{rule expression} on the right.
244 The start expression of the grammar also is an \emph{rule expression}.
245
246 A \emph{rule expression} looks like an expression (see above) but
247 there are restrictions on where grammar variables might occur:
248 Starting from the top of the syntax tree of a rule expression, on the
249 path to any grammar variable contained therein, only constructors and
250 \verb-++- operators are allowed. In branches of rule expressions where
251 no grammar variables occur, arbitrary expressions are permitted.
252
253 Note that \verb+grammar+ does not evaluate its arguments.
254 Rather, it behaves like a LISP special form that gets to see
255 the syntax tree of its argument.
256
257 \subsection*{$RX$ predefined identifiers}
258
259 There are predefined operators for rational languages:
260 \begin{enumerate}
261 \item \verb,++, union
262 \item \verb,\\, difference
263 \item \verb,&, intersection
264 \end{enumerate}
265
266 and predefined functions that only transform a language's representation,
267 but keep its meaning (the set of its words).
268 \begin{enumerate}
269 \item \verb,unify,:
270   unify seemingly identical states in the automaton
271 \item \verb,useful,
272   only keep reachable and productive states
273 \item \verb,det,
274   make automaton deterministic
275 \item \verb,min,
276   make automaton deterministic and then minimal
277 \end{enumerate}
278
279 \subsection*{Evaluation of expressions} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
280
281 If the switch \verb,eval, is \verb,on,, each expression is
282 evaluated and the evaluation may result in state changes
283 (because new bindings were added).
284
285 However, if evaluating an inline expression changes the current $RX$ state,
286 this change is not promoted to other code blocks or snippets.
287
288 That is, assignments cannot be hidden inside the text.
289 Rather, they must be made visible in code blocks.
290 (You can still cheat there, by turning the output off, see below.)
291
292 If the switch \verb,exp, is \verb,on,, the input expression is printed.
293 For normal typesetting, you would 
294 \begin{verbatim}
295  .set (eval=off,exp=on)
296 \end{verbatim}
297
298 If the switch \verb,res, is \verb,on,, the result of
299 evaluating the input is printed. (If evaluation took place at all.)
300
301 \subsection*{Preprocessing} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
302
303 The switches \verb+unify,useful,det,min+ tell whether the so named
304 functions should be automatically inserted on top of all expressions
305 that are being evaluated. In bindings, this refers to expressions
306 right of the \verb,=,.
307
308 The switch \verb,expand, tells whether the input expansion
309 is shown or hidden.
310
311
312 \subsection*{Postprocessing} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
313
314 The result of an evaluation is a finite tree automaton.
315 It is shown as a rational grammar. There are switches that
316 control the appearance of that grammar.
317 \begin{enumerate}
318 \item \verb,foldconst,
319   rules \verb,x -> e, where \verb,e, does not contain grammar
320   variables, are applied to all other rules, and the deleted.
321 \item \verb,foldnonrec,
322   rules \verb,x -> e, where \verb,e, does not contain \verb,x,,
323   are applied to all other rules, and the deleted.
324 \item \verb,hidegrammar,
325   if the rule set is empty, don't say \verb,grammar x {},.
326   Rather, use \verb,x, instead.
327 \end{enumerate}
328
329
330 \newpage
331 \section{Controlling $RX$'s behaviour} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
332
333 In addition to the core language, $RX$ has means for preprocessing
334 its input, and specifying aspects of its behaviour.
335
336 \subsection*{Options}
337
338 While processing input, $RX$ keeps a set of \emph{options}.
339
340 An \emph{option set} is a mapping from strings to strings.
341 It maps \emph{options} to \emph{values}.
342
343 A \emph{switch} is an option that only takes on values 
344 of \verb+on+ or \verb+off+.
345
346 Options can be set by \emph{directives}, or on the
347 command line when invoking $RX$.
348
349 A \emph{directive} starts with a dot as the very first character in a line.
350
351 Options can be set globally by
352 \begin{verbatim}
353  .set (opt1=val1, opt2=val2, ...)
354 \end{verbatim}
355 A \verb+.set+ is effective from where it stands to the end of
356 the file it is located in.
357
358 Option names and values can be given as $RX$ names or strings.
359
360 A value can also refer to another option's value by prepending
361 a dollar sign to it, as in 
362 .begin(keepsep="/")
363 \verb+.set (foo=$bar)+.
364 .end
365
366 Options can be set locally by
367 \begin{verbatim}
368  .begin (opt1=val1,...)
369     ...
370  .end
371 \end{verbatim}
372 The new option set is effective only in between \verb+.begin+
373 and \verb+.end+.
374
375 \subsection*{Default values for options}
376
377 The file \verb,Defaults.hs, from the $RX$ source distribution
378 contains the option set that is compiled in. All of those
379 options can be changed, however.
380
381 \subsection*{Importing files}
382
383 $RX$ input can be split over several files. The \verb+.import+
384 directive includes the contents of a file into the input stream.
385 \begin{verbatim}
386  .import file
387 \end{verbatim}
388 \verb+file+ must be the file's complete name as an $RX$ string.
389
390 The string \verb+"-"+, when used as a file name,
391 means the standard input stream. This is only really useful
392 on the command line, see below.
393
394 It is possible to set some options that are only in effect while
395 the imported file is processed
396 \begin{verbatim}
397  .import (opt1=val1,...) file
398 \end{verbatim}
399
400 In any case, none of the possible \verb+.set+ commands in the
401 \emph{imported} file has an effect on the options in the \emph{importing} 
402 file.
403
404 \subsection*{$RX$ command line invocation}
405
406 When the $RX$ executable is invoked, it analyzes its command line,
407 takes appropriate actions, and writes its output to the standard
408 output stream, from where it may be redirected by other means.
409
410 On the command line, you may specify option values
411 and files to read. 
412
413 Example:
414 \begin{verbatim}
415 RX opt1=val1 opt2=val2 filea opt3=val3 fileb filec -
416 \end{verbatim}
417 is handled as
418 \begin{verbatim}
419  .set (opt1=val1)
420  .set (opt2=val2)
421  .import "filea"
422  .set (opt3=val3)
423  .import "fileb"
424  .import "filec"
425  .import "-"
426 \end{verbatim}
427 Note that the last line means ``read standard input''.
428
429 Additionally, $RX$ might understand options for its underlying runtime system.
430 They depend on the compiler that had been used when building $RX$.
431 A common idiom is
432 \begin{verbatim}
433 RX +RTS -H50M -RTS opt1=val1 ...
434 \end{verbatim}
435 telling the system to use lots of heap space.
436
437
438 \newpage
439 \section{Literate Programming} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
440
441 A literate document contains text and code.
442 From this, $RX$ generates a text document
443 that has  code expressions and possibly their values converted to
444 formatted text.
445
446 The switch \verb,output, says whether to generate any
447 output at all. Beware that even if this is off, 
448 imports, sets, and evaluations may take place.
449
450 $RX$ knows whether it is currently looking at text or code
451 by looking up the value of the option \verb,current,. So a typical
452 code block is
453 \begin{verbatim}
454  .begin(current=code)
455     ...
456  .end
457 \end{verbatim}
458 The physical lines inside such a block are glued together to
459 form logical lines that are fed into the $RX$ evaluator one by one.
460
461 A \emph{logical line} consists of one or more \emph{physical lines}.
462 Each physical line that starts with a non-blank character
463 begins a new logical line. Physical lines that start with a blank
464 character are called \emph{continuation lines}. They are appended
465 to the most recent logical line.
466
467 Each logical line must be a syntactically valid $RX$ expression.
468
469 Apart from code blocks, there may be code snippets contained
470 inside lines of text.
471
472 Example:
473 .begin(keepsep="/")
474 \begin{verbatim}
475   ... the expression $S Q1 Q0$ denotes ...
476 \end{verbatim}
477 .end
478
479 Such inline code must be a valid expression.
480 It is also sent to the $RX$ evaluator.
481
482 There are two variations of inline code. They differ in
483 whether the separator is omitted or kept.
484 Per default,
485 .begin(keepsep="/",omitsep="/")
486 \begin{verbatim}
487  .set (keepsep="$",omitsep="|")
488 \end{verbatim}
489 and \verb,$x$, will result in \verb,$y$,,
490 while \verb,|x|, will result in \verb,y,,
491 .end
492 where \verb,y, denotes the result of typesetting \verb,x,.
493
494 The default setting should prove reasonable,
495 and in fact $RX$ inline code mode can be seen 
496 as a replacement for \LaTeX's math mode.
497
498
499
500
501 \subsection*{Typesetting customization} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
502
503 $RX$ has two styles for typesetting its output:
504 \verb,plain, and \verb,latex,.
505
506 Both can be assigned independently to the options \verb,code,
507 and \verb,text,.
508
509 Example:
510 \begin{verbatim}
511  .set (text=latex,code=plain)
512 \end{verbatim}
513 tells $RX$ to use \verb+\verb+ for inline code
514 and the \verb+{verbatim}+ environment for code blocks.
515
516 You can assign a special \LaTeX\ expansion to $RX$ identifiers.
517 This will be used when \verb,code=latex,. It is achieved by
518 form declarations, of which there are two kinds:
519
520 A \emph{passive form} is just a string that gets printed instead
521 of the identifier's name. Example:
522 \begin{verbatim}
523  .begin(current=code,output=off)
524  form S = "\textbf{S}"
525  form (+) = "\cup"
526  .end
527 \end{verbatim}
528 Note that form declarations happen inside code, not text.
529
530 An \emph{active} form is a formatting macro that takes arguments.
531 Example:
532 \begin{verbatim}
533  .begin(current=code,output=off)
534  form (/) 2 = "\frac#1#2"
535  .end
536 \end{verbatim}
537
538 In the arguments of the operators, parentheses are inserted
539 so that the output is correctly parseable with the given operator 
540 precedences and associativities. 
541 This remains unaffected when a passive form is used for an operator.
542
543 When an active form is in effect, its arguments are typeset
544 for a very low precedence. So, there will be no outer parentheses,
545 because it is assumed that the form takes care of visual grouping.
546 For instance, \verb,4 / (1 + 3), will come out as \verb,\frac{4}{1 + 3},,
547 given the above declaration.
548
549 (As an aside, this idea of omitting some parentheses was already present
550 in the \texttt{smugweb} system \cite{waldmann:smugweb}.)
551
552 \subsection*{Typesetting trees}
553
554 As seen in this thesis, $RX$ can be conveniently used to read and
555 typeset trees. Reading is eased by the \emph{implicit apply} convention which
556 inserts \verb+@+ nodes.  These nodes can be visually typeset by giving
557 \verb+@+ an active form. In this paper we use \verb+tree.sty+
558 written by  Edward M. Reingold and Nachum Dershowitz
559 which in turn uses \PiCTeX.
560
561
562
563 \newpage
564 \section{$RX$ example} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
565 \label{sec:rxexample}
566
567 .set (code=plain,res=on)
568
569 .begin (current=code,output=off)
570 local contains, all, redex, normal, normal', t, x, y
571 arity 0 all, redex, normal, normal', t, x, y
572 arity 1 contains
573 .end
574
575 Here is some input that is used in the thesis itself.
576
577 First, describe the set of all $S$-terms.
578 .begin(current=code,eval=on)
579 all = grammar t { t -> S ++ t t }
580 .end
581 So $all$ is a constant whose value is an automaton that accepts
582 (produces) the set of all terms.
583
584 The set of all redexes obviously is
585 .begin(current=code,eval=on)
586 redex = S all all all
587 .end
588
589 Now we define a function with one argument.
590 .begin(current=code,eval=on)
591 contains x = grammar y { y -> x, y -> y all ++ all y }
592 .end
593
594
595 The argument is any language $x$, and the result 
596 is the language of all terms $y$ that contain $x$ as a subterm.
597
598 This allows to compute the set of normal forms.
599 .begin(current=code,eval=on)
600 normal = all \\ contains redex
601 .end
602
603 Finally, this could be compared to the representation
604 .begin(current=code,eval=on)
605 normal' = grammar t { t -> S, t -> S t, t -> S t t }
606 .end
607
608
609 .begin (current=code,output=off)
610 unlocal
611 .end