Download MONA Version 1.4 User Manual

MONA 1.4
7.9
Recursive types and WSRT
ws2s;
type Tree = RED(left: Tree, middle: List, right: Tree), BLUE(next: List);
type List = NULL(), GREEN(next: List);
universe u:Tree;
tree [u] x;
A formula is built from the usual boolean connectives, first-order and weak monadic secondorder quantifiers, and the special WSRT basic formulas:
type(t,E) which is true iff the the first-order term t denotes a node which is associated the
type E; and
variant(t,x,E,V ) which is true iff the tree denoted by the tree variable x at the position
denoted by t has type E and is labeled with the E variant V .
Second-order terms are built from second-order variables and the set operations union, intersection and difference, as in WS1S and WS2S. First-order terms are built from first-order
variables and the special WSRT functions:
tree root(x) which evaluates to the root of the tree denoted by x; and
succ(t,E,V ,C) which, provided that the first-order term t denotes a node of the E variant
V , evaluates to its C component (and is undefined otherwise).
Tree constants can be expressed using the second-order term construct
const tree(t,E,consttree)
where a consttree has the form V (consttree1 ,. . . ,consttree m ), V is a variant of E, and, recursively, there is a consttreei for each component of V .
Continuing the example above, consider the following extension:
tree_root(x)~=root(u);
var2 r;
all1 p:
p in r <=>
(variant(p,x,Tree,BLUE) &
variant(succ(p,Tree,BLUE,next),x,List,GREEN));
~empty(r);
First, it is stated that the root of x is not located at the root of u. Then, a second-order
variable r is declared. A position p is in the set denoted by r if and only if its x label is BLUE
and the next successor is GREEN for x. Finally, r is required to be non-empty.
For the full WSRT syntax, see Appendix A. This logic corresponds to the core of the
FIDO language [KS99] and is also reminiscent of the LISA language [ABP98]. It can be
reduced to WS2S and thus provides no more expressive power, but utilizing the guide, a more
efficient decision procedure is often possible.
Example output
When one or more recursive types have been declared, the output format of satisfying examples and counter-examples is essentially the same as the format of constant tree expressions.
For instance, MONA generates the following satisfying example for the program shown above:
49