September 3, 2007

Expander2 is a flexible multi-purpose workbench for interactive term rewriting, graph transformation, theorem proving, constraint solving, flow graph analysis and other procedures that build up proofs or computation sequences. Moreover, tailor-made interpreters display terms as two-dimensional structures ranging from trees and graphs to a variety of pictorial representations that include tables, matrices, alignments, partitions, fractals and various tree-like or rectangular graph layouts (see Widget interpreters). Proofs and computations performed with Expander2 follow the rules and the semantics of swinging types. Swinging types are based on many-sorted predicate logic and combine constructor-based types with destructor-based (e.g. state-based) ones. The former come as initial term models, the latter as final models consisting of context interpretations. Relation symbols are interpreted as least or greatest solutions of their respective axioms.

The user may interact with the system at three levels of decreasing control over proofs and computations. At the top level, rules like induction and coinduction are applied locally and step by step. At the medium level, goals are rewritten or narrowed, i.e. axioms are applied exhaustively and iteratively. At the bottom level, built-in rules (some of them executing Haskell programs) simplify, i.e. (partially) evaluate terms and formulas, and thus hide routine steps of a proof or computation (see Overview). Proofs are automatically translated into proof terms that can be evaluated and modified later. This allows one to design functional-logic programs as proof carrying code that a client can validate by running the proof term evaluator (proof checker).

Expander2 has been written in O'Haskell, an extension of Haskell with object-oriented features for reactive programming and a typed interface to Tcl/Tk. Besides a comfortable GUI the design goals of Expander2 were to integrate testing, proving and visualizing deductive methods, admit several degrees of interaction and keep the system open for extensions or adaptations of individual components to changing demands.

Send comments, bugs, etc. to Peter Padawitz. Any suggestions for improvements, extensions, applications or project proposals are welcome!


Overview Main commands Overall code structure Solver features
Solver state variables Built-in signature term/formula menu Mouse and key events
font menu transform-selection menu specification menu signature menu
axioms menu theorems menu substitution menu graph menu
parse buttons narrow/rewrite buttons simplify button paint buttons
Further buttons Grammar Axioms and theorems Derivations
Variables Simplifications Examples Widget interpreters
pict type menu Alignments and palindromes Dissections and partitions References

Main commands

A command followed by a letter in round brackets is executed when the corresponding key is pushed after the keyboard has been activated by placing the cursor over the entry resp. label field and pressing the left mouse button. The keys for add spec, apply clause, load text and save tree work if the entry field has been activated. The keys for parse up and parse down work if the text field has been activated. The keys for other commands work if the label field has been activated.
add map add spec from file (Return) apply for symbols
apply clause (a/b)
left to right (Left) - right to left (Right)
apply (axioms) in text field apply map
apply substitution apply to variable: build equations
build graph build list build Trans/TransL
build unifier call enumerator check proof term (c)
clear subtrees coinduction collapse
collapse levelwise coordinates copy
create Hoare invariant create induction hypotheses create subgoal invariant
decompose atom decrease current (Left) derive/stop
enclose/replace by text expand fixpoint induction
flatten (co-)Horn clause generalize heap numbers
height numbers hide/show Horn axioms for copredicates
increase current (Right) instantiate invert for symbols
label graph with Atoms label roots with entry load text from file (Up)
move up quantifiers (m) narrow/rewrite (n) negate for symbols
paint parse up (Up) parse down (Down)
polarities positions preorder numbers
redraw (z) remove entry&label remove from entry field
remove other trees re-add/remove spec remove subtrees
remove text rename replace by other sides
replace by tree of Solver1/2 reverse (r) save spec to file
save proof to file save proof term to file (p) save tree to file (Down)
save tree in eps format to file (i) shift subformulas set
show axioms for symbols (x) show changed show map
show node infos show sig simplify (s)
split/join store graph stretch conclusion
stretch premise subsume turn local def into function application
unify unify with tree of Solver1/2 use transitivity
<---/---> (Down/Up) +1/-1

Create two subdirectories of your home directory and call them Examples and Pics, respectively. The save commands of Expander2 store strings into files of Examples and graphs (in eps format) into files of Pics. If the directories do not exist, nothing is saved! A file parameter of add or load commands is looked up first in your Examples directory. If it is not found there, it is searched for in the synonymous system directory. Gif files used as widgets (see Widget interpreters) are also looked up in the Examples directory.


The main components of Expander2 are the solver, the painter, the simplifier, the enumerator and a recorder of proofs and computation sequences.

Fig. 1. Components of Expander2

The solver is accessed via a window for editing and displaying trees that represents a disjunction or conjunction of logical formulas or a sum of functional terms. A proper (non-singleton) sum results from a computation obtained by nondeterministic rewriting. The solver window has a canvas for the two-dimensional representation of the list of current trees (among which one browses by moving the slider below the window) and a text field for their string representation. With the parse buttons one switches between the tree (or graph) and the string representation. Both representations are editable. As the usual cut, copy and paste operate on substrings in the text field, so do corresponding mouse-triggered functions when the cursor is moved over subtrees on the canvas.

After a widget interpreter has been selected from the pict type menu, pushing the paint button opens a painter window and the pictorial representations of all interpretable subtrees of the solver's current trees will be shown. Pictures are lists of widgets that can be edited in the painter window and completed to widget graphs. Widgets are built up of path, polygon and turtle action constructors that admit the definition of a variety of pictorial representations ranging from tables and matrices via string alignments, piles and partitions to complex fractals generated by turtle systems [RS], which define a picture in terms of a sequence of actions that a turtle would perform when drawing the picture while moving over a canvas. The turtle works recursively in two ways: it maintains a stack of positions and orientations where it may return to, and it may give birth to subturtles, i.e. call other turtle systems. The solver and its associated painter are fully synchronized: the selection of a tree in the solver window is automatically translated to a selection of the tree's pictorial representation in the painter window and vice versa. Hence rewriting, narrowing and simplification steps can be carried out from either window.

The enumerator provides algorithms that enumerate trees or graphs and passes their results both to the solver and the painter. Currently, two algorithms are available: a generator of all sequence alignments [Gie,P01] satisfying constraints that are partly given by axioms, and a generator of all nested partitions of a list with a given length and satisfying constraints given by particular predicates. The painter displays an alignment in the way DNA sequences are usually visualized. A nested partition is displayed as the corresponding rectangular dissection of a square.

Expander2 allows the user to control proofs and computations at three levels of interaction.

At the high level, analytic or synthetic inference rules or other syntactic transformations are applied individually and locally to selected subtrees (see the transform-selection menu). The rules cover single axiom applications, substitution or unification steps, Noetherian, Hoare, subgoal or fixpoint induction and coinduction. Derivations are correct if, in the case of trees representing terms, their sum is equivalent to the sum of their sucessors or, in the case of trees representing formulas, their dis- resp. conjunction is implied by the dis- resp. conjunction of their successors. The underlying models are determined by built-in data types and the least/greatest interpretation of Horn/co-Horn axioms. Incorrect deduction steps are detected and cause a warning. All proper tree transformations are recorded, be they correct proofs or other transformations. Terms and formulas are built up from the symbols of the current signature (see Solver state variables). For more details on the syntax and semantics of axioms, theorems and goals, see Axioms and theorems and Swinging Types.

At the medium level, rewriting and narrowing realize the iterated and exhaustive application of all axioms for the defined functions, predicates and copredicates of the current signature. Terminating rewriting sequences end up with normal forms, i.e. terms consisting of constructors and variables. Terminating narrowing sequences end up with the formula True, False or solved formulas that represent solutions of the initial formula. Since the axioms are functional-logic programs in abstract logical syntax, rewriting and narrowing agree with program execution. Hence the medium level allows one to test such programs, while the inference rules of the high level provide a "tool box" for program verification. In the case of finite data sets, rewriting and narrowing is often sufficient even for program verification. Besides relations and deterministic functions, non-deterministic transition systems employing structured states, such as Maude programs [C] or algebraic nets [SMÖ], may also be axiomatized and verified by Expander2. The latter are executed by applying associative-commutative rewriting or narrowing on bag terms, i.e. multisets of terms.

At the low level, built-in Haskell functions simplify or (partially) evaluate terms and formulas and thereby hide most routine steps of proofs or computations. The functions comprise arithmetic, list, bag and set operations, term equivalence and inequivalence (that depend on the current signature's constructors) and logical simplifications that turn formulas into nested Gentzen clauses. Evaluating a function f at the medium level means narrowing upon the axioms for f, Evaluating f at the low level means running a built-in Haskell implementation of f. This allows one to test and debug algorithms and visualize their results. For instance, translators between different representations of Boolean functions were integrated into Expander2 in this way. In addition, an execution of an iterative algorithm can be split into its loop traversals such that intermediate results become visible, too. Currently, the computation steps of Gaussian equation solving, automata minimization [HMU], OBDD optimization, LR parsing, data flow analysis and global model checking can be carried out and displayed (see Simplifications).

Overall code structure

The code of Expander2 consists of four O'Haskell modules: The solver, painter and enumerator templates make use of the O'Haskell module Tk.hs that provides the interface to Tcl/Tk (see the O'Hugs computing environments).

Fig. 2. The solver window shows four axioms of a list specification.

Solver features

Viewed from top to bottom, a solver window consists of the following widgets:

Solver state variables

Built-in signature

            preds:      -> <= >= < > >> _ all any zipAll zipAny `disjoint` `in` `NOTin` null `shares` `subset` `NOTsubset`
                        Int Real
reduced INV ~/~ ~/~0 ~/~1 ~/~2 ...
            copreds:    ~ ~0 ~1 ~2 ...
            constructs: <+> () [] ^ {} : 0 from_to bool cond fun lin inj0 inj1 inj2 ... suc
            defuncts:   . ; + ++ - * ** / auto bag bisim blink concat count dnf drop foldl get0 get1 get2 ... head height
                        init iter last length map mapt max `meet` min minimize `mod` nerode obdd parse permute postflow
                        product reverse sat set shuffle stateflow subsflow sum tail take `then` tup upd0 upd1 upd2 ...
                        zip zipWith

            fovars:     i j x y z
-> denotes a (labelled or unlabelled) transition relation (see below). <=,>=,<,> are predefined on integers, reals, strings and the defined functions x_0,x_1,x_2,... (used as node labels of OBDDs; see below). `subset` and `in` denote the subset resp. membership relation on all collections, i.e. terms C(t1,...,tn) where C is one of the constructors [] or {} or C(t1,...,tn)=t1^...^tn. reduced checks whether its argument is a variable-free tree without defined functions.

Int(t) and Real(t) return True if t is an integer or real number, respectively. Int(t) and Real(t) return False if t is a real or an integer number, respectively. all(P)(as) return True if all elements of as satisfy P. any(P)(as) return True if as contains an element that satisfies P. zipAll(P)([a1,..,an])([b1,..,bn]) return True if for all 1 <= i <= n, (ai,bi) satisfies P. zipAny(P)([a1,..,an])([b1,..,bn]) return True if for some 1 <= i <= n, (ai,bi) satisfies P.

If n > 1, then length(t1,...,tn) simplifies to n. shuffle[ts] shuffles the lists of ts before concatenating them. height(t) simplifies to the height of t, regardless of the semantics of t.

Formulas involving >> or INV are generated whenever an induction hypothesis or a (Hoare or subgoal) invariant is created (see the transform-selection menu). For the use of the underline symbol, see enclose/replace by text.

Terms combined with the infix constructor <+> are called sum terms. Semantically, <+> is a set union resp. insertion operator. The simplifier transforms a term of the form f(...,t1<+>...<+>tn,...) into the sum f(...,t1,...)<+>...<+>f(...,tn,...).

$ denotes the apply operator whose first argument is a higher-order term t that represents a predicate or function f. The other arguments of $ are the arguments of f, i.e. $(t,t1,...,tn) stands for t(t1,...,tn).

Given terms p1,...,pn,c and a formula u,

            t = fun(p1,...,pn,bool(c)`then`u)

denotes a conditional λ-abstraction. The simplifier evaluates a corresponding application t(t1,...,tn) of t to (t1,...,tn) by matching (t1,...,tn) to (p1,...,pn), applying the unifier f to c and then to u provided that c[f] simplifies to True and (t1,...,tn) does not contain variables that are bound in t. Otherwise the simplification fails.

Given terms f1,...,fk, the application (f1;...;fk)(t1,...,tn) is simplified to fi(t1,...,tn) if i is the least m such that the simplification of fm(t1,...,tn) does nor fail.

tup(f1,...,fn)(t) is simplified to the list [f1(t),...,fn(t)]. Given a collector c, c(f1,...,fn)(t) is simplified to the collection c(f1(t),...,fn(t)).

A unary function f is applied repeatedly if a term of the form iter(f)(t) is simplified: n simplification steps transform this term into iter(f)(u) where u represents the value of f^n(t).

(), [] and {} denote tuple, list resp. set constructors of arbitrary finite arity. If () has no arguments, then () denotes "undefined" and is neutral with respect to the sum constructor <+>. A term of the form f((t1,...,tn)) is identified with f(t1,...,tn) provided that f is not a collector. Accordingly, for a variable x, f(x) unifies with f(t1,...,tn). The constructor : appends an element to a list from the left. 0 and suc are the natural number constructors. If applied to a number list s, suc returns the next permutation of s in reverse lexicographic order. In particular, if s is sorted, then suc(s)=reverse(s). The constructors inj0,inj1,inj2,... denote the first, second, third,... injection into a sum type. The simplifier decomposes (in)equations with the same leading constructor on both sides. The simplifier also replaces (in)equations with different leading constructors on both sides by False (True).

bool, cond and lin embed formulas into terms (see the Grammar).

+,-,*,**,/,`mod`,max,min are defined on integer and real numbers. +,-,*,/ work also for polynomials (* and / only as scalar operators).

Given finite lists or sets s,s' and integers i,k, s-s' and [i..k] denote the list of elements of s that are not in s' and the interval of integers from i to k, respectively. from_to is an internal constructor. For instance, the parser translates the string [t..u] to the term from_to(t,u), while the simplifier compiles from_to(t,u) to the corresponding interval if t and u have been evaluated to integers. Haskell shortcuts like [i,k..n] may also be used. ., ++, concat, drop, foldl, head, init, last, length, map, null, product, sum, tail, take, reverse, zip and zipWith are defined as the synonymous Haskell functions. Some functions on lists also apply to bags and sets.

any, all, map, foldl, zip, zipAny zipAll and zipWith also occur in LIST and LISTEVAL with (recursive) axioms. The synonymous built-in symbols are interpreted as partial non-recursive functions. For instance, a rewriting step via LIST transforms the term map(suc)(x:s) into x:map(suc)(s), while the simplifier does not modify this term, but would turn map(suc)[x,y,z] into [suc(x),suc(y),suc(z)]. Of course, axioms introduced for built-in symbols should comply with their built-in interpretation that is realized by the simplifier.

count(ts,t) counts the number of occurrences of t in the list ts. ts `disjoint` us checks whether the lists ts and us are disjoint. ts `meet` us computes the intersection of the lists ts and us. ts `shares` us checks whether the lists ts and us are not disjoint.

get0,get1,get2,... and upd0,upd1,upd2,... return resp. update the first, second, third,... component of a tuple or element of a collection.

bag transforms a list into a bag and flattens terms built up with the infix operator ^ (see below). set turns a list or bag into a set. Many functions defined on lists are also defined on other collections. For obvious semantical reasons, the simplifier applies count, `disjoint`, `in`, `meet`, `shares`, ++, - and <= only to variable-free terms without defined functions.

Fig. 3. A DNF (DNF5), its minimal OBDD and its Karnaugh diagram

obdd transforms a DNF represented as a list of strings of the same positive length whose characters are 0, 1 or # into an equivalent minimal OBDD. dnf transforms OBDDs into equivalent minimal DNFs. If applied to a DNF, minimize minimizes the number of summands of a DNF. If applied to an OBDD, minimize minimizes the number of nodes of an OBDD according to the two reduction rules for OBDDs [Bry].

^ is an infix operator for building bags and treated by the unification algorithm as an associative and commutative function. When a bag term t1^...^tn in the displayed tree is to be unified with another bag term u, then the unification succeeds even if only a permutation of t1^...^tn unifies with u. If there are several unifiers, those are preferred, which substitute only variables for variables. Among these unifiers those are preferred, which substitute variables only for variables of u.

Axioms of the form

          {guard ==>} (t1^...^tn -> u {<=== prem})           (*)

are called transitional axioms. (*) can be applied to a bag term t = u1^...^um if the list [t1,...,tn] unifies with a list [ui1,...,uin] of elements of t such that 1<=i1<... <=m, the unifier f satisfies guard and t is the left-hand side of a transitional atom t -> t'. This atom is then replaced by the instance of the formula

          (u^uk1^...^uk(m-n) = t' {& prem}

by f. If u = [v1,...,vk] for some k>1, then (*) is treated as a conjunction of the clauses

          {guard ==>} (t1^...^tn -> v1 {<=== prem})
          {guard ==>} (t1^...^tn -> vk {<=== prem})

Set brackets used in clauses enclose optional subformulas, i.e. guard and prem in axiom (*) may be empty.

If the application of (*) to t fails, the elements of t are permuted. If after 100 permutations (*) is still inapplicable, the last permutation of t will be returned as result - and yield a new starting point for further attempts to apply (*).

For instance, repeated applications of the AC rule

          i`mod`j = 0 ==> i^j -> j

(see PRIMS) to 2^3^4^5^6^7^8^9^10^11^12^13^14^15 sift out the primes and thus end up with 2^3^5^7^11^13.
ACCOUNT, BOTTLEAC, PUZZLE and the algebraic net specifications PHILAC and ECHOAC also contain AC rules.
Fig. 4. Snapshots of a run of the echo algorithm (cf. [SMÖ])

The symbols &,|,=,=/=,+,*,^,{},<+>,~,~0,~1,~2,...,~/~,~/~0,~/~1,~/~2,... are permutators, i.e. the order of their arguments is irrelevant. Consequently, AC unification replaces ordinary unification whenever the respective arguments of a permutator are to be unified.

The symbols ^,{},++ and <+> are treated as associative operators and thus may have an arbitrary finite number of arguments. {} and <+> are idempotent. [] is neutral with respect to ^,{} and ++. () is neutral with respect to <+>.

Actions,Atoms,Finals,FinalsL,Fix,Matrix,MatrixL,Perm,Trans and TransL denote state terms to be initialized by equational axioms and modified by simplifications (see also the narrow button).

~,~0,~1,~2,... are declared as copredicates and used as congruence relations. They are supposed to denote behavioral equalities. <,>,=/=,~/~,~/~0,~/~1,~/~2,... are the complements of >=,<=,=,~,~0,~1,~2,..., respectively. The simplifier replaces behavioral (in)equations with different leading injections or tuples of different length on both sides by False (True).

For each other predicate or copredicate P, notP denotes the complement of P. Axioms for the complement of P are added to the current axioms if P is entered into the entry field and the button negate axioms for symbol is pushed.

Subformulas involving built-in functions or predicates are (partially) evaluated when the displayed tree is simplified. This includes the stepwise execution of built-in functions with state term parameters (see Simplifications).

The declaration of a copredicate p overwrites preceding declarations of p as a predicate or constructor. The declaration of a predicate or defined function f overwrites preceding declarations of f as a constructor. The declaration of a defined function x overwrites preceding declarations of x as a first-order variable (like in OBDD).

For example, the signature OBDD reads as follows:

     defuncts: restrict forall exists quantor x X Y F and or not
     fovars:   u2 u1 u t2 t1 t j i b
     hovars:   F{and,or} X{x} Y{x}

F{and,or} denotes that the defined functions and and or are the only admissable instances of the higher-order variable F. In general, the list of strings following a higher-order variable F consists of symbols that are admissable for F. In addition to the symbols of the list, all higher-order variables are admissable for F. If F is not followed by a list of of strings, then all symbols of the current signature are admissable for F.

Keywords (specs:, preds:, copreds:, constructs:, defuncts:, fovars: and hovars:) may appear at any place in the list of symbols that builds up a signature. To be recognized as keywords they must be separated from their context by blanks. User-defined signatures automatically inherit the built-in signature. Symbols that are to be interpreted as infix operators must start and end with the character ` or consist of characters among 

     : + - * < = ~ > / ^ #

(see the language generated by infixToken in the Grammar). Symbols used in axioms, theorems or conjectures that do not belong to the current signature are interpreted as (undefined) function symbols (see the Grammar). This facilitates certain applications, but may also lead to unexpected unification failures when axioms or theorems are applied.

Mouse and key events

A subtree t is selected (or deselected if it has already been selected) by clicking on the left mouse button while placing the cursor over its root. If the mouse is moved while the button is pressed, t is shifted over the canvas. If the button is released while the root of t is placed over the root of another subtree u, u is replaced by t. If u is an existentially (resp. universally) quantified variable and the scope of u has positive (resp. negative) polarity, then all occurrences of u within the scope are replaced by t. Hence, in these cases, the replacement works like instantiate.

Subtrees are deselected backwards with respect to the order in which they were selected by moving the cursor away from the displayed tree and pushing the left mouse button. All selected subtrees are deselected simultaneously if the clear subtrees button is pushed. If you stop moving a subtree before inserting it into the displayed tree, it will stay at the place where you released the mouse button. Then push the redraw button and the subtree will be returned to its previous place within the displayed tree.

If a subtree t has been selected and the move of t is started with a click on the middle mouse button, t will be removed from the displayed tree and replaced by the variable zn where the index n is increased each time a subtree is removed or a new variable is needed when an axiom is flattened (see below). Moreover, the current substitution is extended by the assignment of t to zn.

By moving the mouse and pushing the middle button outside the root of a selected subtree the entire displayed tree is shifted over the canvas. By pressing the right mouse button while placing the cursor over a node x a pointer (edge) from x to the root of the last selected subtree t is drawn and all successors of x are removed. The arc is orange-colored if it closes a circle consisting of edges of t. Otherwise it is magenta-colored. Subtree replacements and substititutions for variables adapt the pointer values.

A command followed by a letter in round brackets is executed when the key with the letter is pressed after the cursor has been placed over the label field and the left mouse button has been pushed (see Commands).

term/formula menu

The commands of the term/formula menu create or transform the current trees or the current proof.

font menu

consists of buttons for choosing the font to be used for the text in tree nodes and pictorial term representations. The font size is controlled by a slider (see Solver features).

transform-selection menu

The commands of this menu transform the subtrees that were selected with the left mouse button. If no subtree has been selected, the entire displayed tree is regarded as being selected. Most commands call inference rules and deliver messages that tell us whether or not the executed rule application is sound with respect to the initial model induced by the current signature and axioms (see Derivations). For each predicate, copredicate or function p, let AX(p) be the set of axioms for p.

specification menu

signature menu

axioms menu

theorems menu

graph menu

substitution menu

parse buttons

parse up parses the string in the text field according to the grammar given below, initializes the list of current trees and the tree mode and displays the first element of the list on the canvas. Term graphs are implemented as objects of the instance Term String of the Haskell type

     data Term a = V a | F a [Term a] | Actions (STATE -> String -> ActLR) | Atoms [String] (String -> [STATE]) |
                   Dissect [(Int,Int,Int,Int)] | Finals (STATE -> Bool) | FinalsL (STATE -> String -> Bool) |
                   Fix [[Int]] | MatchFailureC (Term a) | Matrix [STATE] (STATE -> STATE -> [(STATE,STATE)]) |
                   MatrixL [STATE] (STATE -> STATE -> [([STATE],[STATE])]) | Trans [STATE] (STATE -> [STATE]) |
                   TransL [STATE] [String] (STATE -> String -> [STATE])
     type STATE = String

The constructor V encapsulates first-order variables, F encloses logical and non-logical function symbols and higher-order variables. The other constructors are called state constructors and will be explained later (see Simplifications).

parse up expects a term or formula built up of logical operators, signature symbols and further strings that are regarded as function symbols and displays its tree representation on the canvas. If the term resp. formula splits into numbered subexpressions, then only the ones whose numbers are listed in the entry field will be combined by <+> resp. & and displayed.

Given natural numbers n1,..,nk, strings of the form pos n1 .. nk are interpreted as pointers (see above). Only first-order variables and pointers are turned into objects built up with the constructor V. Subtrees whose root starts with the character @ are not displayed.

parse down computes the textual representation of the displayed tree resp. selected subtrees, connects them with the symbol in the entry field and writes the result into the text field provided that all selected subtrees are either terms or formulas.

narrow/rewrite buttons

By repeatedly pushing the unlabelled button right of the match/unify button narrowing resp. rewriting steps are performed on (selected) trees in a depth-first order until,

In cases (5) and (6), subterms are modified only if they match against unconditional equations. By pressing the match/unify button one changes between the (default) match mode, the unify mode and greedy versions of these modes that determine whether a potential redex is matched or unified against an axiom. The unify modes admit the instantiation of redex variables by non-variables, the match modes do not. Rewriting can only be performed in a match mode. Usually, all applicable axioms are applied in parallel and each solution of the guard of an applicable axiom leads to a reduct. In a greedy mode, only one - randomly selected - applicable axiom is applied, but, as in a non-greedy mode, different solutions of the guard of this axiom lead to several reducts.

Narrowing upon a predicate or copredicate p generalizes linear resolution to the simultaneous application of all axioms for p. Narrowing also generalizes rewriting from terms to formulas and admits the instantiation of redex variables by non-variable terms. These substitutions are supposed to build up solutions of the formula at the beginning of a narrowing sequence. Since each narrowing step applies the definition (axioms) of a predicate, copredicate or defined function, we have also used the term unfolding for narrowing steps [P00].

Applying all applicable (Horn) axioms for a predicate p or a defined function f simultaneously results in the replacement of the redex by the disjunction of their premises and equations representing the computed unifiers. Applying all applicable (co-Horn) axioms for a copredicate p simultaneously results in the replacement of the redex by the conjunction of their conclusions. Some equational or transitional axioms may be only partially unifiable with the redex. These are applied as well, but contribute to the reduct not with their premises resp. conclusions, but with equations representing the partial unifiers. This extension is called needed narrowing [AEH,P96] and ensures that the iteration of narrowing steps proceeding from supertrees to subtrees leads to all solutions of the current trees (see NEED).

A rewriting or narrowing step consists in the simultaneous application of all axioms for the outermost predicate, copredicate or defined function of the maximal subtree to which some axiom applies (if rules is empty) or some clause of rules applies (if rules is nonempty).

In cases (1), (3), (4), (5) and (6), reducts are simplified iff simplifyBit is set to True and simplified and refuted iff removeBit and simplifyBit are set to True (see Solver state variables).

simplify button

simplify performs simplification steps on (selected) trees from top to bottom and, on each level, from left to right, until,

paint buttons

Fig. 6. The painter window shows the ten solutions of queens(5,ps)
obtained from applying axioms of QUEENS.

Pictorial term representations consist of widgets. A list of widgets is called a picture. A picture becomes a widget graph if some of its widgets are connected by directed arcs. Widgets comprise circles, paths, polygons, text entries, node-labelled trees, and sequences of turtle actions that admit the hierarchical construction of pictures insofar as the drawing of a picture (without arcs) is also a turtle action.

The actual widget interpreter is selected from the pict type menu. Some built-in axiom files (see Examples) and enumerators are automatically associated with a widget interpreter.

paint fast/slow opens a Painter window with the background color entered in the solver's entry field (see the Grammar; white is the default color) that consists of the following widgets:

The commands for creating and editing widget graphs are summarized in Figures 20 and 21 (see Widget interpreters).

If subtrees have been selected, paint combines the pictorial representations of all representable selected subtrees and displays the resulting picture on the canvas. Using the middle mouse button, the individual widgets, which are usually displayed on top of each other, can be pulled from each other horizontally or vertically.

If no subtrees have been selected, then for each element t of the list of current trees, paint combines the pictorial representations of all maximal representable subtrees of t. The resulting picture that corresponds to the tree displayed on the solver canvas is drawn on the painter canvas, while the pictures derived from other elements of the list of current trees are assigned to other positions in the list of current pictures. One may browse among the pictures by moving the graph selecting slider (see above). Expander2 provides several widget interpreters and combinators thereof. The actual one depends on the current axioms, but can also be set by selecting from the pict type menu. For instance, Fig. 7 shows solutions of the formula

      Any pa: (loop((0,0),path[],pa) & turt(pa:place(circ(2,red),[(2,6),(6,2)])) = z)

in ss obtained by applying axioms of robot, were generated by the interpreter polygon solution that looks for solved formulas and applies the interpreter polygon to the solving terms in these formulas. A solved formula looks as follows:

      Any Z1:x1=t1 &...& Any Zk:xk=tk & All Z(k+1):x(k+1)=/=t(k+1) &...& All Zn:xn=/=tn.

x1,...,xn are different free variables, t1,...,tn are normal forms and the transitive closure of {(i,j)|ti contains xj} is acyclic.

Fig. 7. Pictorial representations of solutions obtained by applying axioms of robot

Further buttons


according to which parse up translates a string in the text field into a term or formula. Bold symbols are terminal.
 implication ---> disjunct ==> disjunct | disjunct <==> disjunct | disjunct ===> disjunct | disjunct <=== disjunct

disjunct ---> conjunct | conjunct | disjunct

conjunct ---> enclosedFactor | enclosedFactor & conjunct

enclosedFactor ---> (implication) | factor

factor ---> True | False | Not enclosedFactor | Any vars : enclosedFactor |

vars : enclosedFactor | infixAtom | prefixAtom | singleTerm^singleTerm moreBag

vars ---> var | var vars

var ---> noBlanks noBlanks must derive to a first- or higher-order variable.

infixAtom ---> term infixToken term infixToken must derive to =, =/= or a predicate or copredicate.

prefixAtom ---> noBlanks | noBlanks must derive to a first-order variable.

noBlanks atomrest | noBlanks must derive to =, =/=, a predicate or a copredicate.

(infixRelTerm) someTerms | (infixRelTerm)

atomrest ---> (relTerms) someTerms | enclosedTerms manyTerms

someTerms ---> (relTerms) someTerms | enclosedTerms someTerms | enclosedTerms

relTerms ---> relTerm | relTerm , relTerms

relTerm ---> prefixRelTerm | infixRelTerm | term

prefixRelTerm ---> preRelChars | preRelChars (relTerms) |

preRelChars must derive to =, =/=, a predicate or a copredicate.

infixRelTerm ---> (enclosedRelTerm infixToken enclosedRelTerm)

infixToken must derive to a constructor or a defined function.

enclosedRelTerm ---> (relTerm) | prefixRelTerm

enclosedTerms ---> (terms) | list | set | (infixFun)

terms ---> term | term , terms | term .. terms

term ---> bagTerm | bagTerm <+> term

bagTerm ---> singleTerm moreInfix | singleTerm moreInfix ^ bagTerm

moreInfix ---> + singleTerm moreInfix | - singleTerm moreInfix | infixFunR bagTerm | empty

+ and - are left-associative.

infixFun ---> infixToken infixToken must derive to a constructor or a defined function.

infixFunR ---> infixFun

infixFun must derive to a right-associative function, but not to +, -, ^ or <+>.

singleTerm ---> list | set | boolTerm | int | int curryrest | double | string | fovar | #dddddd |

RGB int int int | pos treepos | -singleTerm | () | (term) curryrest |

enclosedTerms | noDelims | noDelims curryrest

noDelims must not derive to =, =/=, a logical symbol, a predicate (except for _),

a copredicate (except for _) or a first-order variable.

curryrest ---> enclosedTerms curryrest | empty

boolTerm ---> bool(implication) | cond(implication,terms) | lin(conjunct)

list ---> [] | [terms]

set ---> {} | {terms}

int ---> any constant of Haskell type Int

double ---> any constant of Haskell type Double

string ---> any string

fovar ---> noBlanks noBlanks must derive to a first-order variable.

treepos ---> any finite list of natural numbers separated by blanks

infixChars ---> any string that consists of characters among . ; : + - * < = ~ > / \ ^ #

infixWord ---> `any string that does not contain back quotes`

infixToken ---> infixChars | infixWord | ~k | ~/~k for all natural numbers k

noDelims ---> any string that does not contain a character among

( ) [ ] { } , ` | & . ; : + - * < = ~ > / ^ # \t \n

noBlanks ---> any string that neither contains a blank or a character among


relChars ---> any string that neither contains a blank nor a character among ( ) , \t \n


noDelims need not derive to a symbol of the current signature. Any string derived from noDelims is turned into a node with the Term constructor F (see the parse buttons). Moreover, noDelims may derive to a string with blanks. This permits the use of symbols consisting of several words separated by blanks.

Integers, reals and (quoted) strings are automatically interpreted as (not always nullary!) constructors. This admits, for instance, the use of natural numbers in the tree representations of nested partitions (see Dissections and partitions).

An important technical reason for declaring a function symbol as a defined function is the fact that the outermost non-equational symbol of each axiom must be a predicate, a copredicate or a defined function.

Newline characters followed by a dot must be avoided because this because such a string is interpreted in a particular way. When a line with more than 120 characters is entered into the text field, it is split into several lines each of which starts with a dot. This ensures that decomposed lines are recognized as single ones when the contents of the text field is parsed.

Line suffixes starting with -- are regarded as comments.

If the prefix x of a string x_y is parsed into a color c according to the following grammar, then x_y will be displayed on the canvas of a solver as a c-colored y.

The color grammar:

      color ---> light color | dark color | RGB int int int | #dddddd
      color ---> black | grey | white | red | magenta
      color ---> blue | cyan | green | yellow | orange
      int   ---> any constant of Haskell type Int

Axioms and theorems

Axioms and theorems to be applied with apply clause must have a stretchable premise or conclusion or must be
Horn clauses:              
      (1) {guard ==>} (f(t1,..,tn)) = u {<=== prem})

      (2) {guard ==>} (p(t1,..,tn) {<=== prem})

      (3) t = u {<=== prem}
      (4) q(t1,..,tn) {<=== prem}
co-Horn clauses
      (5) {guard ==>} (q(t1,..,tn) ===> conc)

      (6) t = u ===> conc

      (7) p(t1,..,tn) ===> conc

distributed Horn clauses:
      (8) at1 | ... | atn {<=== prem}

      (9) at1 & ... & atn {<=== prem}
distributed co-Horn clauses:
      (10) at1 | ... | atn ===> conc

      (11) at1 & ... & atn ===> conc

f, p and q denote a defined function, a predicate and a copredicate, respectively, of the current signature. If the current trees are terms, then the reducts must be terms and thus only premise-free clauses of the form (1) can be applied.

A clause with a guard is applied only if the guard is solvable. The solution becomes part of the unifier that is generated when the clause is applied. For instance, the axiom

 split(s) = (s1,s2) ==> sort(x:(y:s)) = merge(sort(x:s1),sort(y:s2)),

for sort (see LISTEVAL) is guarded, while the logically equivalent axiom
 sort(x:(y:s)) = merge(sort(x:s1),sort(y:s2)) <=== split(s) = (s1,s2)

(see LIST) is unguarded. On the one hand, guarded axioms are needed for evaluating ground terms efficiently. On the other hand, axioms and theorems used as lemmas in step-by-step derivations (see below) must be unguarded. Otherwise the search for a solution of the guard may block the derivation process.

Narrowing is used for solving guards. In order to ensure termination, at most 100 narrowing steps, each of which followed by at most 100 simplification steps, are performed for solving a guard.

Axioms are of type (1), (2) or (6). The step functions (or consequence operators) induced by axioms must be monotone [P00,P05]. Usually, f, p resp. q agree with the root of the redex to which a clause is applied.

For applying a non-distributed clause, select a term/atom at' with positive/negative polarity in the displayed tree such that the leading term/atom at is unifiable with at'. at' is replaced by the corresponding instance of prem/conc.

For applying a distributed clause cl, select n atoms at1',...,atn' in a disjunction/conjunction F with positive/negative polarity of the displayed tree such that for all 1 <= i <= n, ati is unifiable with ati'. The summands/factors of F where at1',...,atn' are selected from must not contain universal/existential quantifiers or negation or implication symbols. at1',...,atn' are replaced by the corresponding instance of prem/conc. The resulting summands/factors are combined conjunctively if cl is a Horn clause and disjunctively if cl is a co-Horn clause (see [FMS,P02]).

When a formula F with a stretchable premise/conclusion is selected for application, then the premise/conclusion of F is streched and thus F is turned into a co-Horn/Horn clause (see fixpoint induction for premise stretching and coinduction for conclusion stretching), which is then applied as in case (3), (4), (6) or (7), respectively.


A proof with Expander2 is a sequence of successive values of the state variable trees. It is documented and stored in the state variable proof. The values of proof and current trees are initialized whenever parse up parses the contents of the text field and displays the resulting tree t on the canvas. Then trees is set to [t], tree is set to t, and proof is set to the initial values of its components.

A proof step is correct if the transformed disjunction (or conjunction or sum) of the current trees implies (or is equivalent to) the original one. In the case of possible incorrectness Expander2 delivers the warning

	CAUTION: This step may be semantically incorrect.

Such steps are not stored in the current proof term.

If the current trees are formulas, a proof ending up with True or False yields a proof resp. refutation of the conjunction/disjunction of the initial trees. Other final results are given by solved formulas that represent solutions of the original conjecture in their free variables.

Axioms of the form {guard ==>} t -> u {<=== prem} can only be applied to left-hand sides of transitional atoms t' -> v. If t and t' are unifiable, then t' -> v is replaced by the corresponding instance of the formula u = v {& prem} provided that the unifier satisfies guard (see Built-in signature).

If the current trees are terms, the application of an axiom yields a rewriting step from a term to a term. Hence only axioms of the form {guard ==>} t = u or {guard ==>} t -> u may be applied: the term to be rewritten is matched against t replaced by the corresponding instance of u provided that the corresponding instance of guard is solvable (by narrowing). If several axioms are applicable to the same term, they are applied in parallel and the reducts are combined by <+> to a sum term. For semantical reasons, the latter should only happen if an axiom of the form {guard ==>} t -> u is applied.

A higher-order variable F may be substituted when terms or formulas are matched or unified, but only if the symbol g substituted for F is admissable for F (see Built-in signature) and either the outdegrees of the nodes m and n labelled with F resp. g are equal or the outdegree of m is 0 and the entire subtree with root n is substituted for m. The correctness of a proof step depends on the polarity of the redex with respect to its position within the displayed tree. The polarity is positive if the number of preceding negation symbols or premise positions is even. Otherwise the polarity is negative. Fixpoint induction, coinduction, summand removal, summand unification, applications of Horn clauses, instantiations of existential variables and term replacements (see replace by other sides) are correct if the redex has positive polarity because here the reduct implies the redex. Atom composition, factor removal, factor unification, applications of co-Horn clauses and instantiations of universal variables are sound if the redex has negative polarity because here the redex implies the reduct. Simplification, rewriting, narrowing in a unify mode (see the narrow/rewrite buttons), splitting, flattening and stretching may be applied to any possible redex within the displayed tree because here the redex and the reduct are equivalent. Narrowing in a match mode may also be applied to any possible redex. However, if a narrowing redex unifies, but does not match with some axiom, narrowing in a match mode is stopped with a corresponding message. All these restrictions ensure that the resulting formula implies the original one.

The theorem-proving features of Expander2 do not aim at fully automatic proofs. Expander2 favors natural deduction in contrast to many other provers that submit a conjecture to Skolemization and other extensive normalizations before the proof can start. This restricts the readability and thus the controllability of derivation processes significantly, especially when induction or coinduction steps are involved that are at the heart of any non-trivial program verification. Fortunately, the axioms, the theorems and, to some extent, the conjectures we are faced with in program verification already come as Horn or co-Horn clauses and thus can indeed be handled by Expander2 in their original form.

It also complies with a natural proof process that Expander2 avoids negation symbols. The simplifier drives them innermost until they directly precede (co)predicates and can be removed completely by transforming the (co)predicates into their complements (see negate axioms for symbol). Negation-free axioms induce monotone consequence operators. Hence predicates and copredicates have least resp. greatest interpretations in the initial model of the underlying specification [P00,P05].


Variables of a clause that are introduced into the current tree when the clause is applied to the tree are renamed by increasing the number suffixes of the variables. Variables that the tree shares with the applied clause are renamed in the same way. Since variable renaming affects the state variable varCounter, it is not performed during simplification.

Variables of a Horn or co-Horn clause are turned into existential resp. universal variables. The scope of these variables is the respective reduct.

If a free variable x of a redex is instantiated by a term t during a rewriting or narrowing step, then the equation x=t is added to the reduct.


Narrowing removes predicates, copredicates and non-constructor functions from the current trees. The simplifier does the same with logical operators, constructors and built-in symbols. Simplifications realize the highest degree of automation and the lowest level of interaction (see Overview). Pushing the simplify button admits step-by-step simplification of the current trees. The rules applied by the simplifier employ not only logical equivalences, but also the semantics of constructors, equality or inequality predicates and other built-in symbols. For instance, an implication prem==>conc is reduced to True if prem subsumes conc, a disjunction is reduced to its minimal summands, a conjunction to its maximal factors. Here are some examples:
 Any x y z:(x=f(y) & Q(z)) ==> Any x' y' z':(Q(z') & f(y')=x')

reduces to True.
 Any x:Q(x) & Q(suc(y)) & All x:R(x) & R(y+z) & Any x:x=suc(y) & suc(y)=y+z

reduces to Q(suc(y)) & All x:R(x) & suc(y)=y+z.
 Any x: (x = f(h(y,z),z) & P(x,y))

& All x: (x =/= f(h(y,z),z) | P(x,y))

& All x: (x = f(h(y,z),z) & P(x,y) ==> Q(x))

& All x: (P(x,y) ==> x =/= f(h(y,z),z) | Q(x)).

reduces to P(f(h(y,z),z),y) & Q(f(h(y,z),z)).
 P(x,y) & Q(z) & (P(x,y) ==> R(x,y,z))

reduces to P(x,y) & Q(z) & R(x,y,z).
 P(x,y) ==> (Q(y) ==> R(x,y,z)) | P(y,z)

reduces to P(x,y) & Q(y) ==> R(x,y,z) | P(y,z).
 2 `in` [1,2,3]

reduces to True.
 y `in` [1,x,4]

reduces to y=1 | y=x | y=4. The example shows that an atom of the form t`in`ts where t and ts are constructor terms is simplified to a solved formula and can thus be used in the guard of an axiom.
 [2,3]++[5`mod`2,1] <+> 78 <+>{}^{9,5,5}^{9,9,5}

reduces to [2,3,1,1] <+> 78 <+> {}^{5,9}^{5,9}.

reduces to [1,3].

reduces to x=2 | 3=y.

reduces to True.

reduces to x=2 & 3=y.

All rules applied by the simplifier and dealing with logical operators and equality or inequality predicates are listed in [Prover], section 5. This section also contains a defintion of subsumption (see above) that captures almost all implications whose validity follows from their syntactic structure.

Fig. 8. The environment of state terms

Some commands induce the creation of state terms. A state term consists of a state constructor and attributes of various types and may occur as part of any other term or formula (see the parse buttons). If the simplifier encounters a state term t in the current tree, it calls a built-in Haskell function f that operates on the attributes of t and assigns new values to the attributes of t. The entire current tree is modified accordingly. The attributes of a state term do not appear on the canvas or in the text field of a solver. However, the painter may be able to translate them into pictures.

Fig. 9. All dissections of a 3x3-rectangle that satisfy area(2):
each dissection consists of ceiling(9/2)=5 subrectangles.

The following Haskell programs executed (stepwise) by the simplifier use and modify state terms:

The programs receive their input by initializing the associated state terms. The initialization consists in rewriting synomymous constants upon particular equational axioms or calling build Trans/TransL: The individual programs are executed as follows:


specification or axioms theorems conjectures derivation or proof term
alignments ALIGN
and simplifications
DIVproof DIVterm
EVproof EVterm
POTproof POTterm
WIRTHproof WIRTHterm
binary trees BTREE REPMIN
Boolean functions BOOL OBDD
concept formation FRUIT FRUITths FRUITconjs FRUIT1proof ...
finite sequences LIST LISTEVAL
PARTproof PARTterm
PARTproof2 PARTterm2
SORTproof PERMproof
PARTNproof PARTNterm
PARTN2proof PARTN2term
imperative programs FACTPOST
infinite sequences STREAM
STREAMths STREAMconjs FAIRBLINK proof term
BLINKZIP proof term
ITER1ITER2 proof term
ITERLOOP proof term
ODDSEVENS proof term
MAPFACT proof term
MAPITER1 proof term
MAPLOOP proof term
MAPLOOP0 proof term
NATLOOP proof term
ZIPODDS proof term
ABPproofA1 ABPproofA2
ABPproofB ABPproofC
ABPproofD ABPproofE
needed narrowing NEED NEEDproof NEEDterm
NEED1proof NEED2proof
parser LR1 LR2 LR1run LR2run
and partitions
LOG LOGproof LOGproof1
LOGproof2 PARTsols
pictures CARPET
files whose names start
with a small letter
regular expressions COREGS
sets and relations SET GRAPHS
SET1 SETproof
RELALG1proof RELALG2proof
NEWMAN2proof NEWMAN2term
UPDproof UPDterm
transition systems
and model checking
CTLlist CTLlablist
BOTTLEsols CTLproof
CTLlabproof CTLlabterm
ECHOproof ECHOACproof
PHIL1proof PHIL2proof
PHILAC1proof PHILAC2proof
ROBOTsols2 ROBOTactsproof

Widget interpreters

Built on top of the Tk interface module Tk.hs, the module Epaint provides features for creating and editing pictorial term representations. These are displayed in the painter window of a solver when a paint button is pushed. The scroll region of this window is adapted automatically to the displayed picture.

Expander2 provides several widget interpreters and combinators thereof, which recognize paintable terms and transform them into pictorial representations. The actual widget interpreter can be selected from the pict type menu. The default interpreter is matrices. The alignment enumerator and the palindrome enumerator are associated with the alignment interpreter, the dissection enumerator with rectangles and the partition enumerator with partition.

The basic elements of pictorial term representations are called widgets. A picture is a list of widgets. A widget graph G is a pair consisting of a picture [w1,...,wn] and a list [as1,...,asn] of sublists of [1,...,n] that represents the set A of arcs of G:

A = {(wi,wj) | j ∈ asi, 1 <= i,j <= n}.

For editing widget graphs, see Figures 20 and 21 and the paint buttons.

A graph is saved in Haskell code to Examples/file or in eps format to Pics/file.eps  by writing file resp. file.eps into the save to field and pushing the Down key while the cursor is in this field.

Widgets are encoded in Haskell as follows:

 data Widget_ = Arc Color ArcStyleType Point Float (Float,Float) | 

Arc0 State ArcStyleType Float Float |

Arc0, Path0 and Tree0 are abstract versions of Arc, Path resp. Tree

which they are turned into before being displayed.

Bunch Widget_ [Int] |

Bunch w ns represents widget w together with arcs leading from w

to the widgets at positions ns.

Circ State Float | CircA State Float | Dot Color Point |

CircA and RectA ignore the scale of enclosing turtles.

Fast Widget_ | File_ String | Gif String Point | New | Old | Path Color Int [Point] |

Path0 State Int [Point] | Poly State Int [Float] Float | Rect State Float Float |

RectA State Float Float | Repeat Widget_ | Snow State Int Float | Text_ State [String] |

Tree Color Color (Term TNode) | Tree0 State String Color [Term TNode] |

Tria State Float | Turtle State Float [TurtleAct] | White

data TurtleAct = Move Float | MoveA Float | Jump Float | JumpA Float | Turn Float |

MoveA and JumpA ignore the scale of the enclosing turtle.

Open Color Int | Scale Float | Close | Draw | Widg Widget_ | WidgB Widget_

Widg w ignores the orientation of the enclosing turtle,

WidgB w adds it to the orientation of w.

type State = (Point,Float,Color,Int)

type TNode = (String,Point)

type Point = (Float,Float)

A widget is a two-dimensional object with state. The state is a quadruple (p,a,c,i) consisting of the widget's actual position (as Cartesian coordinates), orientation (in degrees), (brilliant) color and lightness (see the picture operators newLight and nextLight described below). Only color and lightness can be set directly by the user. The standard values of p and a are (0,0) and 0, respectively. Other values are computed by the painter in dependence of picture (generating or modifying) operators called by the user.

Certain picture operators interpreted by polygon (see below) have a color parameter c that is used as the first element of a list cs of equidistant colors, i.e. the difference between the RGB values of two subsequent colors of cs is always the same. The colors are ordered like in a rainbow.For ensuring the correct computation of cs from c, c should be a pure (hue) color, i.e. c is neither black nor white and at most one of the R-, G- and B-values of c is different from both 0 and 255. If you want the picture operator to create a light or dark version of the colors of cs, you must apply it to the pure version of c and then apply to the result the picture operator newLight or nextLight with the desired lightness value i (see below). Then all colors of cs will be lightened (or darkened if i is negative) as desired. 

Colors must be entered as strings generated by the color grammar (see the Grammar).

Each widget interpreter is a Haskell function of type Term String -> Maybe Picture.

A displayed graph is always aligned to the top and the left of the painter's canvas. The available graph editing commands are shown in Figures 20 and 21.

Fig. 20. Graph editing actions I

Fig. 21. Graph editing actions II
In all states reachable from rect, the displayed graph contains a rectangle whose enclosed widgets are processed differently from the rest of the graph.

pict type menu

The actual widget interpreter is set in the pict type menu. The interpreters, the term patterns they recognize and the widget graphs they display on the canvas of a painter read as follows.

alignment recognizes syntax trees generated by the grammar G1 or G2 of section Alignments and palindromes are displayed as horizontal alignments.

graph transforms the current tree into a widget graph. Subterms of the form widg(t1,...,tn,t) such that polygon (see below) recognizes t as a single widget w is turned into the subgraph w(g1,...,gn) where gi is the widget graph for ti, 1<=i<=n. Other non-pointer nodes are turned into text widgets. Each non-tree edge of the current tree is compiled into a B-splined arc with a red control point for interactive reshaping.

t1 t2 p w
Fig. 22. Simplifying and rewriting term t1 with axioms of trans0
leads to term t2, which is further simplified to a term that is compiled by
graph into picture p and by matrix into widget w.

linear equations: A term of the form p1=r1 & ... & pn=rn where p1,...,pn are polynomials and r1,...,rn are real numbers is interpreted as a system of linear equations and displayed as the corresponding matrix of coefficients. The variables occurring in the equations must be part of the current signature (see gauss1).

matrix interprets the following rooted graphs and displays them as corresponding matrices.

matrix solution recognizes each solved formula

and submits the terms t1,...,tn to matrix.

combines the maximal subgraphs of the current graphs that are recognizable by matrix.

partition interprets the displayed tree t as a nested partition (see Dissections and partitions) and draws t as a square combined of colored rectangles each of which represents a leaf of t. The coloring method can be changed by pushing the combis button (see the paint buttons).

Fig. 23. Widgets drawn by the polygons interpreter

Fig. 24. More widgets drawn by the polygons interpreter

polygon interprets the following rooted graphs and displays them as corresponding pictures. ps denotes a list of pictures (with or without enclosing square brackets).

polygon solution recognizes each solved formula

and submits the terms t1,...,tn to polygon.

polygons combines the maximal subgraphs of the current graphs that are recognizable by polygon.

rectangles interprets a term of the form [(x1,y1,b1,h1),...,(xn,yn,bn,hn)] as a collection of rectangles r1,...,rn such that for all 1 <= i <= n, (xi,yi) is the top-left corner, bi the breadth and hi is the height of ri.

If a file F contains the Haskell code of a graph G, each interpreter compiles the term file(F) into G. Conversely, given a term t that represents a graph G, if the command store graph is applied to the term file(t,F), it saves the Haskell code of G to F and replaces file(t,F) by file(F) (see the graph menu).

Alignments and palindromes

This and the following sections deal with the alignment, palindrome, dissection and partition enumerators that can be called from the solver's term/formula menu. Other enumeration algorithms may be added accordingly. The alignment enumerator and the palindrome enumerator compute alignments between two string sequences [Gie] or within a single sequence [GM], respectively. A development of the Haskell program for the former can be found in [P01], Section 2.4.

After two lines xs and ys of strings separated by blanks have been entered into the text field, the alignment enumerator asks for a constraint. There are two possibilities:

Following the assignment of complementary DNA bases, the function compl maps a to t, t to a, c to g, g to c and all other strings to #. Corresponding axioms are loaded when the alignment or palindrome enumerator is called from the solver.

Given the sequences

 s1 = a c t a c t g c t, s2 = a g a t a g,

s3 = a d f a a a a a a, s4 = a a a a a a d f a,

the trees in Fig. 25 are the only two syntax trees of s1#reverse(s2) that meet the match-constraint and the only two syntax trees of s3#reverse(s4) that meet the match-constraint and the local-constraint, respectively. Here compl is defined by ALIGN.

Fig. 25. Alignment terms and their pictorial representations

Fig. 26. The pictorial representation of the palindrome "Ein Neger blubb mit Gazelle zagt im Recen nie".
Again, compl is defined by ALIGN.

After a sequence xs of strings separated by blanks has been entered into the text field, the palindrome enumerator computes syntax trees for xs with a maximal number of equal- or compl-nodes according to grammar G above with end rule replaced by two rules:

 single : match ---> s for all strings s

end : align ---> _

Moreover, the match rule is preferred to the insert and delete rules. Again, compl is a function on strings defined by a specification that must be entered before the enumerator is called (see above).

Dissections and partitions

Fig. 27. All dissections of a 5x4-rectangle that satisfy area(1,2)&brick&hori:
each dissection satisfies brick and consists of subrectangles covering 1 or 2 unit squares
and satisfying hori (see below).

Fig. 28. All dissections of a 6x4-rectangle that satisfy eqarea(6):
each dissection consists of 6 subrectangles that cover the same area.

Fig. 29. All dissections of a 6x6-rectangle that satisfy sizes[6]&factor(2):
each dissection consists of 6 subrectangles and the breadth b and the height h
of each subrectangle satisfy b=2*h or h=2*b.

The dissection enumerator computes dissections of a rectangle and represents them directly without a detour via term representations. The underlying algorithm creates and modifies a triple of lists of top, left and inner subrectangles, respectively, such that dissection elements violating certain given constraints are discarded as early as possible (see [P94], Section 4).

Constraints. The dissection enumerator returns dissections of a given rectangle with breadth b and height h that satisfy one of the following atomic constraints or disjunctive or conjunctive combinations thereof:

constraint holds true for all dissections
area(n) consisting of ceiling((b*h)/n) subrectangles that cover at most n unit squares
area(m,n) consisting of subrectangles that cover at least m and at most n unit squares
brick consisting of subrectangles r such that for all (x,y,b,h),(x,y',b',h') ∈ r, x=0, y'=/=y+h y' or y=/=y'+h' (see below)
eqarea(n) consisting of n subrectangles that cover the same number of unit squares
factor(p) consisting of subrectangles such that the breadth b and the height h of each subrectangle satisfy b=p*h or h=p*b
hori consisting of subrectangles whose height does not exceed the breadth
sizes(ns) consisting of n ∈ ns subrectangles
vert consisting of subrectangles whose breadth does not exceed the height

Formulas built up of atomic constraints are parsed according to the Grammar. Each constraint is translated into a triple of the Haskell type

 ((Int,Int,Int,Int) -> Bool, [Int], [(Int,Int,Int,Int)] -> [(Int,Int,Int,Int)] -> Bool).

The first component is a Boolean function that checks individual rectangles each of which is represented as a quadruple (x,y,b,h) where (x,y) is the top-left corner, b the breadth and h the height of the rectangle.
The second component lists the admissable cardinalities of a dissection. The third component is a Boolean function that checks a relation between two parts of a dissection. Such a Boolean function is needed for expressing the brick constraint.

Fig. 30. A nested partition satisfying eqout&sym of a list with 10 elements and its interpretation by partition (see the pict type menu).

Fig. 31. The nested partitions satisfying bal&eqout of a list with 16 elements

The partition enumerator computes nested partitions of a list and represents them as trees whose nodes are labelled with the nesting degrees of the respective subpartitions. Partitions with singleton subpartitions are not constructed.

Let s be a set with n elements and parts(s) be the set of non-nested partitions of s with at least two elements. A Haskell program that computes the cardinality f(n) of parts(s) reads as follows:

 f 0 = 1

f n = sum (map g [0..n-1]) where g i = (fact n/(fact (n-i)*fact i))*f i

fact i = product [1..i]

For the number h(n) of nested partitions of s we obtain:
	h 2 = 1

h n | n > 2 = sum[product[h (length p) | p <- ps] | ps <- parts s]

Hence, without meeting additional constraints, the number of trees representing nested partitions increases combinatorially with the number of leaves:

number of leaves number of trees
5 45
6 197
7 903
8 4279
9 20793
10 103049

Constraints. The partition enumerator returns nested partitions that satisfy one of the following atomic constraints or disjunctive or conjunctive combinations thereof.

constraint holds true for all trees
alter whose nodes at even (odd) positions of a list s of all nodes with the same direct predecessor
are leaves (inner nodes) unless s consists of leaves
bal that are balanced
eqout whose inner nodes with the same direct predecessor have the same outdegree
hei(n) whose height is at most n
levmin whose inner nodes at level n have an outdegree of at least n
levmax whose nodes at level n have an outdegree of at most max(2,n)
sym that are vertically symmetric
out(m,n) whose inner nodes at level n > 1 have an outdegree between m and n

Formulas built up of atomic constraints are parsed according to the Grammar